| Step | Hyp | Ref
| Expression |
| 1 | | frfnom 8475 |
. . . . . . 7
⊢
(rec((𝑖 ∈
ω, 𝑣 ∈ V ↦
〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾ ω) Fn
ω |
| 2 | | seqomlem.a |
. . . . . . . . 9
⊢ 𝑄 = rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) |
| 3 | 2 | reseq1i 5993 |
. . . . . . . 8
⊢ (𝑄 ↾ ω) = (rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc
𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾
ω) |
| 4 | 3 | fneq1i 6665 |
. . . . . . 7
⊢ ((𝑄 ↾ ω) Fn ω
↔ (rec((𝑖 ∈
ω, 𝑣 ∈ V ↦
〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾ ω) Fn
ω) |
| 5 | 1, 4 | mpbir 231 |
. . . . . 6
⊢ (𝑄 ↾ ω) Fn
ω |
| 6 | | fvres 6925 |
. . . . . . . . 9
⊢ (𝑏 ∈ ω → ((𝑄 ↾ ω)‘𝑏) = (𝑄‘𝑏)) |
| 7 | 2 | seqomlem1 8490 |
. . . . . . . . 9
⊢ (𝑏 ∈ ω → (𝑄‘𝑏) = 〈𝑏, (2nd ‘(𝑄‘𝑏))〉) |
| 8 | 6, 7 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝑏 ∈ ω → ((𝑄 ↾ ω)‘𝑏) = 〈𝑏, (2nd ‘(𝑄‘𝑏))〉) |
| 9 | | fvex 6919 |
. . . . . . . . 9
⊢
(2nd ‘(𝑄‘𝑏)) ∈ V |
| 10 | | opelxpi 5722 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ω ∧
(2nd ‘(𝑄‘𝑏)) ∈ V) → 〈𝑏, (2nd ‘(𝑄‘𝑏))〉 ∈ (ω ×
V)) |
| 11 | 9, 10 | mpan2 691 |
. . . . . . . 8
⊢ (𝑏 ∈ ω →
〈𝑏, (2nd
‘(𝑄‘𝑏))〉 ∈ (ω ×
V)) |
| 12 | 8, 11 | eqeltrd 2841 |
. . . . . . 7
⊢ (𝑏 ∈ ω → ((𝑄 ↾ ω)‘𝑏) ∈ (ω ×
V)) |
| 13 | 12 | rgen 3063 |
. . . . . 6
⊢
∀𝑏 ∈
ω ((𝑄 ↾
ω)‘𝑏) ∈
(ω × V) |
| 14 | | ffnfv 7139 |
. . . . . 6
⊢ ((𝑄 ↾
ω):ω⟶(ω × V) ↔ ((𝑄 ↾ ω) Fn ω ∧
∀𝑏 ∈ ω
((𝑄 ↾
ω)‘𝑏) ∈
(ω × V))) |
| 15 | 5, 13, 14 | mpbir2an 711 |
. . . . 5
⊢ (𝑄 ↾
ω):ω⟶(ω × V) |
| 16 | | frn 6743 |
. . . . 5
⊢ ((𝑄 ↾
ω):ω⟶(ω × V) → ran (𝑄 ↾ ω) ⊆ (ω ×
V)) |
| 17 | 15, 16 | ax-mp 5 |
. . . 4
⊢ ran
(𝑄 ↾ ω) ⊆
(ω × V) |
| 18 | | df-br 5144 |
. . . . . . . . . 10
⊢ (𝑎ran (𝑄 ↾ ω)𝑏 ↔ 〈𝑎, 𝑏〉 ∈ ran (𝑄 ↾ ω)) |
| 19 | | fvelrnb 6969 |
. . . . . . . . . . 11
⊢ ((𝑄 ↾ ω) Fn ω
→ (〈𝑎, 𝑏〉 ∈ ran (𝑄 ↾ ω) ↔
∃𝑐 ∈ ω
((𝑄 ↾
ω)‘𝑐) =
〈𝑎, 𝑏〉)) |
| 20 | 5, 19 | ax-mp 5 |
. . . . . . . . . 10
⊢
(〈𝑎, 𝑏〉 ∈ ran (𝑄 ↾ ω) ↔
∃𝑐 ∈ ω
((𝑄 ↾
ω)‘𝑐) =
〈𝑎, 𝑏〉) |
| 21 | | fvres 6925 |
. . . . . . . . . . . 12
⊢ (𝑐 ∈ ω → ((𝑄 ↾ ω)‘𝑐) = (𝑄‘𝑐)) |
| 22 | 21 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ (𝑐 ∈ ω → (((𝑄 ↾ ω)‘𝑐) = 〈𝑎, 𝑏〉 ↔ (𝑄‘𝑐) = 〈𝑎, 𝑏〉)) |
| 23 | 22 | rexbiia 3092 |
. . . . . . . . . 10
⊢
(∃𝑐 ∈
ω ((𝑄 ↾
ω)‘𝑐) =
〈𝑎, 𝑏〉 ↔ ∃𝑐 ∈ ω (𝑄‘𝑐) = 〈𝑎, 𝑏〉) |
| 24 | 18, 20, 23 | 3bitri 297 |
. . . . . . . . 9
⊢ (𝑎ran (𝑄 ↾ ω)𝑏 ↔ ∃𝑐 ∈ ω (𝑄‘𝑐) = 〈𝑎, 𝑏〉) |
| 25 | 2 | seqomlem1 8490 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 ∈ ω → (𝑄‘𝑐) = 〈𝑐, (2nd ‘(𝑄‘𝑐))〉) |
| 26 | 25 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ω ∧ 𝑐 ∈ ω) → (𝑄‘𝑐) = 〈𝑐, (2nd ‘(𝑄‘𝑐))〉) |
| 27 | 26 | eqeq1d 2739 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ω ∧ 𝑐 ∈ ω) → ((𝑄‘𝑐) = 〈𝑎, 𝑏〉 ↔ 〈𝑐, (2nd ‘(𝑄‘𝑐))〉 = 〈𝑎, 𝑏〉)) |
| 28 | | vex 3484 |
. . . . . . . . . . . . . . 15
⊢ 𝑐 ∈ V |
| 29 | | fvex 6919 |
. . . . . . . . . . . . . . 15
⊢
(2nd ‘(𝑄‘𝑐)) ∈ V |
| 30 | 28, 29 | opth1 5480 |
. . . . . . . . . . . . . 14
⊢
(〈𝑐,
(2nd ‘(𝑄‘𝑐))〉 = 〈𝑎, 𝑏〉 → 𝑐 = 𝑎) |
| 31 | 27, 30 | biimtrdi 253 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ω ∧ 𝑐 ∈ ω) → ((𝑄‘𝑐) = 〈𝑎, 𝑏〉 → 𝑐 = 𝑎)) |
| 32 | | fveqeq2 6915 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = 𝑎 → ((𝑄‘𝑐) = 〈𝑎, 𝑏〉 ↔ (𝑄‘𝑎) = 〈𝑎, 𝑏〉)) |
| 33 | 32 | biimpd 229 |
. . . . . . . . . . . . 13
⊢ (𝑐 = 𝑎 → ((𝑄‘𝑐) = 〈𝑎, 𝑏〉 → (𝑄‘𝑎) = 〈𝑎, 𝑏〉)) |
| 34 | 31, 33 | syli 39 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ω ∧ 𝑐 ∈ ω) → ((𝑄‘𝑐) = 〈𝑎, 𝑏〉 → (𝑄‘𝑎) = 〈𝑎, 𝑏〉)) |
| 35 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ ((𝑄‘𝑎) = 〈𝑎, 𝑏〉 → (2nd ‘(𝑄‘𝑎)) = (2nd ‘〈𝑎, 𝑏〉)) |
| 36 | | vex 3484 |
. . . . . . . . . . . . . 14
⊢ 𝑎 ∈ V |
| 37 | | vex 3484 |
. . . . . . . . . . . . . 14
⊢ 𝑏 ∈ V |
| 38 | 36, 37 | op2nd 8023 |
. . . . . . . . . . . . 13
⊢
(2nd ‘〈𝑎, 𝑏〉) = 𝑏 |
| 39 | 35, 38 | eqtr2di 2794 |
. . . . . . . . . . . 12
⊢ ((𝑄‘𝑎) = 〈𝑎, 𝑏〉 → 𝑏 = (2nd ‘(𝑄‘𝑎))) |
| 40 | 34, 39 | syl6 35 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ω ∧ 𝑐 ∈ ω) → ((𝑄‘𝑐) = 〈𝑎, 𝑏〉 → 𝑏 = (2nd ‘(𝑄‘𝑎)))) |
| 41 | 40 | rexlimdva 3155 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ω →
(∃𝑐 ∈ ω
(𝑄‘𝑐) = 〈𝑎, 𝑏〉 → 𝑏 = (2nd ‘(𝑄‘𝑎)))) |
| 42 | 2 | seqomlem1 8490 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ω → (𝑄‘𝑎) = 〈𝑎, (2nd ‘(𝑄‘𝑎))〉) |
| 43 | | fveqeq2 6915 |
. . . . . . . . . . . . 13
⊢ (𝑐 = 𝑎 → ((𝑄‘𝑐) = 〈𝑎, (2nd ‘(𝑄‘𝑎))〉 ↔ (𝑄‘𝑎) = 〈𝑎, (2nd ‘(𝑄‘𝑎))〉)) |
| 44 | 43 | rspcev 3622 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ω ∧ (𝑄‘𝑎) = 〈𝑎, (2nd ‘(𝑄‘𝑎))〉) → ∃𝑐 ∈ ω (𝑄‘𝑐) = 〈𝑎, (2nd ‘(𝑄‘𝑎))〉) |
| 45 | 42, 44 | mpdan 687 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ω →
∃𝑐 ∈ ω
(𝑄‘𝑐) = 〈𝑎, (2nd ‘(𝑄‘𝑎))〉) |
| 46 | | opeq2 4874 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (2nd ‘(𝑄‘𝑎)) → 〈𝑎, 𝑏〉 = 〈𝑎, (2nd ‘(𝑄‘𝑎))〉) |
| 47 | 46 | eqeq2d 2748 |
. . . . . . . . . . . 12
⊢ (𝑏 = (2nd ‘(𝑄‘𝑎)) → ((𝑄‘𝑐) = 〈𝑎, 𝑏〉 ↔ (𝑄‘𝑐) = 〈𝑎, (2nd ‘(𝑄‘𝑎))〉)) |
| 48 | 47 | rexbidv 3179 |
. . . . . . . . . . 11
⊢ (𝑏 = (2nd ‘(𝑄‘𝑎)) → (∃𝑐 ∈ ω (𝑄‘𝑐) = 〈𝑎, 𝑏〉 ↔ ∃𝑐 ∈ ω (𝑄‘𝑐) = 〈𝑎, (2nd ‘(𝑄‘𝑎))〉)) |
| 49 | 45, 48 | syl5ibrcom 247 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ω → (𝑏 = (2nd ‘(𝑄‘𝑎)) → ∃𝑐 ∈ ω (𝑄‘𝑐) = 〈𝑎, 𝑏〉)) |
| 50 | 41, 49 | impbid 212 |
. . . . . . . . 9
⊢ (𝑎 ∈ ω →
(∃𝑐 ∈ ω
(𝑄‘𝑐) = 〈𝑎, 𝑏〉 ↔ 𝑏 = (2nd ‘(𝑄‘𝑎)))) |
| 51 | 24, 50 | bitrid 283 |
. . . . . . . 8
⊢ (𝑎 ∈ ω → (𝑎ran (𝑄 ↾ ω)𝑏 ↔ 𝑏 = (2nd ‘(𝑄‘𝑎)))) |
| 52 | 51 | alrimiv 1927 |
. . . . . . 7
⊢ (𝑎 ∈ ω →
∀𝑏(𝑎ran (𝑄 ↾ ω)𝑏 ↔ 𝑏 = (2nd ‘(𝑄‘𝑎)))) |
| 53 | | fvex 6919 |
. . . . . . . 8
⊢
(2nd ‘(𝑄‘𝑎)) ∈ V |
| 54 | | eqeq2 2749 |
. . . . . . . . . 10
⊢ (𝑐 = (2nd ‘(𝑄‘𝑎)) → (𝑏 = 𝑐 ↔ 𝑏 = (2nd ‘(𝑄‘𝑎)))) |
| 55 | 54 | bibi2d 342 |
. . . . . . . . 9
⊢ (𝑐 = (2nd ‘(𝑄‘𝑎)) → ((𝑎ran (𝑄 ↾ ω)𝑏 ↔ 𝑏 = 𝑐) ↔ (𝑎ran (𝑄 ↾ ω)𝑏 ↔ 𝑏 = (2nd ‘(𝑄‘𝑎))))) |
| 56 | 55 | albidv 1920 |
. . . . . . . 8
⊢ (𝑐 = (2nd ‘(𝑄‘𝑎)) → (∀𝑏(𝑎ran (𝑄 ↾ ω)𝑏 ↔ 𝑏 = 𝑐) ↔ ∀𝑏(𝑎ran (𝑄 ↾ ω)𝑏 ↔ 𝑏 = (2nd ‘(𝑄‘𝑎))))) |
| 57 | 53, 56 | spcev 3606 |
. . . . . . 7
⊢
(∀𝑏(𝑎ran (𝑄 ↾ ω)𝑏 ↔ 𝑏 = (2nd ‘(𝑄‘𝑎))) → ∃𝑐∀𝑏(𝑎ran (𝑄 ↾ ω)𝑏 ↔ 𝑏 = 𝑐)) |
| 58 | 52, 57 | syl 17 |
. . . . . 6
⊢ (𝑎 ∈ ω →
∃𝑐∀𝑏(𝑎ran (𝑄 ↾ ω)𝑏 ↔ 𝑏 = 𝑐)) |
| 59 | | eu6 2574 |
. . . . . 6
⊢
(∃!𝑏 𝑎ran (𝑄 ↾ ω)𝑏 ↔ ∃𝑐∀𝑏(𝑎ran (𝑄 ↾ ω)𝑏 ↔ 𝑏 = 𝑐)) |
| 60 | 58, 59 | sylibr 234 |
. . . . 5
⊢ (𝑎 ∈ ω →
∃!𝑏 𝑎ran (𝑄 ↾ ω)𝑏) |
| 61 | 60 | rgen 3063 |
. . . 4
⊢
∀𝑎 ∈
ω ∃!𝑏 𝑎ran (𝑄 ↾ ω)𝑏 |
| 62 | | dff3 7120 |
. . . 4
⊢ (ran
(𝑄 ↾
ω):ω⟶V ↔ (ran (𝑄 ↾ ω) ⊆ (ω ×
V) ∧ ∀𝑎 ∈
ω ∃!𝑏 𝑎ran (𝑄 ↾ ω)𝑏)) |
| 63 | 17, 61, 62 | mpbir2an 711 |
. . 3
⊢ ran
(𝑄 ↾
ω):ω⟶V |
| 64 | | df-ima 5698 |
. . . 4
⊢ (𝑄 “ ω) = ran (𝑄 ↾
ω) |
| 65 | 64 | feq1i 6727 |
. . 3
⊢ ((𝑄 “
ω):ω⟶V ↔ ran (𝑄 ↾
ω):ω⟶V) |
| 66 | 63, 65 | mpbir 231 |
. 2
⊢ (𝑄 “
ω):ω⟶V |
| 67 | | dffn2 6738 |
. 2
⊢ ((𝑄 “ ω) Fn ω
↔ (𝑄 “
ω):ω⟶V) |
| 68 | 66, 67 | mpbir 231 |
1
⊢ (𝑄 “ ω) Fn
ω |