Step | Hyp | Ref
| Expression |
1 | | frfnom 7417 |
. . . . . . 7
⊢
(rec((𝑖 ∈
ω, 𝑣 ∈ V ↦
〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾ ω) Fn
ω |
2 | | seqomlem.a |
. . . . . . . . 9
⊢ 𝑄 = rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) |
3 | 2 | reseq1i 5313 |
. . . . . . . 8
⊢ (𝑄 ↾ ω) = (rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc
𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾
ω) |
4 | 3 | fneq1i 5899 |
. . . . . . 7
⊢ ((𝑄 ↾ ω) Fn ω
↔ (rec((𝑖 ∈
ω, 𝑣 ∈ V ↦
〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾ ω) Fn
ω) |
5 | 1, 4 | mpbir 220 |
. . . . . 6
⊢ (𝑄 ↾ ω) Fn
ω |
6 | | fvres 6117 |
. . . . . . . . 9
⊢ (𝑏 ∈ ω → ((𝑄 ↾ ω)‘𝑏) = (𝑄‘𝑏)) |
7 | 2 | seqomlem1 7432 |
. . . . . . . . 9
⊢ (𝑏 ∈ ω → (𝑄‘𝑏) = 〈𝑏, (2nd ‘(𝑄‘𝑏))〉) |
8 | 6, 7 | eqtrd 2644 |
. . . . . . . 8
⊢ (𝑏 ∈ ω → ((𝑄 ↾ ω)‘𝑏) = 〈𝑏, (2nd ‘(𝑄‘𝑏))〉) |
9 | | fvex 6113 |
. . . . . . . . 9
⊢
(2nd ‘(𝑄‘𝑏)) ∈ V |
10 | | opelxpi 5072 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ω ∧
(2nd ‘(𝑄‘𝑏)) ∈ V) → 〈𝑏, (2nd ‘(𝑄‘𝑏))〉 ∈ (ω ×
V)) |
11 | 9, 10 | mpan2 703 |
. . . . . . . 8
⊢ (𝑏 ∈ ω →
〈𝑏, (2nd
‘(𝑄‘𝑏))〉 ∈ (ω ×
V)) |
12 | 8, 11 | eqeltrd 2688 |
. . . . . . 7
⊢ (𝑏 ∈ ω → ((𝑄 ↾ ω)‘𝑏) ∈ (ω ×
V)) |
13 | 12 | rgen 2906 |
. . . . . 6
⊢
∀𝑏 ∈
ω ((𝑄 ↾
ω)‘𝑏) ∈
(ω × V) |
14 | | ffnfv 6295 |
. . . . . 6
⊢ ((𝑄 ↾
ω):ω⟶(ω × V) ↔ ((𝑄 ↾ ω) Fn ω ∧
∀𝑏 ∈ ω
((𝑄 ↾
ω)‘𝑏) ∈
(ω × V))) |
15 | 5, 13, 14 | mpbir2an 957 |
. . . . 5
⊢ (𝑄 ↾
ω):ω⟶(ω × V) |
16 | | frn 5966 |
. . . . 5
⊢ ((𝑄 ↾
ω):ω⟶(ω × V) → ran (𝑄 ↾ ω) ⊆ (ω ×
V)) |
17 | 15, 16 | ax-mp 5 |
. . . 4
⊢ ran
(𝑄 ↾ ω) ⊆
(ω × V) |
18 | | df-br 4584 |
. . . . . . . . . 10
⊢ (𝑎ran (𝑄 ↾ ω)𝑏 ↔ 〈𝑎, 𝑏〉 ∈ ran (𝑄 ↾ ω)) |
19 | | fvelrnb 6153 |
. . . . . . . . . . 11
⊢ ((𝑄 ↾ ω) Fn ω
→ (〈𝑎, 𝑏〉 ∈ ran (𝑄 ↾ ω) ↔
∃𝑐 ∈ ω
((𝑄 ↾
ω)‘𝑐) =
〈𝑎, 𝑏〉)) |
20 | 5, 19 | ax-mp 5 |
. . . . . . . . . 10
⊢
(〈𝑎, 𝑏〉 ∈ ran (𝑄 ↾ ω) ↔
∃𝑐 ∈ ω
((𝑄 ↾
ω)‘𝑐) =
〈𝑎, 𝑏〉) |
21 | | fvres 6117 |
. . . . . . . . . . . 12
⊢ (𝑐 ∈ ω → ((𝑄 ↾ ω)‘𝑐) = (𝑄‘𝑐)) |
22 | 21 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢ (𝑐 ∈ ω → (((𝑄 ↾ ω)‘𝑐) = 〈𝑎, 𝑏〉 ↔ (𝑄‘𝑐) = 〈𝑎, 𝑏〉)) |
23 | 22 | rexbiia 3022 |
. . . . . . . . . 10
⊢
(∃𝑐 ∈
ω ((𝑄 ↾
ω)‘𝑐) =
〈𝑎, 𝑏〉 ↔ ∃𝑐 ∈ ω (𝑄‘𝑐) = 〈𝑎, 𝑏〉) |
24 | 18, 20, 23 | 3bitri 285 |
. . . . . . . . 9
⊢ (𝑎ran (𝑄 ↾ ω)𝑏 ↔ ∃𝑐 ∈ ω (𝑄‘𝑐) = 〈𝑎, 𝑏〉) |
25 | 2 | seqomlem1 7432 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 ∈ ω → (𝑄‘𝑐) = 〈𝑐, (2nd ‘(𝑄‘𝑐))〉) |
26 | 25 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ω ∧ 𝑐 ∈ ω) → (𝑄‘𝑐) = 〈𝑐, (2nd ‘(𝑄‘𝑐))〉) |
27 | 26 | eqeq1d 2612 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ω ∧ 𝑐 ∈ ω) → ((𝑄‘𝑐) = 〈𝑎, 𝑏〉 ↔ 〈𝑐, (2nd ‘(𝑄‘𝑐))〉 = 〈𝑎, 𝑏〉)) |
28 | | vex 3176 |
. . . . . . . . . . . . . . 15
⊢ 𝑐 ∈ V |
29 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢
(2nd ‘(𝑄‘𝑐)) ∈ V |
30 | 28, 29 | opth1 4870 |
. . . . . . . . . . . . . 14
⊢
(〈𝑐,
(2nd ‘(𝑄‘𝑐))〉 = 〈𝑎, 𝑏〉 → 𝑐 = 𝑎) |
31 | 27, 30 | syl6bi 242 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ω ∧ 𝑐 ∈ ω) → ((𝑄‘𝑐) = 〈𝑎, 𝑏〉 → 𝑐 = 𝑎)) |
32 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = 𝑎 → (𝑄‘𝑐) = (𝑄‘𝑎)) |
33 | 32 | eqeq1d 2612 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = 𝑎 → ((𝑄‘𝑐) = 〈𝑎, 𝑏〉 ↔ (𝑄‘𝑎) = 〈𝑎, 𝑏〉)) |
34 | 33 | biimpd 218 |
. . . . . . . . . . . . 13
⊢ (𝑐 = 𝑎 → ((𝑄‘𝑐) = 〈𝑎, 𝑏〉 → (𝑄‘𝑎) = 〈𝑎, 𝑏〉)) |
35 | 31, 34 | syli 38 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ω ∧ 𝑐 ∈ ω) → ((𝑄‘𝑐) = 〈𝑎, 𝑏〉 → (𝑄‘𝑎) = 〈𝑎, 𝑏〉)) |
36 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ ((𝑄‘𝑎) = 〈𝑎, 𝑏〉 → (2nd ‘(𝑄‘𝑎)) = (2nd ‘〈𝑎, 𝑏〉)) |
37 | | vex 3176 |
. . . . . . . . . . . . . 14
⊢ 𝑎 ∈ V |
38 | | vex 3176 |
. . . . . . . . . . . . . 14
⊢ 𝑏 ∈ V |
39 | 37, 38 | op2nd 7068 |
. . . . . . . . . . . . 13
⊢
(2nd ‘〈𝑎, 𝑏〉) = 𝑏 |
40 | 36, 39 | syl6req 2661 |
. . . . . . . . . . . 12
⊢ ((𝑄‘𝑎) = 〈𝑎, 𝑏〉 → 𝑏 = (2nd ‘(𝑄‘𝑎))) |
41 | 35, 40 | syl6 34 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ω ∧ 𝑐 ∈ ω) → ((𝑄‘𝑐) = 〈𝑎, 𝑏〉 → 𝑏 = (2nd ‘(𝑄‘𝑎)))) |
42 | 41 | rexlimdva 3013 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ω →
(∃𝑐 ∈ ω
(𝑄‘𝑐) = 〈𝑎, 𝑏〉 → 𝑏 = (2nd ‘(𝑄‘𝑎)))) |
43 | 2 | seqomlem1 7432 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ω → (𝑄‘𝑎) = 〈𝑎, (2nd ‘(𝑄‘𝑎))〉) |
44 | 32 | eqeq1d 2612 |
. . . . . . . . . . . . 13
⊢ (𝑐 = 𝑎 → ((𝑄‘𝑐) = 〈𝑎, (2nd ‘(𝑄‘𝑎))〉 ↔ (𝑄‘𝑎) = 〈𝑎, (2nd ‘(𝑄‘𝑎))〉)) |
45 | 44 | rspcev 3282 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ω ∧ (𝑄‘𝑎) = 〈𝑎, (2nd ‘(𝑄‘𝑎))〉) → ∃𝑐 ∈ ω (𝑄‘𝑐) = 〈𝑎, (2nd ‘(𝑄‘𝑎))〉) |
46 | 43, 45 | mpdan 699 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ω →
∃𝑐 ∈ ω
(𝑄‘𝑐) = 〈𝑎, (2nd ‘(𝑄‘𝑎))〉) |
47 | | opeq2 4341 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (2nd ‘(𝑄‘𝑎)) → 〈𝑎, 𝑏〉 = 〈𝑎, (2nd ‘(𝑄‘𝑎))〉) |
48 | 47 | eqeq2d 2620 |
. . . . . . . . . . . 12
⊢ (𝑏 = (2nd ‘(𝑄‘𝑎)) → ((𝑄‘𝑐) = 〈𝑎, 𝑏〉 ↔ (𝑄‘𝑐) = 〈𝑎, (2nd ‘(𝑄‘𝑎))〉)) |
49 | 48 | rexbidv 3034 |
. . . . . . . . . . 11
⊢ (𝑏 = (2nd ‘(𝑄‘𝑎)) → (∃𝑐 ∈ ω (𝑄‘𝑐) = 〈𝑎, 𝑏〉 ↔ ∃𝑐 ∈ ω (𝑄‘𝑐) = 〈𝑎, (2nd ‘(𝑄‘𝑎))〉)) |
50 | 46, 49 | syl5ibrcom 236 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ω → (𝑏 = (2nd ‘(𝑄‘𝑎)) → ∃𝑐 ∈ ω (𝑄‘𝑐) = 〈𝑎, 𝑏〉)) |
51 | 42, 50 | impbid 201 |
. . . . . . . . 9
⊢ (𝑎 ∈ ω →
(∃𝑐 ∈ ω
(𝑄‘𝑐) = 〈𝑎, 𝑏〉 ↔ 𝑏 = (2nd ‘(𝑄‘𝑎)))) |
52 | 24, 51 | syl5bb 271 |
. . . . . . . 8
⊢ (𝑎 ∈ ω → (𝑎ran (𝑄 ↾ ω)𝑏 ↔ 𝑏 = (2nd ‘(𝑄‘𝑎)))) |
53 | 52 | alrimiv 1842 |
. . . . . . 7
⊢ (𝑎 ∈ ω →
∀𝑏(𝑎ran (𝑄 ↾ ω)𝑏 ↔ 𝑏 = (2nd ‘(𝑄‘𝑎)))) |
54 | | fvex 6113 |
. . . . . . . 8
⊢
(2nd ‘(𝑄‘𝑎)) ∈ V |
55 | | eqeq2 2621 |
. . . . . . . . . 10
⊢ (𝑐 = (2nd ‘(𝑄‘𝑎)) → (𝑏 = 𝑐 ↔ 𝑏 = (2nd ‘(𝑄‘𝑎)))) |
56 | 55 | bibi2d 331 |
. . . . . . . . 9
⊢ (𝑐 = (2nd ‘(𝑄‘𝑎)) → ((𝑎ran (𝑄 ↾ ω)𝑏 ↔ 𝑏 = 𝑐) ↔ (𝑎ran (𝑄 ↾ ω)𝑏 ↔ 𝑏 = (2nd ‘(𝑄‘𝑎))))) |
57 | 56 | albidv 1836 |
. . . . . . . 8
⊢ (𝑐 = (2nd ‘(𝑄‘𝑎)) → (∀𝑏(𝑎ran (𝑄 ↾ ω)𝑏 ↔ 𝑏 = 𝑐) ↔ ∀𝑏(𝑎ran (𝑄 ↾ ω)𝑏 ↔ 𝑏 = (2nd ‘(𝑄‘𝑎))))) |
58 | 54, 57 | spcev 3273 |
. . . . . . 7
⊢
(∀𝑏(𝑎ran (𝑄 ↾ ω)𝑏 ↔ 𝑏 = (2nd ‘(𝑄‘𝑎))) → ∃𝑐∀𝑏(𝑎ran (𝑄 ↾ ω)𝑏 ↔ 𝑏 = 𝑐)) |
59 | 53, 58 | syl 17 |
. . . . . 6
⊢ (𝑎 ∈ ω →
∃𝑐∀𝑏(𝑎ran (𝑄 ↾ ω)𝑏 ↔ 𝑏 = 𝑐)) |
60 | | df-eu 2462 |
. . . . . 6
⊢
(∃!𝑏 𝑎ran (𝑄 ↾ ω)𝑏 ↔ ∃𝑐∀𝑏(𝑎ran (𝑄 ↾ ω)𝑏 ↔ 𝑏 = 𝑐)) |
61 | 59, 60 | sylibr 223 |
. . . . 5
⊢ (𝑎 ∈ ω →
∃!𝑏 𝑎ran (𝑄 ↾ ω)𝑏) |
62 | 61 | rgen 2906 |
. . . 4
⊢
∀𝑎 ∈
ω ∃!𝑏 𝑎ran (𝑄 ↾ ω)𝑏 |
63 | | dff3 6280 |
. . . 4
⊢ (ran
(𝑄 ↾
ω):ω⟶V ↔ (ran (𝑄 ↾ ω) ⊆ (ω ×
V) ∧ ∀𝑎 ∈
ω ∃!𝑏 𝑎ran (𝑄 ↾ ω)𝑏)) |
64 | 17, 62, 63 | mpbir2an 957 |
. . 3
⊢ ran
(𝑄 ↾
ω):ω⟶V |
65 | | df-ima 5051 |
. . . 4
⊢ (𝑄 “ ω) = ran (𝑄 ↾
ω) |
66 | 65 | feq1i 5949 |
. . 3
⊢ ((𝑄 “
ω):ω⟶V ↔ ran (𝑄 ↾
ω):ω⟶V) |
67 | 64, 66 | mpbir 220 |
. 2
⊢ (𝑄 “
ω):ω⟶V |
68 | | dffn2 5960 |
. 2
⊢ ((𝑄 “ ω) Fn ω
↔ (𝑄 “
ω):ω⟶V) |
69 | 67, 68 | mpbir 220 |
1
⊢ (𝑄 “ ω) Fn
ω |