Step | Hyp | Ref
| Expression |
1 | | frecuzrdgfn.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 = ran 𝑅) |
2 | 1 | eleq2d 2107 |
. . . . . . . 8
⊢ (𝜑 → (𝑧 ∈ 𝑇 ↔ 𝑧 ∈ ran 𝑅)) |
3 | | frec2uz.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ ℤ) |
4 | | frec2uz.2 |
. . . . . . . . . 10
⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 𝐶) |
5 | | uzrdg.s |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ 𝑉) |
6 | | uzrdg.a |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ 𝑆) |
7 | | uzrdg.f |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝐶) ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆) |
8 | | uzrdg.2 |
. . . . . . . . . 10
⊢ 𝑅 = frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) |
9 | 3, 4, 5, 6, 7, 8 | frecuzrdgrom 9196 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 Fn ω) |
10 | | fvelrnb 5221 |
. . . . . . . . 9
⊢ (𝑅 Fn ω → (𝑧 ∈ ran 𝑅 ↔ ∃𝑤 ∈ ω (𝑅‘𝑤) = 𝑧)) |
11 | 9, 10 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → (𝑧 ∈ ran 𝑅 ↔ ∃𝑤 ∈ ω (𝑅‘𝑤) = 𝑧)) |
12 | 2, 11 | bitrd 177 |
. . . . . . 7
⊢ (𝜑 → (𝑧 ∈ 𝑇 ↔ ∃𝑤 ∈ ω (𝑅‘𝑤) = 𝑧)) |
13 | 3, 4, 5, 6, 7, 8 | frecuzrdgrrn 9194 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ ω) → (𝑅‘𝑤) ∈ ((ℤ≥‘𝐶) × 𝑆)) |
14 | | eleq1 2100 |
. . . . . . . . 9
⊢ ((𝑅‘𝑤) = 𝑧 → ((𝑅‘𝑤) ∈ ((ℤ≥‘𝐶) × 𝑆) ↔ 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆))) |
15 | 13, 14 | syl5ibcom 144 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ ω) → ((𝑅‘𝑤) = 𝑧 → 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆))) |
16 | 15 | rexlimdva 2433 |
. . . . . . 7
⊢ (𝜑 → (∃𝑤 ∈ ω (𝑅‘𝑤) = 𝑧 → 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆))) |
17 | 12, 16 | sylbid 139 |
. . . . . 6
⊢ (𝜑 → (𝑧 ∈ 𝑇 → 𝑧 ∈ ((ℤ≥‘𝐶) × 𝑆))) |
18 | 17 | ssrdv 2951 |
. . . . 5
⊢ (𝜑 → 𝑇 ⊆
((ℤ≥‘𝐶) × 𝑆)) |
19 | | xpss 4446 |
. . . . 5
⊢
((ℤ≥‘𝐶) × 𝑆) ⊆ (V × V) |
20 | 18, 19 | syl6ss 2957 |
. . . 4
⊢ (𝜑 → 𝑇 ⊆ (V × V)) |
21 | | df-rel 4352 |
. . . 4
⊢ (Rel
𝑇 ↔ 𝑇 ⊆ (V × V)) |
22 | 20, 21 | sylibr 137 |
. . 3
⊢ (𝜑 → Rel 𝑇) |
23 | 3, 4 | frec2uzf1od 9192 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺:ω–1-1-onto→(ℤ≥‘𝐶)) |
24 | | f1ocnvdm 5421 |
. . . . . . . . . 10
⊢ ((𝐺:ω–1-1-onto→(ℤ≥‘𝐶) ∧ 𝑣 ∈ (ℤ≥‘𝐶)) → (◡𝐺‘𝑣) ∈ ω) |
25 | 23, 24 | sylan 267 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ (ℤ≥‘𝐶)) → (◡𝐺‘𝑣) ∈ ω) |
26 | 3, 4, 5, 6, 7, 8 | frecuzrdgrrn 9194 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (◡𝐺‘𝑣) ∈ ω) → (𝑅‘(◡𝐺‘𝑣)) ∈
((ℤ≥‘𝐶) × 𝑆)) |
27 | 25, 26 | syldan 266 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑣 ∈ (ℤ≥‘𝐶)) → (𝑅‘(◡𝐺‘𝑣)) ∈
((ℤ≥‘𝐶) × 𝑆)) |
28 | | xp2nd 5793 |
. . . . . . . 8
⊢ ((𝑅‘(◡𝐺‘𝑣)) ∈
((ℤ≥‘𝐶) × 𝑆) → (2nd ‘(𝑅‘(◡𝐺‘𝑣))) ∈ 𝑆) |
29 | 27, 28 | syl 14 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ (ℤ≥‘𝐶)) → (2nd
‘(𝑅‘(◡𝐺‘𝑣))) ∈ 𝑆) |
30 | 1 | eleq2d 2107 |
. . . . . . . . . . 11
⊢ (𝜑 → (〈𝑣, 𝑧〉 ∈ 𝑇 ↔ 〈𝑣, 𝑧〉 ∈ ran 𝑅)) |
31 | | fvelrnb 5221 |
. . . . . . . . . . . 12
⊢ (𝑅 Fn ω → (〈𝑣, 𝑧〉 ∈ ran 𝑅 ↔ ∃𝑤 ∈ ω (𝑅‘𝑤) = 〈𝑣, 𝑧〉)) |
32 | 9, 31 | syl 14 |
. . . . . . . . . . 11
⊢ (𝜑 → (〈𝑣, 𝑧〉 ∈ ran 𝑅 ↔ ∃𝑤 ∈ ω (𝑅‘𝑤) = 〈𝑣, 𝑧〉)) |
33 | 30, 32 | bitrd 177 |
. . . . . . . . . 10
⊢ (𝜑 → (〈𝑣, 𝑧〉 ∈ 𝑇 ↔ ∃𝑤 ∈ ω (𝑅‘𝑤) = 〈𝑣, 𝑧〉)) |
34 | 3 | adantr 261 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ ω) → 𝐶 ∈ ℤ) |
35 | 5 | adantr 261 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ ω) → 𝑆 ∈ 𝑉) |
36 | 6 | adantr 261 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ ω) → 𝐴 ∈ 𝑆) |
37 | 7 | adantlr 446 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑤 ∈ ω) ∧ (𝑥 ∈ (ℤ≥‘𝐶) ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆) |
38 | | simpr 103 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ ω) → 𝑤 ∈ ω) |
39 | 34, 4, 35, 36, 37, 8, 38 | frec2uzrdg 9195 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ ω) → (𝑅‘𝑤) = 〈(𝐺‘𝑤), (2nd ‘(𝑅‘𝑤))〉) |
40 | 39 | eqeq1d 2048 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ ω) → ((𝑅‘𝑤) = 〈𝑣, 𝑧〉 ↔ 〈(𝐺‘𝑤), (2nd ‘(𝑅‘𝑤))〉 = 〈𝑣, 𝑧〉)) |
41 | | vex 2560 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑣 ∈ V |
42 | | vex 2560 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑧 ∈ V |
43 | 41, 42 | opth2 3977 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈(𝐺‘𝑤), (2nd ‘(𝑅‘𝑤))〉 = 〈𝑣, 𝑧〉 ↔ ((𝐺‘𝑤) = 𝑣 ∧ (2nd ‘(𝑅‘𝑤)) = 𝑧)) |
44 | 43 | simplbi 259 |
. . . . . . . . . . . . . . . . 17
⊢
(〈(𝐺‘𝑤), (2nd ‘(𝑅‘𝑤))〉 = 〈𝑣, 𝑧〉 → (𝐺‘𝑤) = 𝑣) |
45 | 40, 44 | syl6bi 152 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ ω) → ((𝑅‘𝑤) = 〈𝑣, 𝑧〉 → (𝐺‘𝑤) = 𝑣)) |
46 | | f1ocnvfv 5419 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺:ω–1-1-onto→(ℤ≥‘𝐶) ∧ 𝑤 ∈ ω) → ((𝐺‘𝑤) = 𝑣 → (◡𝐺‘𝑣) = 𝑤)) |
47 | 23, 46 | sylan 267 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ ω) → ((𝐺‘𝑤) = 𝑣 → (◡𝐺‘𝑣) = 𝑤)) |
48 | 45, 47 | syld 40 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ ω) → ((𝑅‘𝑤) = 〈𝑣, 𝑧〉 → (◡𝐺‘𝑣) = 𝑤)) |
49 | | fveq2 5178 |
. . . . . . . . . . . . . . . 16
⊢ ((◡𝐺‘𝑣) = 𝑤 → (𝑅‘(◡𝐺‘𝑣)) = (𝑅‘𝑤)) |
50 | 49 | fveq2d 5182 |
. . . . . . . . . . . . . . 15
⊢ ((◡𝐺‘𝑣) = 𝑤 → (2nd ‘(𝑅‘(◡𝐺‘𝑣))) = (2nd ‘(𝑅‘𝑤))) |
51 | 48, 50 | syl6 29 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ ω) → ((𝑅‘𝑤) = 〈𝑣, 𝑧〉 → (2nd ‘(𝑅‘(◡𝐺‘𝑣))) = (2nd ‘(𝑅‘𝑤)))) |
52 | 51 | imp 115 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ ω) ∧ (𝑅‘𝑤) = 〈𝑣, 𝑧〉) → (2nd ‘(𝑅‘(◡𝐺‘𝑣))) = (2nd ‘(𝑅‘𝑤))) |
53 | 41, 42 | op2ndd 5776 |
. . . . . . . . . . . . . 14
⊢ ((𝑅‘𝑤) = 〈𝑣, 𝑧〉 → (2nd ‘(𝑅‘𝑤)) = 𝑧) |
54 | 53 | adantl 262 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ ω) ∧ (𝑅‘𝑤) = 〈𝑣, 𝑧〉) → (2nd ‘(𝑅‘𝑤)) = 𝑧) |
55 | 52, 54 | eqtr2d 2073 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ ω) ∧ (𝑅‘𝑤) = 〈𝑣, 𝑧〉) → 𝑧 = (2nd ‘(𝑅‘(◡𝐺‘𝑣)))) |
56 | 55 | ex 108 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ ω) → ((𝑅‘𝑤) = 〈𝑣, 𝑧〉 → 𝑧 = (2nd ‘(𝑅‘(◡𝐺‘𝑣))))) |
57 | 56 | rexlimdva 2433 |
. . . . . . . . . 10
⊢ (𝜑 → (∃𝑤 ∈ ω (𝑅‘𝑤) = 〈𝑣, 𝑧〉 → 𝑧 = (2nd ‘(𝑅‘(◡𝐺‘𝑣))))) |
58 | 33, 57 | sylbid 139 |
. . . . . . . . 9
⊢ (𝜑 → (〈𝑣, 𝑧〉 ∈ 𝑇 → 𝑧 = (2nd ‘(𝑅‘(◡𝐺‘𝑣))))) |
59 | 58 | alrimiv 1754 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑧(〈𝑣, 𝑧〉 ∈ 𝑇 → 𝑧 = (2nd ‘(𝑅‘(◡𝐺‘𝑣))))) |
60 | 59 | adantr 261 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ (ℤ≥‘𝐶)) → ∀𝑧(〈𝑣, 𝑧〉 ∈ 𝑇 → 𝑧 = (2nd ‘(𝑅‘(◡𝐺‘𝑣))))) |
61 | | eqeq2 2049 |
. . . . . . . . . 10
⊢ (𝑤 = (2nd ‘(𝑅‘(◡𝐺‘𝑣))) → (𝑧 = 𝑤 ↔ 𝑧 = (2nd ‘(𝑅‘(◡𝐺‘𝑣))))) |
62 | 61 | imbi2d 219 |
. . . . . . . . 9
⊢ (𝑤 = (2nd ‘(𝑅‘(◡𝐺‘𝑣))) → ((〈𝑣, 𝑧〉 ∈ 𝑇 → 𝑧 = 𝑤) ↔ (〈𝑣, 𝑧〉 ∈ 𝑇 → 𝑧 = (2nd ‘(𝑅‘(◡𝐺‘𝑣)))))) |
63 | 62 | albidv 1705 |
. . . . . . . 8
⊢ (𝑤 = (2nd ‘(𝑅‘(◡𝐺‘𝑣))) → (∀𝑧(〈𝑣, 𝑧〉 ∈ 𝑇 → 𝑧 = 𝑤) ↔ ∀𝑧(〈𝑣, 𝑧〉 ∈ 𝑇 → 𝑧 = (2nd ‘(𝑅‘(◡𝐺‘𝑣)))))) |
64 | 63 | spcegv 2641 |
. . . . . . 7
⊢
((2nd ‘(𝑅‘(◡𝐺‘𝑣))) ∈ 𝑆 → (∀𝑧(〈𝑣, 𝑧〉 ∈ 𝑇 → 𝑧 = (2nd ‘(𝑅‘(◡𝐺‘𝑣)))) → ∃𝑤∀𝑧(〈𝑣, 𝑧〉 ∈ 𝑇 → 𝑧 = 𝑤))) |
65 | 29, 60, 64 | sylc 56 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ (ℤ≥‘𝐶)) → ∃𝑤∀𝑧(〈𝑣, 𝑧〉 ∈ 𝑇 → 𝑧 = 𝑤)) |
66 | | nfv 1421 |
. . . . . . 7
⊢
Ⅎ𝑤〈𝑣, 𝑧〉 ∈ 𝑇 |
67 | 66 | mo2r 1952 |
. . . . . 6
⊢
(∃𝑤∀𝑧(〈𝑣, 𝑧〉 ∈ 𝑇 → 𝑧 = 𝑤) → ∃*𝑧〈𝑣, 𝑧〉 ∈ 𝑇) |
68 | 65, 67 | syl 14 |
. . . . 5
⊢ ((𝜑 ∧ 𝑣 ∈ (ℤ≥‘𝐶)) → ∃*𝑧〈𝑣, 𝑧〉 ∈ 𝑇) |
69 | | dmss 4534 |
. . . . . . . . . 10
⊢ (𝑇 ⊆
((ℤ≥‘𝐶) × 𝑆) → dom 𝑇 ⊆ dom
((ℤ≥‘𝐶) × 𝑆)) |
70 | 18, 69 | syl 14 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝑇 ⊆ dom
((ℤ≥‘𝐶) × 𝑆)) |
71 | | dmxpss 4753 |
. . . . . . . . 9
⊢ dom
((ℤ≥‘𝐶) × 𝑆) ⊆
(ℤ≥‘𝐶) |
72 | 70, 71 | syl6ss 2957 |
. . . . . . . 8
⊢ (𝜑 → dom 𝑇 ⊆ (ℤ≥‘𝐶)) |
73 | 3 | adantr 261 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ (ℤ≥‘𝐶)) → 𝐶 ∈ ℤ) |
74 | 5 | adantr 261 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ (ℤ≥‘𝐶)) → 𝑆 ∈ 𝑉) |
75 | 6 | adantr 261 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ (ℤ≥‘𝐶)) → 𝐴 ∈ 𝑆) |
76 | 7 | adantlr 446 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑣 ∈ (ℤ≥‘𝐶)) ∧ (𝑥 ∈ (ℤ≥‘𝐶) ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆) |
77 | | simpr 103 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ (ℤ≥‘𝐶)) → 𝑣 ∈ (ℤ≥‘𝐶)) |
78 | 73, 4, 74, 75, 76, 8, 77 | frecuzrdglem 9197 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ (ℤ≥‘𝐶)) → 〈𝑣, (2nd ‘(𝑅‘(◡𝐺‘𝑣)))〉 ∈ ran 𝑅) |
79 | 1 | eleq2d 2107 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (〈𝑣, (2nd ‘(𝑅‘(◡𝐺‘𝑣)))〉 ∈ 𝑇 ↔ 〈𝑣, (2nd ‘(𝑅‘(◡𝐺‘𝑣)))〉 ∈ ran 𝑅)) |
80 | 79 | adantr 261 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ (ℤ≥‘𝐶)) → (〈𝑣, (2nd ‘(𝑅‘(◡𝐺‘𝑣)))〉 ∈ 𝑇 ↔ 〈𝑣, (2nd ‘(𝑅‘(◡𝐺‘𝑣)))〉 ∈ ran 𝑅)) |
81 | 78, 80 | mpbird 156 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ (ℤ≥‘𝐶)) → 〈𝑣, (2nd ‘(𝑅‘(◡𝐺‘𝑣)))〉 ∈ 𝑇) |
82 | | opeldmg 4540 |
. . . . . . . . . . . 12
⊢ ((𝑣 ∈ V ∧ (2nd
‘(𝑅‘(◡𝐺‘𝑣))) ∈ 𝑆) → (〈𝑣, (2nd ‘(𝑅‘(◡𝐺‘𝑣)))〉 ∈ 𝑇 → 𝑣 ∈ dom 𝑇)) |
83 | 41, 82 | mpan 400 |
. . . . . . . . . . 11
⊢
((2nd ‘(𝑅‘(◡𝐺‘𝑣))) ∈ 𝑆 → (〈𝑣, (2nd ‘(𝑅‘(◡𝐺‘𝑣)))〉 ∈ 𝑇 → 𝑣 ∈ dom 𝑇)) |
84 | 29, 81, 83 | sylc 56 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ (ℤ≥‘𝐶)) → 𝑣 ∈ dom 𝑇) |
85 | 84 | ex 108 |
. . . . . . . . 9
⊢ (𝜑 → (𝑣 ∈ (ℤ≥‘𝐶) → 𝑣 ∈ dom 𝑇)) |
86 | 85 | ssrdv 2951 |
. . . . . . . 8
⊢ (𝜑 →
(ℤ≥‘𝐶) ⊆ dom 𝑇) |
87 | 72, 86 | eqssd 2962 |
. . . . . . 7
⊢ (𝜑 → dom 𝑇 = (ℤ≥‘𝐶)) |
88 | 87 | eleq2d 2107 |
. . . . . 6
⊢ (𝜑 → (𝑣 ∈ dom 𝑇 ↔ 𝑣 ∈ (ℤ≥‘𝐶))) |
89 | 88 | pm5.32i 427 |
. . . . 5
⊢ ((𝜑 ∧ 𝑣 ∈ dom 𝑇) ↔ (𝜑 ∧ 𝑣 ∈ (ℤ≥‘𝐶))) |
90 | | df-br 3765 |
. . . . . 6
⊢ (𝑣𝑇𝑧 ↔ 〈𝑣, 𝑧〉 ∈ 𝑇) |
91 | 90 | mobii 1937 |
. . . . 5
⊢
(∃*𝑧 𝑣𝑇𝑧 ↔ ∃*𝑧〈𝑣, 𝑧〉 ∈ 𝑇) |
92 | 68, 89, 91 | 3imtr4i 190 |
. . . 4
⊢ ((𝜑 ∧ 𝑣 ∈ dom 𝑇) → ∃*𝑧 𝑣𝑇𝑧) |
93 | 92 | ralrimiva 2392 |
. . 3
⊢ (𝜑 → ∀𝑣 ∈ dom 𝑇∃*𝑧 𝑣𝑇𝑧) |
94 | | dffun7 4928 |
. . 3
⊢ (Fun
𝑇 ↔ (Rel 𝑇 ∧ ∀𝑣 ∈ dom 𝑇∃*𝑧 𝑣𝑇𝑧)) |
95 | 22, 93, 94 | sylanbrc 394 |
. 2
⊢ (𝜑 → Fun 𝑇) |
96 | | df-fn 4905 |
. 2
⊢ (𝑇 Fn
(ℤ≥‘𝐶) ↔ (Fun 𝑇 ∧ dom 𝑇 = (ℤ≥‘𝐶))) |
97 | 95, 87, 96 | sylanbrc 394 |
1
⊢ (𝜑 → 𝑇 Fn (ℤ≥‘𝐶)) |