Metamath Proof Explorer


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→ ( ℤ𝐶 )