Theorem om2uzuzi

Description: The value G (see om2uz0i ) at an ordinal natural number is in the upper integers. (Contributed by NM, 3-Oct-2004) (Revised by Mario Carneiro, 13-Sep-2013)

	Ref	Expression
Hypotheses	om2uz.1	$$⊢C\in \mathbb{Z}$$
	om2uz.2	$$⊢G={\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),C\right)\upharpoonright }_{\mathrm{\omega }}$$
Assertion	om2uzuzi	$$⊢A\in \mathrm{\omega }\to G\left(A\right)\in {\mathbb{Z}}_{\ge C}$$

Proof

Step	Hyp	Ref	Expression
1		om2uz.1	$$⊢C\in \mathbb{Z}$$
2		om2uz.2	$$⊢G={\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),C\right)\upharpoonright }_{\mathrm{\omega }}$$
3		fveq2	$$⊢y=\varnothing \to G\left(y\right)=G\left(\varnothing \right)$$
4	3	eleq1d	$$⊢y=\varnothing \to \left(G\left(y\right)\in {\mathbb{Z}}_{\ge C}\leftrightarrow G\left(\varnothing \right)\in {\mathbb{Z}}_{\ge C}\right)$$
5		fveq2	$$⊢y=z\to G\left(y\right)=G\left(z\right)$$
6	5	eleq1d	$$⊢y=z\to \left(G\left(y\right)\in {\mathbb{Z}}_{\ge C}\leftrightarrow G\left(z\right)\in {\mathbb{Z}}_{\ge C}\right)$$
7		fveq2	$$⊢y=\mathrm{suc}z\to G\left(y\right)=G\left(\mathrm{suc}z\right)$$
8	7	eleq1d	$$⊢y=\mathrm{suc}z\to \left(G\left(y\right)\in {\mathbb{Z}}_{\ge C}\leftrightarrow G\left(\mathrm{suc}z\right)\in {\mathbb{Z}}_{\ge C}\right)$$
9		fveq2	$$⊢y=A\to G\left(y\right)=G\left(A\right)$$
10	9	eleq1d	$$⊢y=A\to \left(G\left(y\right)\in {\mathbb{Z}}_{\ge C}\leftrightarrow G\left(A\right)\in {\mathbb{Z}}_{\ge C}\right)$$
11	1 2	om2uz0i	$$⊢G\left(\varnothing \right)=C$$
12		uzid	$$⊢C\in \mathbb{Z}\to C\in {\mathbb{Z}}_{\ge C}$$
13	1 12	ax-mp	$$⊢C\in {\mathbb{Z}}_{\ge C}$$
14	11 13	eqeltri	$$⊢G\left(\varnothing \right)\in {\mathbb{Z}}_{\ge C}$$
15		peano2uz	$$⊢G\left(z\right)\in {\mathbb{Z}}_{\ge C}\to G\left(z\right)+1\in {\mathbb{Z}}_{\ge C}$$
16	1 2	om2uzsuci	$$⊢z\in \mathrm{\omega }\to G\left(\mathrm{suc}z\right)=G\left(z\right)+1$$
17	16	eleq1d	$$⊢z\in \mathrm{\omega }\to \left(G\left(\mathrm{suc}z\right)\in {\mathbb{Z}}_{\ge C}\leftrightarrow G\left(z\right)+1\in {\mathbb{Z}}_{\ge C}\right)$$
18	15 17	imbitrrid	$$⊢z\in \mathrm{\omega }\to \left(G\left(z\right)\in {\mathbb{Z}}_{\ge C}\to G\left(\mathrm{suc}z\right)\in {\mathbb{Z}}_{\ge C}\right)$$
19	4 6 8 10 14 18	finds	$$⊢A\in \mathrm{\omega }\to G\left(A\right)\in {\mathbb{Z}}_{\ge C}$$