Step | Hyp | Ref
| Expression |
1 | | uzrdg.3 |
. . . . . . . . 9
⊢ 𝑆 = ran 𝑅 |
2 | 1 | eleq2i 2832 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝑆 ↔ 𝑧 ∈ ran 𝑅) |
3 | | frfnom 8257 |
. . . . . . . . . 10
⊢
(rec((𝑥 ∈ V,
𝑦 ∈ V ↦
〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω) Fn
ω |
4 | | uzrdg.2 |
. . . . . . . . . . 11
⊢ 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω) |
5 | 4 | fneq1i 6528 |
. . . . . . . . . 10
⊢ (𝑅 Fn ω ↔ (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω) Fn
ω) |
6 | 3, 5 | mpbir 230 |
. . . . . . . . 9
⊢ 𝑅 Fn ω |
7 | | fvelrnb 6827 |
. . . . . . . . 9
⊢ (𝑅 Fn ω → (𝑧 ∈ ran 𝑅 ↔ ∃𝑤 ∈ ω (𝑅‘𝑤) = 𝑧)) |
8 | 6, 7 | ax-mp 5 |
. . . . . . . 8
⊢ (𝑧 ∈ ran 𝑅 ↔ ∃𝑤 ∈ ω (𝑅‘𝑤) = 𝑧) |
9 | 2, 8 | bitri 274 |
. . . . . . 7
⊢ (𝑧 ∈ 𝑆 ↔ ∃𝑤 ∈ ω (𝑅‘𝑤) = 𝑧) |
10 | | om2uz.1 |
. . . . . . . . . . 11
⊢ 𝐶 ∈ ℤ |
11 | | om2uz.2 |
. . . . . . . . . . 11
⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐶) ↾ ω) |
12 | | uzrdg.1 |
. . . . . . . . . . 11
⊢ 𝐴 ∈ V |
13 | 10, 11, 12, 4 | om2uzrdg 13674 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ω → (𝑅‘𝑤) = 〈(𝐺‘𝑤), (2nd ‘(𝑅‘𝑤))〉) |
14 | 10, 11 | om2uzuzi 13667 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ω → (𝐺‘𝑤) ∈ (ℤ≥‘𝐶)) |
15 | | fvex 6784 |
. . . . . . . . . . 11
⊢
(2nd ‘(𝑅‘𝑤)) ∈ V |
16 | | opelxpi 5627 |
. . . . . . . . . . 11
⊢ (((𝐺‘𝑤) ∈ (ℤ≥‘𝐶) ∧ (2nd
‘(𝑅‘𝑤)) ∈ V) → 〈(𝐺‘𝑤), (2nd ‘(𝑅‘𝑤))〉 ∈
((ℤ≥‘𝐶) × V)) |
17 | 14, 15, 16 | sylancl 586 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ω →
〈(𝐺‘𝑤), (2nd ‘(𝑅‘𝑤))〉 ∈
((ℤ≥‘𝐶) × V)) |
18 | 13, 17 | eqeltrd 2841 |
. . . . . . . . 9
⊢ (𝑤 ∈ ω → (𝑅‘𝑤) ∈ ((ℤ≥‘𝐶) × V)) |
19 | | eleq1 2828 |
. . . . . . . . 9
⊢ ((𝑅‘𝑤) = 𝑧 → ((𝑅‘𝑤) ∈ ((ℤ≥‘𝐶) × V) ↔ 𝑧 ∈
((ℤ≥‘𝐶) × V))) |
20 | 18, 19 | syl5ibcom 244 |
. . . . . . . 8
⊢ (𝑤 ∈ ω → ((𝑅‘𝑤) = 𝑧 → 𝑧 ∈ ((ℤ≥‘𝐶) × V))) |
21 | 20 | rexlimiv 3211 |
. . . . . . 7
⊢
(∃𝑤 ∈
ω (𝑅‘𝑤) = 𝑧 → 𝑧 ∈ ((ℤ≥‘𝐶) × V)) |
22 | 9, 21 | sylbi 216 |
. . . . . 6
⊢ (𝑧 ∈ 𝑆 → 𝑧 ∈ ((ℤ≥‘𝐶) × V)) |
23 | 22 | ssriv 3930 |
. . . . 5
⊢ 𝑆 ⊆
((ℤ≥‘𝐶) × V) |
24 | | xpss 5606 |
. . . . 5
⊢
((ℤ≥‘𝐶) × V) ⊆ (V ×
V) |
25 | 23, 24 | sstri 3935 |
. . . 4
⊢ 𝑆 ⊆ (V ×
V) |
26 | | df-rel 5597 |
. . . 4
⊢ (Rel
𝑆 ↔ 𝑆 ⊆ (V × V)) |
27 | 25, 26 | mpbir 230 |
. . 3
⊢ Rel 𝑆 |
28 | | fvex 6784 |
. . . . . 6
⊢
(2nd ‘(𝑅‘(◡𝐺‘𝑣))) ∈ V |
29 | | eqeq2 2752 |
. . . . . . . 8
⊢ (𝑤 = (2nd ‘(𝑅‘(◡𝐺‘𝑣))) → (𝑧 = 𝑤 ↔ 𝑧 = (2nd ‘(𝑅‘(◡𝐺‘𝑣))))) |
30 | 29 | imbi2d 341 |
. . . . . . 7
⊢ (𝑤 = (2nd ‘(𝑅‘(◡𝐺‘𝑣))) → ((〈𝑣, 𝑧〉 ∈ 𝑆 → 𝑧 = 𝑤) ↔ (〈𝑣, 𝑧〉 ∈ 𝑆 → 𝑧 = (2nd ‘(𝑅‘(◡𝐺‘𝑣)))))) |
31 | 30 | albidv 1927 |
. . . . . 6
⊢ (𝑤 = (2nd ‘(𝑅‘(◡𝐺‘𝑣))) → (∀𝑧(〈𝑣, 𝑧〉 ∈ 𝑆 → 𝑧 = 𝑤) ↔ ∀𝑧(〈𝑣, 𝑧〉 ∈ 𝑆 → 𝑧 = (2nd ‘(𝑅‘(◡𝐺‘𝑣)))))) |
32 | 28, 31 | spcev 3544 |
. . . . 5
⊢
(∀𝑧(〈𝑣, 𝑧〉 ∈ 𝑆 → 𝑧 = (2nd ‘(𝑅‘(◡𝐺‘𝑣)))) → ∃𝑤∀𝑧(〈𝑣, 𝑧〉 ∈ 𝑆 → 𝑧 = 𝑤)) |
33 | 1 | eleq2i 2832 |
. . . . . . 7
⊢
(〈𝑣, 𝑧〉 ∈ 𝑆 ↔ 〈𝑣, 𝑧〉 ∈ ran 𝑅) |
34 | | fvelrnb 6827 |
. . . . . . . 8
⊢ (𝑅 Fn ω → (〈𝑣, 𝑧〉 ∈ ran 𝑅 ↔ ∃𝑤 ∈ ω (𝑅‘𝑤) = 〈𝑣, 𝑧〉)) |
35 | 6, 34 | ax-mp 5 |
. . . . . . 7
⊢
(〈𝑣, 𝑧〉 ∈ ran 𝑅 ↔ ∃𝑤 ∈ ω (𝑅‘𝑤) = 〈𝑣, 𝑧〉) |
36 | 33, 35 | bitri 274 |
. . . . . 6
⊢
(〈𝑣, 𝑧〉 ∈ 𝑆 ↔ ∃𝑤 ∈ ω (𝑅‘𝑤) = 〈𝑣, 𝑧〉) |
37 | 13 | eqeq1d 2742 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ ω → ((𝑅‘𝑤) = 〈𝑣, 𝑧〉 ↔ 〈(𝐺‘𝑤), (2nd ‘(𝑅‘𝑤))〉 = 〈𝑣, 𝑧〉)) |
38 | | fvex 6784 |
. . . . . . . . . . . . 13
⊢ (𝐺‘𝑤) ∈ V |
39 | 38, 15 | opth1 5394 |
. . . . . . . . . . . 12
⊢
(〈(𝐺‘𝑤), (2nd ‘(𝑅‘𝑤))〉 = 〈𝑣, 𝑧〉 → (𝐺‘𝑤) = 𝑣) |
40 | 37, 39 | syl6bi 252 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ω → ((𝑅‘𝑤) = 〈𝑣, 𝑧〉 → (𝐺‘𝑤) = 𝑣)) |
41 | 10, 11 | om2uzf1oi 13671 |
. . . . . . . . . . . 12
⊢ 𝐺:ω–1-1-onto→(ℤ≥‘𝐶) |
42 | | f1ocnvfv 7147 |
. . . . . . . . . . . 12
⊢ ((𝐺:ω–1-1-onto→(ℤ≥‘𝐶) ∧ 𝑤 ∈ ω) → ((𝐺‘𝑤) = 𝑣 → (◡𝐺‘𝑣) = 𝑤)) |
43 | 41, 42 | mpan 687 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ω → ((𝐺‘𝑤) = 𝑣 → (◡𝐺‘𝑣) = 𝑤)) |
44 | 40, 43 | syld 47 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ω → ((𝑅‘𝑤) = 〈𝑣, 𝑧〉 → (◡𝐺‘𝑣) = 𝑤)) |
45 | | 2fveq3 6776 |
. . . . . . . . . 10
⊢ ((◡𝐺‘𝑣) = 𝑤 → (2nd ‘(𝑅‘(◡𝐺‘𝑣))) = (2nd ‘(𝑅‘𝑤))) |
46 | 44, 45 | syl6 35 |
. . . . . . . . 9
⊢ (𝑤 ∈ ω → ((𝑅‘𝑤) = 〈𝑣, 𝑧〉 → (2nd ‘(𝑅‘(◡𝐺‘𝑣))) = (2nd ‘(𝑅‘𝑤)))) |
47 | 46 | imp 407 |
. . . . . . . 8
⊢ ((𝑤 ∈ ω ∧ (𝑅‘𝑤) = 〈𝑣, 𝑧〉) → (2nd ‘(𝑅‘(◡𝐺‘𝑣))) = (2nd ‘(𝑅‘𝑤))) |
48 | | vex 3435 |
. . . . . . . . . 10
⊢ 𝑣 ∈ V |
49 | | vex 3435 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
50 | 48, 49 | op2ndd 7835 |
. . . . . . . . 9
⊢ ((𝑅‘𝑤) = 〈𝑣, 𝑧〉 → (2nd ‘(𝑅‘𝑤)) = 𝑧) |
51 | 50 | adantl 482 |
. . . . . . . 8
⊢ ((𝑤 ∈ ω ∧ (𝑅‘𝑤) = 〈𝑣, 𝑧〉) → (2nd ‘(𝑅‘𝑤)) = 𝑧) |
52 | 47, 51 | eqtr2d 2781 |
. . . . . . 7
⊢ ((𝑤 ∈ ω ∧ (𝑅‘𝑤) = 〈𝑣, 𝑧〉) → 𝑧 = (2nd ‘(𝑅‘(◡𝐺‘𝑣)))) |
53 | 52 | rexlimiva 3212 |
. . . . . 6
⊢
(∃𝑤 ∈
ω (𝑅‘𝑤) = 〈𝑣, 𝑧〉 → 𝑧 = (2nd ‘(𝑅‘(◡𝐺‘𝑣)))) |
54 | 36, 53 | sylbi 216 |
. . . . 5
⊢
(〈𝑣, 𝑧〉 ∈ 𝑆 → 𝑧 = (2nd ‘(𝑅‘(◡𝐺‘𝑣)))) |
55 | 32, 54 | mpg 1804 |
. . . 4
⊢
∃𝑤∀𝑧(〈𝑣, 𝑧〉 ∈ 𝑆 → 𝑧 = 𝑤) |
56 | 55 | ax-gen 1802 |
. . 3
⊢
∀𝑣∃𝑤∀𝑧(〈𝑣, 𝑧〉 ∈ 𝑆 → 𝑧 = 𝑤) |
57 | | dffun5 6445 |
. . 3
⊢ (Fun
𝑆 ↔ (Rel 𝑆 ∧ ∀𝑣∃𝑤∀𝑧(〈𝑣, 𝑧〉 ∈ 𝑆 → 𝑧 = 𝑤))) |
58 | 27, 56, 57 | mpbir2an 708 |
. 2
⊢ Fun 𝑆 |
59 | | dmss 5810 |
. . . . 5
⊢ (𝑆 ⊆
((ℤ≥‘𝐶) × V) → dom 𝑆 ⊆ dom
((ℤ≥‘𝐶) × V)) |
60 | 23, 59 | ax-mp 5 |
. . . 4
⊢ dom 𝑆 ⊆ dom
((ℤ≥‘𝐶) × V) |
61 | | dmxpss 6073 |
. . . 4
⊢ dom
((ℤ≥‘𝐶) × V) ⊆
(ℤ≥‘𝐶) |
62 | 60, 61 | sstri 3935 |
. . 3
⊢ dom 𝑆 ⊆
(ℤ≥‘𝐶) |
63 | 10, 11, 12, 4 | uzrdglem 13675 |
. . . . . 6
⊢ (𝑣 ∈
(ℤ≥‘𝐶) → 〈𝑣, (2nd ‘(𝑅‘(◡𝐺‘𝑣)))〉 ∈ ran 𝑅) |
64 | 63, 1 | eleqtrrdi 2852 |
. . . . 5
⊢ (𝑣 ∈
(ℤ≥‘𝐶) → 〈𝑣, (2nd ‘(𝑅‘(◡𝐺‘𝑣)))〉 ∈ 𝑆) |
65 | 48, 28 | opeldm 5815 |
. . . . 5
⊢
(〈𝑣,
(2nd ‘(𝑅‘(◡𝐺‘𝑣)))〉 ∈ 𝑆 → 𝑣 ∈ dom 𝑆) |
66 | 64, 65 | syl 17 |
. . . 4
⊢ (𝑣 ∈
(ℤ≥‘𝐶) → 𝑣 ∈ dom 𝑆) |
67 | 66 | ssriv 3930 |
. . 3
⊢
(ℤ≥‘𝐶) ⊆ dom 𝑆 |
68 | 62, 67 | eqssi 3942 |
. 2
⊢ dom 𝑆 =
(ℤ≥‘𝐶) |
69 | | df-fn 6435 |
. 2
⊢ (𝑆 Fn
(ℤ≥‘𝐶) ↔ (Fun 𝑆 ∧ dom 𝑆 = (ℤ≥‘𝐶))) |
70 | 58, 68, 69 | mpbir2an 708 |
1
⊢ 𝑆 Fn
(ℤ≥‘𝐶) |