Just slightly expanding the comment of Emil Jeřábek: on one hand, in ZFC we can define some objects we call ordinals and prove transfinite induction of each of them. This is not what we mean by the ordinal of ZFC. The latter is defined roughly as follows (although there are several nonequivalent definitions):

1. You take some recursive relation, such that in the actual natural numbers, this relation is well-founded and you actually fix some algorithm which describes this relation (as a set of pairs).

2. Then you ask, whether the theory in question proves that the relation given by this algorithm is a well-founded one.

For instance, think of the following relation $R$: $R(m,n)$ iff $m<n$ and there is no proof of $0 \neq 0$ from the axiom of ZFC or $m>n$ otherwise. This relation is wellfounded (namely isomorphic to $\omega$) iff ZFC is consistent, so ZFC does not even prove that $\omega$ is well-founded under totally arbitrary presentation of $\omega$.

Notice that the above example could give an impression that no theory can have its prof-theoretic ordinal bigger than $\omega,$ therefore precise definition of this concept is a rather subtle issue and there are several nonequivalent definitions. But the rough idea, of what may go wrong is precisely this.

Just slightly expanding the comment of Emil Jeřábek: on one hand, in ZFC we can define some objects we call ordinals and prove transfinite induction of each of them. This is not what we mean by the ordinal of ZFC. The latter is defined roughly as follows (although there are several nonequivalent definitions):

1. You take some recursive relation, such that in the actual natural numbers, this relation is well-founded and you actually fix some algorithm which describes this relation (as a set of pairs).

2. Then you ask, whether the theory in question proves that the relation given by this algorithm is a well-founded one.

For instance, think of the following relation $R$: $R(m,n)$ iff $m<n$ and there is no proof of $0 \neq 0$ from the axiom of ZFC using less than $m$ symbols or $m>n$ otherwise. This relation is easily verified to be a recursive linear order by even very weak theories but is wellfounded (namely isomorphic to $\omega$) iff ZFC is consistent, so ZFC does not even prove that $\omega$ is well-founded under totally arbitrary presentation of $\omega$.

Notice that the above example could give an impression that no theory can have its prof-theoretic ordinal bigger than $\omega,$ therefore precise definition of this concept is a rather subtle issue and there are several nonequivalent definitions. But the rough idea, of what may go wrong is precisely this.

Just slightly expanding the comment of Emil Jeřábek: on one hand, in ZFC we can define some objects we call ordinals and prove transfinite induction of each of them. This is not what we mean by the ordinal of ZFC. The letter is defined roughly as follows (although there are several nonequivalent definitions):

1. You take some recursive relation, such that in the actual natural numbers, this relation is well-founded and you actually fix some algorithm which describes this relation (as a set of pairs).

2. Then you ask, whether the theory in question proves that the relation given by this algorithm is a well--founded one.

For instance, think of the following relation $R$: $R(m,n)$ iff $m<n$ and there is no proof of $0 \neq 0$ from the axiom of ZFC or $m>n$ otherwise. This relation is wellfounded (namely isomorphic to $\omega$) iff ZFC is consistent, so ZFC does not even prove that $\omega$ is well-founded under totally arbitrary presentation of $\omega$.

Notice that the above example could give an impression that no theory can have its prof-theoretic ordinal bigger than $\omega,$ therefore precise definition of this concept is a rather subtle issue and there are several nonequivalent definitions. But the rough idea, of what may go wrong is precisely this.

Just slightly expanding the comment of Emil Jeřábek: on one hand, in ZFC we can define some objects we call ordinals and prove transfinite induction of each of them. This is not what we mean by the ordinal of ZFC. The latter is defined roughly as follows (although there are several nonequivalent definitions):

1. You take some recursive relation, such that in the actual natural numbers, this relation is well-founded and you actually fix some algorithm which describes this relation (as a set of pairs).

2. Then you ask, whether the theory in question proves that the relation given by this algorithm is a well-founded one.

For instance, think of the following relation $R$: $R(m,n)$ iff $m<n$ and there is no proof of $0 \neq 0$ from the axiom of ZFC or $m>n$ otherwise. This relation is wellfounded (namely isomorphic to $\omega$) iff ZFC is consistent, so ZFC does not even prove that $\omega$ is well-founded under totally arbitrary presentation of $\omega$.

Notice that the above example could give an impression that no theory can have its prof-theoretic ordinal bigger than $\omega,$ therefore precise definition of this concept is a rather subtle issue and there are several nonequivalent definitions. But the rough idea, of what may go wrong is precisely this.