Step | Hyp | Ref
| Expression |
1 | | zex 8030 |
. . . . . . . . 9
⊢ ℤ
∈ V |
2 | 1 | mptex 5330 |
. . . . . . . 8
⊢ (x ∈ ℤ
↦ (x + 1)) ∈ V |
3 | | vex 2554 |
. . . . . . . 8
⊢ z ∈
V |
4 | 2, 3 | fvex 5138 |
. . . . . . 7
⊢
((x ∈ ℤ ↦ (x + 1))‘z)
∈ V |
5 | 4 | ax-gen 1335 |
. . . . . 6
⊢ ∀z((x ∈ ℤ
↦ (x + 1))‘z) ∈
V |
6 | | frec2uz.1 |
. . . . . 6
⊢ (φ → 𝐶 ∈
ℤ) |
7 | | frecfnom 5925 |
. . . . . 6
⊢ ((∀z((x ∈ ℤ
↦ (x + 1))‘z) ∈ V ∧ 𝐶 ∈
ℤ) → frec((x ∈ ℤ ↦ (x + 1)), 𝐶) Fn 𝜔) |
8 | 5, 6, 7 | sylancr 393 |
. . . . 5
⊢ (φ → frec((x ∈ ℤ
↦ (x + 1)), 𝐶) Fn 𝜔) |
9 | | frec2uz.2 |
. . . . . 6
⊢ 𝐺 = frec((x ∈ ℤ
↦ (x + 1)), 𝐶) |
10 | 9 | fneq1i 4936 |
. . . . 5
⊢ (𝐺 Fn 𝜔 ↔
frec((x ∈
ℤ ↦ (x + 1)), 𝐶) Fn 𝜔) |
11 | 8, 10 | sylibr 137 |
. . . 4
⊢ (φ → 𝐺 Fn 𝜔) |
12 | 6, 9 | frec2uzrand 8872 |
. . . . 5
⊢ (φ → ran 𝐺 = (ℤ≥‘𝐶)) |
13 | | eqimss 2991 |
. . . . 5
⊢ (ran
𝐺 =
(ℤ≥‘𝐶) → ran 𝐺 ⊆ (ℤ≥‘𝐶)) |
14 | 12, 13 | syl 14 |
. . . 4
⊢ (φ → ran 𝐺 ⊆ (ℤ≥‘𝐶)) |
15 | | df-f 4849 |
. . . 4
⊢ (𝐺:𝜔⟶(ℤ≥‘𝐶) ↔ (𝐺 Fn 𝜔 ∧ ran
𝐺 ⊆
(ℤ≥‘𝐶))) |
16 | 11, 14, 15 | sylanbrc 394 |
. . 3
⊢ (φ → 𝐺:𝜔⟶(ℤ≥‘𝐶)) |
17 | 6 | adantr 261 |
. . . . . . . . . . . . . 14
⊢ ((φ ∧ y ∈ 𝜔)
→ 𝐶 ∈ ℤ) |
18 | | simpr 103 |
. . . . . . . . . . . . . 14
⊢ ((φ ∧ y ∈ 𝜔)
→ y ∈ 𝜔) |
19 | 17, 9, 18 | frec2uzzd 8867 |
. . . . . . . . . . . . 13
⊢ ((φ ∧ y ∈ 𝜔)
→ (𝐺‘y) ∈
ℤ) |
20 | 19 | 3adant3 923 |
. . . . . . . . . . . 12
⊢ ((φ ∧ y ∈ 𝜔
∧ z ∈ 𝜔) → (𝐺‘y) ∈
ℤ) |
21 | 20 | zred 8136 |
. . . . . . . . . . 11
⊢ ((φ ∧ y ∈ 𝜔
∧ z ∈ 𝜔) → (𝐺‘y) ∈
ℝ) |
22 | 21 | ltnrd 6926 |
. . . . . . . . . 10
⊢ ((φ ∧ y ∈ 𝜔
∧ z ∈ 𝜔) → ¬ (𝐺‘y) < (𝐺‘y)) |
23 | 22 | adantr 261 |
. . . . . . . . 9
⊢ (((φ ∧ y ∈ 𝜔
∧ z ∈ 𝜔) ∧
(𝐺‘y) = (𝐺‘z)) → ¬ (𝐺‘y) < (𝐺‘y)) |
24 | | simpr 103 |
. . . . . . . . . 10
⊢ (((φ ∧ y ∈ 𝜔
∧ z ∈ 𝜔) ∧
(𝐺‘y) = (𝐺‘z)) → (𝐺‘y) = (𝐺‘z)) |
25 | 24 | breq2d 3767 |
. . . . . . . . 9
⊢ (((φ ∧ y ∈ 𝜔
∧ z ∈ 𝜔) ∧
(𝐺‘y) = (𝐺‘z)) → ((𝐺‘y) < (𝐺‘y) ↔ (𝐺‘y) < (𝐺‘z))) |
26 | 23, 25 | mtbid 596 |
. . . . . . . 8
⊢ (((φ ∧ y ∈ 𝜔
∧ z ∈ 𝜔) ∧
(𝐺‘y) = (𝐺‘z)) → ¬ (𝐺‘y) < (𝐺‘z)) |
27 | 17 | 3adant3 923 |
. . . . . . . . . . 11
⊢ ((φ ∧ y ∈ 𝜔
∧ z ∈ 𝜔) → 𝐶 ∈
ℤ) |
28 | | simp2 904 |
. . . . . . . . . . 11
⊢ ((φ ∧ y ∈ 𝜔
∧ z ∈ 𝜔) → y ∈
𝜔) |
29 | | simp3 905 |
. . . . . . . . . . 11
⊢ ((φ ∧ y ∈ 𝜔
∧ z ∈ 𝜔) → z ∈
𝜔) |
30 | 27, 9, 28, 29 | frec2uzltd 8870 |
. . . . . . . . . 10
⊢ ((φ ∧ y ∈ 𝜔
∧ z ∈ 𝜔) → (y ∈ z → (𝐺‘y) < (𝐺‘z))) |
31 | 30 | con3d 560 |
. . . . . . . . 9
⊢ ((φ ∧ y ∈ 𝜔
∧ z ∈ 𝜔) → (¬ (𝐺‘y) < (𝐺‘z) → ¬ y ∈ z)) |
32 | 31 | adantr 261 |
. . . . . . . 8
⊢ (((φ ∧ y ∈ 𝜔
∧ z ∈ 𝜔) ∧
(𝐺‘y) = (𝐺‘z)) → (¬ (𝐺‘y) < (𝐺‘z) → ¬ y ∈ z)) |
33 | 26, 32 | mpd 13 |
. . . . . . 7
⊢ (((φ ∧ y ∈ 𝜔
∧ z ∈ 𝜔) ∧
(𝐺‘y) = (𝐺‘z)) → ¬ y ∈ z) |
34 | 24 | breq1d 3765 |
. . . . . . . . 9
⊢ (((φ ∧ y ∈ 𝜔
∧ z ∈ 𝜔) ∧
(𝐺‘y) = (𝐺‘z)) → ((𝐺‘y) < (𝐺‘y) ↔ (𝐺‘z) < (𝐺‘y))) |
35 | 23, 34 | mtbid 596 |
. . . . . . . 8
⊢ (((φ ∧ y ∈ 𝜔
∧ z ∈ 𝜔) ∧
(𝐺‘y) = (𝐺‘z)) → ¬ (𝐺‘z) < (𝐺‘y)) |
36 | 27, 9, 29, 28 | frec2uzltd 8870 |
. . . . . . . . 9
⊢ ((φ ∧ y ∈ 𝜔
∧ z ∈ 𝜔) → (z ∈ y → (𝐺‘z) < (𝐺‘y))) |
37 | 36 | adantr 261 |
. . . . . . . 8
⊢ (((φ ∧ y ∈ 𝜔
∧ z ∈ 𝜔) ∧
(𝐺‘y) = (𝐺‘z)) → (z
∈ y
→ (𝐺‘z) < (𝐺‘y))) |
38 | 35, 37 | mtod 588 |
. . . . . . 7
⊢ (((φ ∧ y ∈ 𝜔
∧ z ∈ 𝜔) ∧
(𝐺‘y) = (𝐺‘z)) → ¬ z ∈ y) |
39 | | nntri3 6014 |
. . . . . . . . 9
⊢
((y ∈ 𝜔 ∧
z ∈
𝜔) → (y = z ↔ (¬ y ∈ z ∧ ¬ z ∈ y))) |
40 | 39 | 3adant1 921 |
. . . . . . . 8
⊢ ((φ ∧ y ∈ 𝜔
∧ z ∈ 𝜔) → (y = z ↔
(¬ y ∈ z ∧ ¬ z ∈ y))) |
41 | 40 | adantr 261 |
. . . . . . 7
⊢ (((φ ∧ y ∈ 𝜔
∧ z ∈ 𝜔) ∧
(𝐺‘y) = (𝐺‘z)) → (y =
z ↔ (¬ y ∈ z ∧ ¬ z ∈ y))) |
42 | 33, 38, 41 | mpbir2and 850 |
. . . . . 6
⊢ (((φ ∧ y ∈ 𝜔
∧ z ∈ 𝜔) ∧
(𝐺‘y) = (𝐺‘z)) → y =
z) |
43 | 42 | ex 108 |
. . . . 5
⊢ ((φ ∧ y ∈ 𝜔
∧ z ∈ 𝜔) → ((𝐺‘y) = (𝐺‘z) → y =
z)) |
44 | 43 | 3expb 1104 |
. . . 4
⊢ ((φ ∧
(y ∈
𝜔 ∧ z ∈ 𝜔))
→ ((𝐺‘y) = (𝐺‘z) → y =
z)) |
45 | 44 | ralrimivva 2395 |
. . 3
⊢ (φ → ∀y ∈ 𝜔 ∀z ∈ 𝜔 ((𝐺‘y) = (𝐺‘z) → y =
z)) |
46 | | dff13 5350 |
. . 3
⊢ (𝐺:𝜔–1-1→(ℤ≥‘𝐶) ↔ (𝐺:𝜔⟶(ℤ≥‘𝐶) ∧
∀y ∈ 𝜔 ∀z ∈ 𝜔 ((𝐺‘y) = (𝐺‘z) →
y = z))) |
47 | 16, 45, 46 | sylanbrc 394 |
. 2
⊢ (φ → 𝐺:𝜔–1-1→(ℤ≥‘𝐶)) |
48 | | dff1o5 5078 |
. 2
⊢ (𝐺:𝜔–1-1-onto→(ℤ≥‘𝐶) ↔ (𝐺:𝜔–1-1→(ℤ≥‘𝐶) ∧ ran
𝐺 =
(ℤ≥‘𝐶))) |
49 | 47, 12, 48 | sylanbrc 394 |
1
⊢ (φ → 𝐺:𝜔–1-1-onto→(ℤ≥‘𝐶)) |