Step | Hyp | Ref
| Expression |
1 | | frecuzrdgfn.3 |
. . . . . . . . 9
⊢ (φ → 𝑇 = ran 𝑅) |
2 | 1 | eleq2d 2104 |
. . . . . . . 8
⊢ (φ → (z ∈ 𝑇 ↔ z ∈ ran 𝑅)) |
3 | | frec2uz.1 |
. . . . . . . . . 10
⊢ (φ → 𝐶 ∈
ℤ) |
4 | | frec2uz.2 |
. . . . . . . . . 10
⊢ 𝐺 = frec((x ∈ ℤ
↦ (x + 1)), 𝐶) |
5 | | uzrdg.s |
. . . . . . . . . 10
⊢ (φ → 𝑆 ∈ 𝑉) |
6 | | uzrdg.a |
. . . . . . . . . 10
⊢ (φ → A ∈ 𝑆) |
7 | | uzrdg.f |
. . . . . . . . . 10
⊢ ((φ ∧
(x ∈
(ℤ≥‘𝐶) ∧
y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆) |
8 | | uzrdg.2 |
. . . . . . . . . 10
⊢ 𝑅 = frec((x ∈
(ℤ≥‘𝐶), y
∈ 𝑆 ↦ 〈(x + 1), (x𝐹y)〉), 〈𝐶, A〉) |
9 | 3, 4, 5, 6, 7, 8 | frecuzrdgrom 8877 |
. . . . . . . . 9
⊢ (φ → 𝑅 Fn 𝜔) |
10 | | fvelrnb 5164 |
. . . . . . . . 9
⊢ (𝑅 Fn 𝜔 → (z ∈ ran 𝑅 ↔ ∃w ∈ 𝜔 (𝑅‘w) = z)) |
11 | 9, 10 | syl 14 |
. . . . . . . 8
⊢ (φ → (z ∈ ran 𝑅 ↔ ∃w ∈ 𝜔 (𝑅‘w) = z)) |
12 | 2, 11 | bitrd 177 |
. . . . . . 7
⊢ (φ → (z ∈ 𝑇 ↔ ∃w ∈ 𝜔 (𝑅‘w) = z)) |
13 | 3, 4, 5, 6, 7, 8 | frecuzrdgrrn 8875 |
. . . . . . . . 9
⊢ ((φ ∧ w ∈ 𝜔)
→ (𝑅‘w) ∈
((ℤ≥‘𝐶) × 𝑆)) |
14 | | eleq1 2097 |
. . . . . . . . 9
⊢ ((𝑅‘w) = z →
((𝑅‘w) ∈
((ℤ≥‘𝐶) × 𝑆) ↔ z ∈
((ℤ≥‘𝐶) × 𝑆))) |
15 | 13, 14 | syl5ibcom 144 |
. . . . . . . 8
⊢ ((φ ∧ w ∈ 𝜔)
→ ((𝑅‘w) = z →
z ∈
((ℤ≥‘𝐶) × 𝑆))) |
16 | 15 | rexlimdva 2427 |
. . . . . . 7
⊢ (φ → (∃w ∈ 𝜔 (𝑅‘w) = z →
z ∈
((ℤ≥‘𝐶) × 𝑆))) |
17 | 12, 16 | sylbid 139 |
. . . . . 6
⊢ (φ → (z ∈ 𝑇 → z ∈
((ℤ≥‘𝐶) × 𝑆))) |
18 | 17 | ssrdv 2945 |
. . . . 5
⊢ (φ → 𝑇 ⊆
((ℤ≥‘𝐶) × 𝑆)) |
19 | | xpss 4389 |
. . . . 5
⊢
((ℤ≥‘𝐶) × 𝑆) ⊆ (V × V) |
20 | 18, 19 | syl6ss 2951 |
. . . 4
⊢ (φ → 𝑇 ⊆ (V × V)) |
21 | | df-rel 4295 |
. . . 4
⊢ (Rel
𝑇 ↔ 𝑇 ⊆ (V × V)) |
22 | 20, 21 | sylibr 137 |
. . 3
⊢ (φ → Rel 𝑇) |
23 | 3, 4 | frec2uzf1od 8873 |
. . . . . . . . . 10
⊢ (φ → 𝐺:𝜔–1-1-onto→(ℤ≥‘𝐶)) |
24 | | f1ocnvdm 5364 |
. . . . . . . . . 10
⊢ ((𝐺:𝜔–1-1-onto→(ℤ≥‘𝐶) ∧ v ∈ (ℤ≥‘𝐶)) → (◡𝐺‘v) ∈
𝜔) |
25 | 23, 24 | sylan 267 |
. . . . . . . . 9
⊢ ((φ ∧ v ∈
(ℤ≥‘𝐶)) → (◡𝐺‘v) ∈
𝜔) |
26 | 3, 4, 5, 6, 7, 8 | frecuzrdgrrn 8875 |
. . . . . . . . 9
⊢ ((φ ∧ (◡𝐺‘v) ∈ 𝜔)
→ (𝑅‘(◡𝐺‘v)) ∈
((ℤ≥‘𝐶) × 𝑆)) |
27 | 25, 26 | syldan 266 |
. . . . . . . 8
⊢ ((φ ∧ v ∈
(ℤ≥‘𝐶)) → (𝑅‘(◡𝐺‘v)) ∈
((ℤ≥‘𝐶) × 𝑆)) |
28 | | xp2nd 5735 |
. . . . . . . 8
⊢ ((𝑅‘(◡𝐺‘v)) ∈
((ℤ≥‘𝐶) × 𝑆) → (2nd ‘(𝑅‘(◡𝐺‘v))) ∈ 𝑆) |
29 | 27, 28 | syl 14 |
. . . . . . 7
⊢ ((φ ∧ v ∈
(ℤ≥‘𝐶)) → (2nd ‘(𝑅‘(◡𝐺‘v))) ∈ 𝑆) |
30 | 1 | eleq2d 2104 |
. . . . . . . . . . 11
⊢ (φ → (〈v, z〉 ∈ 𝑇 ↔ 〈v, z〉 ∈ ran 𝑅)) |
31 | | fvelrnb 5164 |
. . . . . . . . . . . 12
⊢ (𝑅 Fn 𝜔 →
(〈v, z〉 ∈ ran
𝑅 ↔ ∃w ∈ 𝜔 (𝑅‘w) = 〈v,
z〉)) |
32 | 9, 31 | syl 14 |
. . . . . . . . . . 11
⊢ (φ → (〈v, z〉 ∈ ran 𝑅 ↔ ∃w ∈ 𝜔 (𝑅‘w) = 〈v,
z〉)) |
33 | 30, 32 | bitrd 177 |
. . . . . . . . . 10
⊢ (φ → (〈v, z〉 ∈ 𝑇 ↔ ∃w ∈ 𝜔 (𝑅‘w) = 〈v,
z〉)) |
34 | 3 | adantr 261 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((φ ∧ w ∈ 𝜔)
→ 𝐶 ∈ ℤ) |
35 | 5 | adantr 261 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((φ ∧ w ∈ 𝜔)
→ 𝑆 ∈ 𝑉) |
36 | 6 | adantr 261 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((φ ∧ w ∈ 𝜔)
→ A ∈ 𝑆) |
37 | 7 | adantlr 446 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((φ ∧ w ∈ 𝜔)
∧ (x ∈ (ℤ≥‘𝐶) ∧
y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆) |
38 | | simpr 103 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((φ ∧ w ∈ 𝜔)
→ w ∈ 𝜔) |
39 | 34, 4, 35, 36, 37, 8, 38 | frec2uzrdg 8876 |
. . . . . . . . . . . . . . . . . 18
⊢ ((φ ∧ w ∈ 𝜔)
→ (𝑅‘w) = 〈(𝐺‘w), (2nd ‘(𝑅‘w))〉) |
40 | 39 | eqeq1d 2045 |
. . . . . . . . . . . . . . . . 17
⊢ ((φ ∧ w ∈ 𝜔)
→ ((𝑅‘w) = 〈v,
z〉 ↔ 〈(𝐺‘w), (2nd ‘(𝑅‘w))〉 = 〈v, z〉)) |
41 | | vex 2554 |
. . . . . . . . . . . . . . . . . . 19
⊢ v ∈
V |
42 | | vex 2554 |
. . . . . . . . . . . . . . . . . . 19
⊢ z ∈
V |
43 | 41, 42 | opth2 3968 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈(𝐺‘w), (2nd ‘(𝑅‘w))〉 = 〈v, z〉
↔ ((𝐺‘w) = v ∧ (2nd ‘(𝑅‘w)) = z)) |
44 | 43 | simplbi 259 |
. . . . . . . . . . . . . . . . 17
⊢
(〈(𝐺‘w), (2nd ‘(𝑅‘w))〉 = 〈v, z〉
→ (𝐺‘w) = v) |
45 | 40, 44 | syl6bi 152 |
. . . . . . . . . . . . . . . 16
⊢ ((φ ∧ w ∈ 𝜔)
→ ((𝑅‘w) = 〈v,
z〉 → (𝐺‘w) = v)) |
46 | | f1ocnvfv 5362 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺:𝜔–1-1-onto→(ℤ≥‘𝐶) ∧ w ∈ 𝜔) → ((𝐺‘w) = v →
(◡𝐺‘v) = w)) |
47 | 23, 46 | sylan 267 |
. . . . . . . . . . . . . . . 16
⊢ ((φ ∧ w ∈ 𝜔)
→ ((𝐺‘w) = v →
(◡𝐺‘v) = w)) |
48 | 45, 47 | syld 40 |
. . . . . . . . . . . . . . 15
⊢ ((φ ∧ w ∈ 𝜔)
→ ((𝑅‘w) = 〈v,
z〉 → (◡𝐺‘v) = w)) |
49 | | fveq2 5121 |
. . . . . . . . . . . . . . . 16
⊢ ((◡𝐺‘v) = w →
(𝑅‘(◡𝐺‘v)) = (𝑅‘w)) |
50 | 49 | fveq2d 5125 |
. . . . . . . . . . . . . . 15
⊢ ((◡𝐺‘v) = w →
(2nd ‘(𝑅‘(◡𝐺‘v))) = (2nd ‘(𝑅‘w))) |
51 | 48, 50 | syl6 29 |
. . . . . . . . . . . . . 14
⊢ ((φ ∧ w ∈ 𝜔)
→ ((𝑅‘w) = 〈v,
z〉 → (2nd
‘(𝑅‘(◡𝐺‘v))) = (2nd ‘(𝑅‘w)))) |
52 | 51 | imp 115 |
. . . . . . . . . . . . 13
⊢ (((φ ∧ w ∈ 𝜔)
∧ (𝑅‘w) = 〈v,
z〉) → (2nd
‘(𝑅‘(◡𝐺‘v))) = (2nd ‘(𝑅‘w))) |
53 | 41, 42 | op2ndd 5718 |
. . . . . . . . . . . . . 14
⊢ ((𝑅‘w) = 〈v,
z〉 → (2nd
‘(𝑅‘w)) = z) |
54 | 53 | adantl 262 |
. . . . . . . . . . . . 13
⊢ (((φ ∧ w ∈ 𝜔)
∧ (𝑅‘w) = 〈v,
z〉) → (2nd
‘(𝑅‘w)) = z) |
55 | 52, 54 | eqtr2d 2070 |
. . . . . . . . . . . 12
⊢ (((φ ∧ w ∈ 𝜔)
∧ (𝑅‘w) = 〈v,
z〉) → z = (2nd ‘(𝑅‘(◡𝐺‘v)))) |
56 | 55 | ex 108 |
. . . . . . . . . . 11
⊢ ((φ ∧ w ∈ 𝜔)
→ ((𝑅‘w) = 〈v,
z〉 → z = (2nd ‘(𝑅‘(◡𝐺‘v))))) |
57 | 56 | rexlimdva 2427 |
. . . . . . . . . 10
⊢ (φ → (∃w ∈ 𝜔 (𝑅‘w) = 〈v,
z〉 → z = (2nd ‘(𝑅‘(◡𝐺‘v))))) |
58 | 33, 57 | sylbid 139 |
. . . . . . . . 9
⊢ (φ → (〈v, z〉 ∈ 𝑇 → z = (2nd ‘(𝑅‘(◡𝐺‘v))))) |
59 | 58 | alrimiv 1751 |
. . . . . . . 8
⊢ (φ → ∀z(〈v,
z〉 ∈
𝑇 → z = (2nd ‘(𝑅‘(◡𝐺‘v))))) |
60 | 59 | adantr 261 |
. . . . . . 7
⊢ ((φ ∧ v ∈
(ℤ≥‘𝐶)) → ∀z(〈v,
z〉 ∈
𝑇 → z = (2nd ‘(𝑅‘(◡𝐺‘v))))) |
61 | | eqeq2 2046 |
. . . . . . . . . 10
⊢ (w = (2nd ‘(𝑅‘(◡𝐺‘v))) → (z =
w ↔ z = (2nd ‘(𝑅‘(◡𝐺‘v))))) |
62 | 61 | imbi2d 219 |
. . . . . . . . 9
⊢ (w = (2nd ‘(𝑅‘(◡𝐺‘v))) → ((〈v, z〉 ∈ 𝑇 → z = w) ↔
(〈v, z〉 ∈ 𝑇 → z = (2nd ‘(𝑅‘(◡𝐺‘v)))))) |
63 | 62 | albidv 1702 |
. . . . . . . 8
⊢ (w = (2nd ‘(𝑅‘(◡𝐺‘v))) → (∀z(〈v,
z〉 ∈
𝑇 → z = w) ↔
∀z(〈v,
z〉 ∈
𝑇 → z = (2nd ‘(𝑅‘(◡𝐺‘v)))))) |
64 | 63 | spcegv 2635 |
. . . . . . 7
⊢
((2nd ‘(𝑅‘(◡𝐺‘v))) ∈ 𝑆 → (∀z(〈v,
z〉 ∈
𝑇 → z = (2nd ‘(𝑅‘(◡𝐺‘v)))) → ∃w∀z(〈v,
z〉 ∈
𝑇 → z = w))) |
65 | 29, 60, 64 | sylc 56 |
. . . . . 6
⊢ ((φ ∧ v ∈
(ℤ≥‘𝐶)) → ∃w∀z(〈v,
z〉 ∈
𝑇 → z = w)) |
66 | | nfv 1418 |
. . . . . . 7
⊢
Ⅎw〈v, z〉 ∈ 𝑇 |
67 | 66 | mo2r 1949 |
. . . . . 6
⊢ (∃w∀z(〈v,
z〉 ∈
𝑇 → z = w) →
∃*z〈v,
z〉 ∈
𝑇) |
68 | 65, 67 | syl 14 |
. . . . 5
⊢ ((φ ∧ v ∈
(ℤ≥‘𝐶)) → ∃*z〈v,
z〉 ∈
𝑇) |
69 | | dmss 4477 |
. . . . . . . . . 10
⊢ (𝑇 ⊆
((ℤ≥‘𝐶) × 𝑆) → dom 𝑇 ⊆ dom
((ℤ≥‘𝐶) × 𝑆)) |
70 | 18, 69 | syl 14 |
. . . . . . . . 9
⊢ (φ → dom 𝑇 ⊆ dom
((ℤ≥‘𝐶) × 𝑆)) |
71 | | dmxpss 4696 |
. . . . . . . . 9
⊢ dom
((ℤ≥‘𝐶) × 𝑆) ⊆
(ℤ≥‘𝐶) |
72 | 70, 71 | syl6ss 2951 |
. . . . . . . 8
⊢ (φ → dom 𝑇 ⊆ (ℤ≥‘𝐶)) |
73 | 3 | adantr 261 |
. . . . . . . . . . . . 13
⊢ ((φ ∧ v ∈
(ℤ≥‘𝐶)) → 𝐶 ∈
ℤ) |
74 | 5 | adantr 261 |
. . . . . . . . . . . . 13
⊢ ((φ ∧ v ∈
(ℤ≥‘𝐶)) → 𝑆 ∈ 𝑉) |
75 | 6 | adantr 261 |
. . . . . . . . . . . . 13
⊢ ((φ ∧ v ∈
(ℤ≥‘𝐶)) → A ∈ 𝑆) |
76 | 7 | adantlr 446 |
. . . . . . . . . . . . 13
⊢ (((φ ∧ v ∈
(ℤ≥‘𝐶)) ∧
(x ∈
(ℤ≥‘𝐶) ∧
y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆) |
77 | | simpr 103 |
. . . . . . . . . . . . 13
⊢ ((φ ∧ v ∈
(ℤ≥‘𝐶)) → v ∈
(ℤ≥‘𝐶)) |
78 | 73, 4, 74, 75, 76, 8, 77 | frecuzrdglem 8878 |
. . . . . . . . . . . 12
⊢ ((φ ∧ v ∈
(ℤ≥‘𝐶)) → 〈v, (2nd ‘(𝑅‘(◡𝐺‘v)))〉 ∈ ran
𝑅) |
79 | 1 | eleq2d 2104 |
. . . . . . . . . . . . 13
⊢ (φ → (〈v, (2nd ‘(𝑅‘(◡𝐺‘v)))〉 ∈ 𝑇 ↔ 〈v, (2nd ‘(𝑅‘(◡𝐺‘v)))〉 ∈ ran
𝑅)) |
80 | 79 | adantr 261 |
. . . . . . . . . . . 12
⊢ ((φ ∧ v ∈
(ℤ≥‘𝐶)) → (〈v, (2nd ‘(𝑅‘(◡𝐺‘v)))〉 ∈ 𝑇 ↔ 〈v, (2nd ‘(𝑅‘(◡𝐺‘v)))〉 ∈ ran
𝑅)) |
81 | 78, 80 | mpbird 156 |
. . . . . . . . . . 11
⊢ ((φ ∧ v ∈
(ℤ≥‘𝐶)) → 〈v, (2nd ‘(𝑅‘(◡𝐺‘v)))〉 ∈ 𝑇) |
82 | | opeldmg 4483 |
. . . . . . . . . . . 12
⊢
((v ∈ V ∧
(2nd ‘(𝑅‘(◡𝐺‘v))) ∈ 𝑆) → (〈v, (2nd ‘(𝑅‘(◡𝐺‘v)))〉 ∈ 𝑇 → v ∈ dom 𝑇)) |
83 | 41, 82 | mpan 400 |
. . . . . . . . . . 11
⊢
((2nd ‘(𝑅‘(◡𝐺‘v))) ∈ 𝑆 → (〈v, (2nd ‘(𝑅‘(◡𝐺‘v)))〉 ∈ 𝑇 → v ∈ dom 𝑇)) |
84 | 29, 81, 83 | sylc 56 |
. . . . . . . . . 10
⊢ ((φ ∧ v ∈
(ℤ≥‘𝐶)) → v ∈ dom 𝑇) |
85 | 84 | ex 108 |
. . . . . . . . 9
⊢ (φ → (v ∈
(ℤ≥‘𝐶) → v ∈ dom 𝑇)) |
86 | 85 | ssrdv 2945 |
. . . . . . . 8
⊢ (φ → (ℤ≥‘𝐶) ⊆ dom 𝑇) |
87 | 72, 86 | eqssd 2956 |
. . . . . . 7
⊢ (φ → dom 𝑇 = (ℤ≥‘𝐶)) |
88 | 87 | eleq2d 2104 |
. . . . . 6
⊢ (φ → (v ∈ dom 𝑇 ↔ v ∈
(ℤ≥‘𝐶))) |
89 | 88 | pm5.32i 427 |
. . . . 5
⊢ ((φ ∧ v ∈ dom 𝑇) ↔ (φ ∧ v ∈
(ℤ≥‘𝐶))) |
90 | | df-br 3756 |
. . . . . 6
⊢ (v𝑇z ↔
〈v, z〉 ∈ 𝑇) |
91 | 90 | mobii 1934 |
. . . . 5
⊢ (∃*z v𝑇z ↔
∃*z〈v,
z〉 ∈
𝑇) |
92 | 68, 89, 91 | 3imtr4i 190 |
. . . 4
⊢ ((φ ∧ v ∈ dom 𝑇) → ∃*z v𝑇z) |
93 | 92 | ralrimiva 2386 |
. . 3
⊢ (φ → ∀v ∈ dom 𝑇∃*z v𝑇z) |
94 | | dffun7 4871 |
. . 3
⊢ (Fun
𝑇 ↔ (Rel 𝑇 ∧ ∀v ∈ dom 𝑇∃*z v𝑇z)) |
95 | 22, 93, 94 | sylanbrc 394 |
. 2
⊢ (φ → Fun 𝑇) |
96 | | df-fn 4848 |
. 2
⊢ (𝑇 Fn
(ℤ≥‘𝐶) ↔ (Fun 𝑇 ∧ dom
𝑇 =
(ℤ≥‘𝐶))) |
97 | 95, 87, 96 | sylanbrc 394 |
1
⊢ (φ → 𝑇 Fn (ℤ≥‘𝐶)) |