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