| Step | Hyp | Ref
| Expression |
| 1 | | alephfplem.1 |
. . 3
⊢ 𝐻 = (rec(ℵ, ω)
↾ ω) |
| 2 | 1 | alephfplem4 10147 |
. 2
⊢ ∪ (𝐻
“ ω) ∈ ran ℵ |
| 3 | | isinfcard 10132 |
. . 3
⊢ ((ω
⊆ ∪ (𝐻 “ ω) ∧ (card‘∪ (𝐻
“ ω)) = ∪ (𝐻 “ ω)) ↔ ∪ (𝐻
“ ω) ∈ ran ℵ) |
| 4 | | cardalephex 10130 |
. . . 4
⊢ (ω
⊆ ∪ (𝐻 “ ω) → ((card‘∪ (𝐻
“ ω)) = ∪ (𝐻 “ ω) ↔ ∃𝑧 ∈ On ∪ (𝐻
“ ω) = (ℵ‘𝑧))) |
| 5 | 4 | biimpa 476 |
. . 3
⊢ ((ω
⊆ ∪ (𝐻 “ ω) ∧ (card‘∪ (𝐻
“ ω)) = ∪ (𝐻 “ ω)) → ∃𝑧 ∈ On ∪ (𝐻
“ ω) = (ℵ‘𝑧)) |
| 6 | 3, 5 | sylbir 235 |
. 2
⊢ (∪ (𝐻
“ ω) ∈ ran ℵ → ∃𝑧 ∈ On ∪
(𝐻 “ ω) =
(ℵ‘𝑧)) |
| 7 | | alephle 10128 |
. . . . . . . . 9
⊢ (𝑧 ∈ On → 𝑧 ⊆ (ℵ‘𝑧)) |
| 8 | | alephon 10109 |
. . . . . . . . . . 11
⊢
(ℵ‘𝑧)
∈ On |
| 9 | 8 | onirri 6497 |
. . . . . . . . . 10
⊢ ¬
(ℵ‘𝑧) ∈
(ℵ‘𝑧) |
| 10 | | frfnom 8475 |
. . . . . . . . . . . . . 14
⊢
(rec(ℵ, ω) ↾ ω) Fn ω |
| 11 | 1 | fneq1i 6665 |
. . . . . . . . . . . . . 14
⊢ (𝐻 Fn ω ↔ (rec(ℵ,
ω) ↾ ω) Fn ω) |
| 12 | 10, 11 | mpbir 231 |
. . . . . . . . . . . . 13
⊢ 𝐻 Fn ω |
| 13 | | fnfun 6668 |
. . . . . . . . . . . . 13
⊢ (𝐻 Fn ω → Fun 𝐻) |
| 14 | | eluniima 7270 |
. . . . . . . . . . . . 13
⊢ (Fun
𝐻 → (𝑧 ∈ ∪ (𝐻
“ ω) ↔ ∃𝑣 ∈ ω 𝑧 ∈ (𝐻‘𝑣))) |
| 15 | 12, 13, 14 | mp2b 10 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ∪ (𝐻
“ ω) ↔ ∃𝑣 ∈ ω 𝑧 ∈ (𝐻‘𝑣)) |
| 16 | | alephsson 10140 |
. . . . . . . . . . . . . . . 16
⊢ ran
ℵ ⊆ On |
| 17 | 1 | alephfplem3 10146 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 ∈ ω → (𝐻‘𝑣) ∈ ran ℵ) |
| 18 | 16, 17 | sselid 3981 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ ω → (𝐻‘𝑣) ∈ On) |
| 19 | | alephord2i 10117 |
. . . . . . . . . . . . . . 15
⊢ ((𝐻‘𝑣) ∈ On → (𝑧 ∈ (𝐻‘𝑣) → (ℵ‘𝑧) ∈ (ℵ‘(𝐻‘𝑣)))) |
| 20 | 18, 19 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ ω → (𝑧 ∈ (𝐻‘𝑣) → (ℵ‘𝑧) ∈ (ℵ‘(𝐻‘𝑣)))) |
| 21 | 1 | alephfplem2 10145 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 ∈ ω → (𝐻‘suc 𝑣) = (ℵ‘(𝐻‘𝑣))) |
| 22 | | peano2 7912 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 ∈ ω → suc 𝑣 ∈
ω) |
| 23 | | fnfvelrn 7100 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐻 Fn ω ∧ suc 𝑣 ∈ ω) → (𝐻‘suc 𝑣) ∈ ran 𝐻) |
| 24 | 12, 23 | mpan 690 |
. . . . . . . . . . . . . . . . . . 19
⊢ (suc
𝑣 ∈ ω →
(𝐻‘suc 𝑣) ∈ ran 𝐻) |
| 25 | | fnima 6698 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐻 Fn ω → (𝐻 “ ω) = ran 𝐻) |
| 26 | 12, 25 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐻 “ ω) = ran 𝐻 |
| 27 | 24, 26 | eleqtrrdi 2852 |
. . . . . . . . . . . . . . . . . 18
⊢ (suc
𝑣 ∈ ω →
(𝐻‘suc 𝑣) ∈ (𝐻 “ ω)) |
| 28 | 22, 27 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 ∈ ω → (𝐻‘suc 𝑣) ∈ (𝐻 “ ω)) |
| 29 | 21, 28 | eqeltrrd 2842 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 ∈ ω →
(ℵ‘(𝐻‘𝑣)) ∈ (𝐻 “ ω)) |
| 30 | | elssuni 4937 |
. . . . . . . . . . . . . . . 16
⊢
((ℵ‘(𝐻‘𝑣)) ∈ (𝐻 “ ω) →
(ℵ‘(𝐻‘𝑣)) ⊆ ∪
(𝐻 “
ω)) |
| 31 | 29, 30 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ ω →
(ℵ‘(𝐻‘𝑣)) ⊆ ∪
(𝐻 “
ω)) |
| 32 | 31 | sseld 3982 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ ω →
((ℵ‘𝑧) ∈
(ℵ‘(𝐻‘𝑣)) → (ℵ‘𝑧) ∈ ∪ (𝐻 “
ω))) |
| 33 | 20, 32 | syld 47 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ ω → (𝑧 ∈ (𝐻‘𝑣) → (ℵ‘𝑧) ∈ ∪ (𝐻 “
ω))) |
| 34 | 33 | rexlimiv 3148 |
. . . . . . . . . . . 12
⊢
(∃𝑣 ∈
ω 𝑧 ∈ (𝐻‘𝑣) → (ℵ‘𝑧) ∈ ∪ (𝐻 “
ω)) |
| 35 | 15, 34 | sylbi 217 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ∪ (𝐻
“ ω) → (ℵ‘𝑧) ∈ ∪ (𝐻 “
ω)) |
| 36 | | eleq2 2830 |
. . . . . . . . . . . 12
⊢ (∪ (𝐻
“ ω) = (ℵ‘𝑧) → (𝑧 ∈ ∪ (𝐻 “ ω) ↔ 𝑧 ∈ (ℵ‘𝑧))) |
| 37 | | eleq2 2830 |
. . . . . . . . . . . 12
⊢ (∪ (𝐻
“ ω) = (ℵ‘𝑧) → ((ℵ‘𝑧) ∈ ∪ (𝐻 “ ω) ↔
(ℵ‘𝑧) ∈
(ℵ‘𝑧))) |
| 38 | 36, 37 | imbi12d 344 |
. . . . . . . . . . 11
⊢ (∪ (𝐻
“ ω) = (ℵ‘𝑧) → ((𝑧 ∈ ∪ (𝐻 “ ω) →
(ℵ‘𝑧) ∈
∪ (𝐻 “ ω)) ↔ (𝑧 ∈ (ℵ‘𝑧) → (ℵ‘𝑧) ∈ (ℵ‘𝑧)))) |
| 39 | 35, 38 | mpbii 233 |
. . . . . . . . . 10
⊢ (∪ (𝐻
“ ω) = (ℵ‘𝑧) → (𝑧 ∈ (ℵ‘𝑧) → (ℵ‘𝑧) ∈ (ℵ‘𝑧))) |
| 40 | 9, 39 | mtoi 199 |
. . . . . . . . 9
⊢ (∪ (𝐻
“ ω) = (ℵ‘𝑧) → ¬ 𝑧 ∈ (ℵ‘𝑧)) |
| 41 | 7, 40 | anim12i 613 |
. . . . . . . 8
⊢ ((𝑧 ∈ On ∧ ∪ (𝐻
“ ω) = (ℵ‘𝑧)) → (𝑧 ⊆ (ℵ‘𝑧) ∧ ¬ 𝑧 ∈ (ℵ‘𝑧))) |
| 42 | | eloni 6394 |
. . . . . . . . . 10
⊢ (𝑧 ∈ On → Ord 𝑧) |
| 43 | 8 | onordi 6495 |
. . . . . . . . . 10
⊢ Ord
(ℵ‘𝑧) |
| 44 | | ordtri4 6421 |
. . . . . . . . . 10
⊢ ((Ord
𝑧 ∧ Ord
(ℵ‘𝑧)) →
(𝑧 = (ℵ‘𝑧) ↔ (𝑧 ⊆ (ℵ‘𝑧) ∧ ¬ 𝑧 ∈ (ℵ‘𝑧)))) |
| 45 | 42, 43, 44 | sylancl 586 |
. . . . . . . . 9
⊢ (𝑧 ∈ On → (𝑧 = (ℵ‘𝑧) ↔ (𝑧 ⊆ (ℵ‘𝑧) ∧ ¬ 𝑧 ∈ (ℵ‘𝑧)))) |
| 46 | 45 | adantr 480 |
. . . . . . . 8
⊢ ((𝑧 ∈ On ∧ ∪ (𝐻
“ ω) = (ℵ‘𝑧)) → (𝑧 = (ℵ‘𝑧) ↔ (𝑧 ⊆ (ℵ‘𝑧) ∧ ¬ 𝑧 ∈ (ℵ‘𝑧)))) |
| 47 | 41, 46 | mpbird 257 |
. . . . . . 7
⊢ ((𝑧 ∈ On ∧ ∪ (𝐻
“ ω) = (ℵ‘𝑧)) → 𝑧 = (ℵ‘𝑧)) |
| 48 | | eqeq2 2749 |
. . . . . . . 8
⊢ (∪ (𝐻
“ ω) = (ℵ‘𝑧) → (𝑧 = ∪ (𝐻 “ ω) ↔ 𝑧 = (ℵ‘𝑧))) |
| 49 | 48 | adantl 481 |
. . . . . . 7
⊢ ((𝑧 ∈ On ∧ ∪ (𝐻
“ ω) = (ℵ‘𝑧)) → (𝑧 = ∪ (𝐻 “ ω) ↔ 𝑧 = (ℵ‘𝑧))) |
| 50 | 47, 49 | mpbird 257 |
. . . . . 6
⊢ ((𝑧 ∈ On ∧ ∪ (𝐻
“ ω) = (ℵ‘𝑧)) → 𝑧 = ∪ (𝐻 “
ω)) |
| 51 | 50 | eqcomd 2743 |
. . . . 5
⊢ ((𝑧 ∈ On ∧ ∪ (𝐻
“ ω) = (ℵ‘𝑧)) → ∪ (𝐻 “ ω) = 𝑧) |
| 52 | 51 | fveq2d 6910 |
. . . 4
⊢ ((𝑧 ∈ On ∧ ∪ (𝐻
“ ω) = (ℵ‘𝑧)) → (ℵ‘∪ (𝐻
“ ω)) = (ℵ‘𝑧)) |
| 53 | | eqeq2 2749 |
. . . . 5
⊢ (∪ (𝐻
“ ω) = (ℵ‘𝑧) → ((ℵ‘∪ (𝐻
“ ω)) = ∪ (𝐻 “ ω) ↔
(ℵ‘∪ (𝐻 “ ω)) = (ℵ‘𝑧))) |
| 54 | 53 | adantl 481 |
. . . 4
⊢ ((𝑧 ∈ On ∧ ∪ (𝐻
“ ω) = (ℵ‘𝑧)) → ((ℵ‘∪ (𝐻
“ ω)) = ∪ (𝐻 “ ω) ↔
(ℵ‘∪ (𝐻 “ ω)) = (ℵ‘𝑧))) |
| 55 | 52, 54 | mpbird 257 |
. . 3
⊢ ((𝑧 ∈ On ∧ ∪ (𝐻
“ ω) = (ℵ‘𝑧)) → (ℵ‘∪ (𝐻
“ ω)) = ∪ (𝐻 “ ω)) |
| 56 | 55 | rexlimiva 3147 |
. 2
⊢
(∃𝑧 ∈ On
∪ (𝐻 “ ω) = (ℵ‘𝑧) → (ℵ‘∪ (𝐻
“ ω)) = ∪ (𝐻 “ ω)) |
| 57 | 2, 6, 56 | mp2b 10 |
1
⊢
(ℵ‘∪ (𝐻 “ ω)) = ∪ (𝐻
“ ω) |