This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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