A quick google search shows different proof assistants have been used to obtain the Peano axioms from ZFC, such as Isabelle/ZF and Metamath. I think you're just wrong

That increases the likelihood that they are right.

> support your point with explanation or be ignored :-)

Anyone who says "Godel theorems are for systems with basic arithmetic, zfc doesn't include arithmetic, thus are not object of Godel theorems" and isn't joking warrants a permanent ignore.

https://math.stackexchange.com/questions/1366560/why-does-g%...

https://math.stackexchange.com/questions/1090437/how-to-prov...