PA can reason about ZFC [001I]

A proof in ZFC ist just a finite string of symbols. By encoding strings as natural numbers statements about proofs can be translated to statements about natural numbers and thus reasoned about within PA.