Theorem om2uzf1oi

Description: G (see om2uz0i ) is a one-to-one onto mapping. (Contributed by NM, 3-Oct-2004) (Revised by Mario Carneiro, 13-Sep-2013)

	Ref	Expression
Hypotheses	om2uz.1	⊢ 𝐶 ∈ ℤ
	om2uz.2	⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐶 ) ↾ ω )
Assertion	om2uzf1oi	⊢ 𝐺 : ω –1-1-onto→ ( ℤ≥ ‘ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		om2uz.1	⊢ 𝐶 ∈ ℤ
2		om2uz.2	⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐶 ) ↾ ω )
3		frfnom	⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐶 ) ↾ ω ) Fn ω
4	2	fneq1i	⊢ ( 𝐺 Fn ω ↔ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐶 ) ↾ ω ) Fn ω )
5	3 4	mpbir	⊢ 𝐺 Fn ω
6	1 2	om2uzrani	⊢ ran 𝐺 = ( ℤ≥ ‘ 𝐶 )
7	6	eqimssi	⊢ ran 𝐺 ⊆ ( ℤ≥ ‘ 𝐶 )
8		df-f	⊢ ( 𝐺 : ω ⟶ ( ℤ≥ ‘ 𝐶 ) ↔ ( 𝐺 Fn ω ∧ ran 𝐺 ⊆ ( ℤ≥ ‘ 𝐶 ) ) )
9	5 7 8	mpbir2an	⊢ 𝐺 : ω ⟶ ( ℤ≥ ‘ 𝐶 )
10	1 2	om2uzuzi	⊢ ( 𝑦 ∈ ω → ( 𝐺 ‘ 𝑦 ) ∈ ( ℤ≥ ‘ 𝐶 ) )
11		eluzelz	⊢ ( ( 𝐺 ‘ 𝑦 ) ∈ ( ℤ≥ ‘ 𝐶 ) → ( 𝐺 ‘ 𝑦 ) ∈ ℤ )
12	10 11	syl	⊢ ( 𝑦 ∈ ω → ( 𝐺 ‘ 𝑦 ) ∈ ℤ )
13	12	zred	⊢ ( 𝑦 ∈ ω → ( 𝐺 ‘ 𝑦 ) ∈ ℝ )
14	1 2	om2uzuzi	⊢ ( 𝑧 ∈ ω → ( 𝐺 ‘ 𝑧 ) ∈ ( ℤ≥ ‘ 𝐶 ) )
15		eluzelz	⊢ ( ( 𝐺 ‘ 𝑧 ) ∈ ( ℤ≥ ‘ 𝐶 ) → ( 𝐺 ‘ 𝑧 ) ∈ ℤ )
16	14 15	syl	⊢ ( 𝑧 ∈ ω → ( 𝐺 ‘ 𝑧 ) ∈ ℤ )
17	16	zred	⊢ ( 𝑧 ∈ ω → ( 𝐺 ‘ 𝑧 ) ∈ ℝ )
18		lttri3	⊢ ( ( ( 𝐺 ‘ 𝑦 ) ∈ ℝ ∧ ( 𝐺 ‘ 𝑧 ) ∈ ℝ ) → ( ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑧 ) ↔ ( ¬ ( 𝐺 ‘ 𝑦 ) < ( 𝐺 ‘ 𝑧 ) ∧ ¬ ( 𝐺 ‘ 𝑧 ) < ( 𝐺 ‘ 𝑦 ) ) ) )
19	13 17 18	syl2an	⊢ ( ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) → ( ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑧 ) ↔ ( ¬ ( 𝐺 ‘ 𝑦 ) < ( 𝐺 ‘ 𝑧 ) ∧ ¬ ( 𝐺 ‘ 𝑧 ) < ( 𝐺 ‘ 𝑦 ) ) ) )
20		ioran	⊢ ( ¬ ( ( 𝐺 ‘ 𝑦 ) < ( 𝐺 ‘ 𝑧 ) ∨ ( 𝐺 ‘ 𝑧 ) < ( 𝐺 ‘ 𝑦 ) ) ↔ ( ¬ ( 𝐺 ‘ 𝑦 ) < ( 𝐺 ‘ 𝑧 ) ∧ ¬ ( 𝐺 ‘ 𝑧 ) < ( 𝐺 ‘ 𝑦 ) ) )
21	19 20	bitr4di	⊢ ( ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) → ( ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑧 ) ↔ ¬ ( ( 𝐺 ‘ 𝑦 ) < ( 𝐺 ‘ 𝑧 ) ∨ ( 𝐺 ‘ 𝑧 ) < ( 𝐺 ‘ 𝑦 ) ) ) )
22		nnord	⊢ ( 𝑦 ∈ ω → Ord 𝑦 )
23		nnord	⊢ ( 𝑧 ∈ ω → Ord 𝑧 )
24		ordtri3	⊢ ( ( Ord 𝑦 ∧ Ord 𝑧 ) → ( 𝑦 = 𝑧 ↔ ¬ ( 𝑦 ∈ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) )
25	22 23 24	syl2an	⊢ ( ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) → ( 𝑦 = 𝑧 ↔ ¬ ( 𝑦 ∈ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) )
26	25	con2bid	⊢ ( ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) → ( ( 𝑦 ∈ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ↔ ¬ 𝑦 = 𝑧 ) )
27	1 2	om2uzlti	⊢ ( ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) → ( 𝑦 ∈ 𝑧 → ( 𝐺 ‘ 𝑦 ) < ( 𝐺 ‘ 𝑧 ) ) )
28	1 2	om2uzlti	⊢ ( ( 𝑧 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝑧 ∈ 𝑦 → ( 𝐺 ‘ 𝑧 ) < ( 𝐺 ‘ 𝑦 ) ) )
29	28	ancoms	⊢ ( ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) → ( 𝑧 ∈ 𝑦 → ( 𝐺 ‘ 𝑧 ) < ( 𝐺 ‘ 𝑦 ) ) )
30	27 29	orim12d	⊢ ( ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) → ( ( 𝑦 ∈ 𝑧 ∨ 𝑧 ∈ 𝑦 ) → ( ( 𝐺 ‘ 𝑦 ) < ( 𝐺 ‘ 𝑧 ) ∨ ( 𝐺 ‘ 𝑧 ) < ( 𝐺 ‘ 𝑦 ) ) ) )
31	26 30	sylbird	⊢ ( ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) → ( ¬ 𝑦 = 𝑧 → ( ( 𝐺 ‘ 𝑦 ) < ( 𝐺 ‘ 𝑧 ) ∨ ( 𝐺 ‘ 𝑧 ) < ( 𝐺 ‘ 𝑦 ) ) ) )
32	31	con1d	⊢ ( ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) → ( ¬ ( ( 𝐺 ‘ 𝑦 ) < ( 𝐺 ‘ 𝑧 ) ∨ ( 𝐺 ‘ 𝑧 ) < ( 𝐺 ‘ 𝑦 ) ) → 𝑦 = 𝑧 ) )
33	21 32	sylbid	⊢ ( ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) → ( ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑧 ) → 𝑦 = 𝑧 ) )
34	33	rgen2	⊢ ∀ 𝑦 ∈ ω ∀ 𝑧 ∈ ω ( ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑧 ) → 𝑦 = 𝑧 )
35		dff13	⊢ ( 𝐺 : ω –1-1→ ( ℤ≥ ‘ 𝐶 ) ↔ ( 𝐺 : ω ⟶ ( ℤ≥ ‘ 𝐶 ) ∧ ∀ 𝑦 ∈ ω ∀ 𝑧 ∈ ω ( ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑧 ) → 𝑦 = 𝑧 ) ) )
36	9 34 35	mpbir2an	⊢ 𝐺 : ω –1-1→ ( ℤ≥ ‘ 𝐶 )
37		dff1o5	⊢ ( 𝐺 : ω –1-1-onto→ ( ℤ≥ ‘ 𝐶 ) ↔ ( 𝐺 : ω –1-1→ ( ℤ≥ ‘ 𝐶 ) ∧ ran 𝐺 = ( ℤ≥ ‘ 𝐶 ) ) )
38	36 6 37	mpbir2an	⊢ 𝐺 : ω –1-1-onto→ ( ℤ≥ ‘ 𝐶 )