I can't answer your second question, because I don't have the book you're referring to. But here's what I have to offer for the first one:
It is very easy, when first reading about these things, to be lured into thinking that formal reasoning in ZFC is "what mathematics really is", and the usual sort of English prose arguments found in textbooks and papers is just a sloppy conventional shorthand for the actual underlying ZFC reasoning. This is a very appealing picture for someone who likes to take things apart to find out how they work -- it struck me as a tremendous epiphany the first time I learned it.
Unfortunately, as you have also noticed, the world can't be quite that neat. This picture leaves no place for reasoning about ZFC and formal logic to stand on. On one hand this seems to make all of mathematics an ultimately circular exercise; on the other it would feel wrong to say that reasoning about formal logic is a special kind of mathematical thought that doesn't need to be built upon ZFC -- because it clearly feels like the same kind of reasoning we use in other mathematical fields such as calculus or graph theory.
The most common modern resolution of this dilemma is to say that formal logic (and with it formalizations of set theory in formal logic) is not what mathematical reasoning really is. Rather, formal logic is (merely?) a mathematical model of everyday mathematical reasoning. It's a pretty good model in that it is remarkably successful in predicting which kinds of arguments you can get a skeptical mathematician to accept as mathematical, but that doesn't change the fact that the model is not the thing itself.
One point to note is that mathematical reasoning has been going on for centuries (millenia!) but formal logic was only developed during the first half of the 20th century. It would be ridiculous to say that Gauss, Euler, or Cauchy were not actually doing mathematics, and it would be untenable sophistry to claim that they were "really" following precise rules of symbolic manipulation that were only "discovered" (rather than invented) in the 1900s.
Mathematical reasoning exists, inside the heads of mathematicians, without any need for a particular formalization of it to prop it up. The followers "Hilbert's program" around 1900 imagined it could be improved by propping it up by a reduction to clearly defined rules, but as the work to do so was actually done, it turned out that it couldn't really work that way. The results are nevertheless interesting in their own right. The word "foundation" lingers on from those early days, and continues to confuse students because formal logic doesn't really provide the solid, indubitable, "foundation" for the rest of mathematics that the word promises.