| Step | Hyp | Ref
| Expression |
| 1 | | ovex 7464 |
. . . . . . . . 9
⊢ (𝐵 ↑m
(ℵ‘𝐴)) ∈
V |
| 2 | 1 | cardid 10587 |
. . . . . . . 8
⊢
(card‘(𝐵
↑m (ℵ‘𝐴))) ≈ (𝐵 ↑m (ℵ‘𝐴)) |
| 3 | 2 | ensymi 9044 |
. . . . . . 7
⊢ (𝐵 ↑m
(ℵ‘𝐴)) ≈
(card‘(𝐵
↑m (ℵ‘𝐴))) |
| 4 | | fvex 6919 |
. . . . . . . . . . . . . 14
⊢
(ℵ‘𝐴)
∈ V |
| 5 | 4 | canth2 9170 |
. . . . . . . . . . . . 13
⊢
(ℵ‘𝐴)
≺ 𝒫 (ℵ‘𝐴) |
| 6 | 4 | pw2en 9119 |
. . . . . . . . . . . . 13
⊢ 𝒫
(ℵ‘𝐴) ≈
(2o ↑m (ℵ‘𝐴)) |
| 7 | | sdomentr 9151 |
. . . . . . . . . . . . 13
⊢
(((ℵ‘𝐴)
≺ 𝒫 (ℵ‘𝐴) ∧ 𝒫 (ℵ‘𝐴) ≈ (2o
↑m (ℵ‘𝐴))) → (ℵ‘𝐴) ≺ (2o ↑m
(ℵ‘𝐴))) |
| 8 | 5, 6, 7 | mp2an 692 |
. . . . . . . . . . . 12
⊢
(ℵ‘𝐴)
≺ (2o ↑m (ℵ‘𝐴)) |
| 9 | | mapdom1 9182 |
. . . . . . . . . . . 12
⊢
(2o ≼ 𝐵 → (2o ↑m
(ℵ‘𝐴)) ≼
(𝐵 ↑m
(ℵ‘𝐴))) |
| 10 | | sdomdomtr 9150 |
. . . . . . . . . . . 12
⊢
(((ℵ‘𝐴)
≺ (2o ↑m (ℵ‘𝐴)) ∧ (2o ↑m
(ℵ‘𝐴)) ≼
(𝐵 ↑m
(ℵ‘𝐴))) →
(ℵ‘𝐴) ≺
(𝐵 ↑m
(ℵ‘𝐴))) |
| 11 | 8, 9, 10 | sylancr 587 |
. . . . . . . . . . 11
⊢
(2o ≼ 𝐵 → (ℵ‘𝐴) ≺ (𝐵 ↑m (ℵ‘𝐴))) |
| 12 | | ficard 10605 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ↑m
(ℵ‘𝐴)) ∈ V
→ ((𝐵
↑m (ℵ‘𝐴)) ∈ Fin ↔ (card‘(𝐵 ↑m
(ℵ‘𝐴))) ∈
ω)) |
| 13 | 1, 12 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ↑m
(ℵ‘𝐴)) ∈
Fin ↔ (card‘(𝐵
↑m (ℵ‘𝐴))) ∈ ω) |
| 14 | | fict 9693 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ↑m
(ℵ‘𝐴)) ∈
Fin → (𝐵
↑m (ℵ‘𝐴)) ≼ ω) |
| 15 | 13, 14 | sylbir 235 |
. . . . . . . . . . . . . . 15
⊢
((card‘(𝐵
↑m (ℵ‘𝐴))) ∈ ω → (𝐵 ↑m (ℵ‘𝐴)) ≼
ω) |
| 16 | | alephgeom 10122 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ On ↔ ω
⊆ (ℵ‘𝐴)) |
| 17 | | alephon 10109 |
. . . . . . . . . . . . . . . . 17
⊢
(ℵ‘𝐴)
∈ On |
| 18 | | ssdomg 9040 |
. . . . . . . . . . . . . . . . 17
⊢
((ℵ‘𝐴)
∈ On → (ω ⊆ (ℵ‘𝐴) → ω ≼
(ℵ‘𝐴))) |
| 19 | 17, 18 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (ω
⊆ (ℵ‘𝐴)
→ ω ≼ (ℵ‘𝐴)) |
| 20 | 16, 19 | sylbi 217 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ On → ω
≼ (ℵ‘𝐴)) |
| 21 | | domtr 9047 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ↑m
(ℵ‘𝐴)) ≼
ω ∧ ω ≼ (ℵ‘𝐴)) → (𝐵 ↑m (ℵ‘𝐴)) ≼ (ℵ‘𝐴)) |
| 22 | 15, 20, 21 | syl2an 596 |
. . . . . . . . . . . . . 14
⊢
(((card‘(𝐵
↑m (ℵ‘𝐴))) ∈ ω ∧ 𝐴 ∈ On) → (𝐵 ↑m (ℵ‘𝐴)) ≼ (ℵ‘𝐴)) |
| 23 | | domnsym 9139 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ↑m
(ℵ‘𝐴)) ≼
(ℵ‘𝐴) →
¬ (ℵ‘𝐴)
≺ (𝐵
↑m (ℵ‘𝐴))) |
| 24 | 22, 23 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((card‘(𝐵
↑m (ℵ‘𝐴))) ∈ ω ∧ 𝐴 ∈ On) → ¬
(ℵ‘𝐴) ≺
(𝐵 ↑m
(ℵ‘𝐴))) |
| 25 | 24 | expcom 413 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ On →
((card‘(𝐵
↑m (ℵ‘𝐴))) ∈ ω → ¬
(ℵ‘𝐴) ≺
(𝐵 ↑m
(ℵ‘𝐴)))) |
| 26 | 25 | con2d 134 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ On →
((ℵ‘𝐴) ≺
(𝐵 ↑m
(ℵ‘𝐴)) →
¬ (card‘(𝐵
↑m (ℵ‘𝐴))) ∈ ω)) |
| 27 | | cardidm 9999 |
. . . . . . . . . . . 12
⊢
(card‘(card‘(𝐵 ↑m (ℵ‘𝐴)))) = (card‘(𝐵 ↑m
(ℵ‘𝐴))) |
| 28 | | iscard3 10133 |
. . . . . . . . . . . . 13
⊢
((card‘(card‘(𝐵 ↑m (ℵ‘𝐴)))) = (card‘(𝐵 ↑m
(ℵ‘𝐴))) ↔
(card‘(𝐵
↑m (ℵ‘𝐴))) ∈ (ω ∪ ran
ℵ)) |
| 29 | | elun 4153 |
. . . . . . . . . . . . 13
⊢
((card‘(𝐵
↑m (ℵ‘𝐴))) ∈ (ω ∪ ran ℵ)
↔ ((card‘(𝐵
↑m (ℵ‘𝐴))) ∈ ω ∨ (card‘(𝐵 ↑m
(ℵ‘𝐴))) ∈
ran ℵ)) |
| 30 | | df-or 849 |
. . . . . . . . . . . . 13
⊢
(((card‘(𝐵
↑m (ℵ‘𝐴))) ∈ ω ∨ (card‘(𝐵 ↑m
(ℵ‘𝐴))) ∈
ran ℵ) ↔ (¬ (card‘(𝐵 ↑m (ℵ‘𝐴))) ∈ ω →
(card‘(𝐵
↑m (ℵ‘𝐴))) ∈ ran ℵ)) |
| 31 | 28, 29, 30 | 3bitri 297 |
. . . . . . . . . . . 12
⊢
((card‘(card‘(𝐵 ↑m (ℵ‘𝐴)))) = (card‘(𝐵 ↑m
(ℵ‘𝐴))) ↔
(¬ (card‘(𝐵
↑m (ℵ‘𝐴))) ∈ ω → (card‘(𝐵 ↑m
(ℵ‘𝐴))) ∈
ran ℵ)) |
| 32 | 27, 31 | mpbi 230 |
. . . . . . . . . . 11
⊢ (¬
(card‘(𝐵
↑m (ℵ‘𝐴))) ∈ ω → (card‘(𝐵 ↑m
(ℵ‘𝐴))) ∈
ran ℵ) |
| 33 | 11, 26, 32 | syl56 36 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On → (2o
≼ 𝐵 →
(card‘(𝐵
↑m (ℵ‘𝐴))) ∈ ran ℵ)) |
| 34 | | alephfnon 10105 |
. . . . . . . . . . 11
⊢ ℵ
Fn On |
| 35 | | fvelrnb 6969 |
. . . . . . . . . . 11
⊢ (ℵ
Fn On → ((card‘(𝐵 ↑m (ℵ‘𝐴))) ∈ ran ℵ ↔
∃𝑥 ∈ On
(ℵ‘𝑥) =
(card‘(𝐵
↑m (ℵ‘𝐴))))) |
| 36 | 34, 35 | ax-mp 5 |
. . . . . . . . . 10
⊢
((card‘(𝐵
↑m (ℵ‘𝐴))) ∈ ran ℵ ↔ ∃𝑥 ∈ On (ℵ‘𝑥) = (card‘(𝐵 ↑m
(ℵ‘𝐴)))) |
| 37 | 33, 36 | imbitrdi 251 |
. . . . . . . . 9
⊢ (𝐴 ∈ On → (2o
≼ 𝐵 →
∃𝑥 ∈ On
(ℵ‘𝑥) =
(card‘(𝐵
↑m (ℵ‘𝐴))))) |
| 38 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈
(cf‘(ℵ‘𝑥)) ↦ (har‘(𝑧‘𝑦))) = (𝑦 ∈ (cf‘(ℵ‘𝑥)) ↦ (har‘(𝑧‘𝑦))) |
| 39 | 38 | pwcfsdom 10623 |
. . . . . . . . . . 11
⊢
(ℵ‘𝑥)
≺ ((ℵ‘𝑥)
↑m (cf‘(ℵ‘𝑥))) |
| 40 | | id 22 |
. . . . . . . . . . . 12
⊢
((ℵ‘𝑥) =
(card‘(𝐵
↑m (ℵ‘𝐴))) → (ℵ‘𝑥) = (card‘(𝐵 ↑m (ℵ‘𝐴)))) |
| 41 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢
((ℵ‘𝑥) =
(card‘(𝐵
↑m (ℵ‘𝐴))) → (cf‘(ℵ‘𝑥)) =
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴))))) |
| 42 | 40, 41 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢
((ℵ‘𝑥) =
(card‘(𝐵
↑m (ℵ‘𝐴))) → ((ℵ‘𝑥) ↑m
(cf‘(ℵ‘𝑥))) = ((card‘(𝐵 ↑m (ℵ‘𝐴))) ↑m
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴)))))) |
| 43 | 40, 42 | breq12d 5156 |
. . . . . . . . . . 11
⊢
((ℵ‘𝑥) =
(card‘(𝐵
↑m (ℵ‘𝐴))) → ((ℵ‘𝑥) ≺ ((ℵ‘𝑥) ↑m
(cf‘(ℵ‘𝑥))) ↔ (card‘(𝐵 ↑m (ℵ‘𝐴))) ≺ ((card‘(𝐵 ↑m
(ℵ‘𝐴)))
↑m (cf‘(card‘(𝐵 ↑m (ℵ‘𝐴))))))) |
| 44 | 39, 43 | mpbii 233 |
. . . . . . . . . 10
⊢
((ℵ‘𝑥) =
(card‘(𝐵
↑m (ℵ‘𝐴))) → (card‘(𝐵 ↑m (ℵ‘𝐴))) ≺ ((card‘(𝐵 ↑m
(ℵ‘𝐴)))
↑m (cf‘(card‘(𝐵 ↑m (ℵ‘𝐴)))))) |
| 45 | 44 | rexlimivw 3151 |
. . . . . . . . 9
⊢
(∃𝑥 ∈ On
(ℵ‘𝑥) =
(card‘(𝐵
↑m (ℵ‘𝐴))) → (card‘(𝐵 ↑m (ℵ‘𝐴))) ≺ ((card‘(𝐵 ↑m
(ℵ‘𝐴)))
↑m (cf‘(card‘(𝐵 ↑m (ℵ‘𝐴)))))) |
| 46 | 37, 45 | syl6 35 |
. . . . . . . 8
⊢ (𝐴 ∈ On → (2o
≼ 𝐵 →
(card‘(𝐵
↑m (ℵ‘𝐴))) ≺ ((card‘(𝐵 ↑m (ℵ‘𝐴))) ↑m
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴))))))) |
| 47 | 46 | imp 406 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 2o
≼ 𝐵) →
(card‘(𝐵
↑m (ℵ‘𝐴))) ≺ ((card‘(𝐵 ↑m (ℵ‘𝐴))) ↑m
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴)))))) |
| 48 | | ensdomtr 9153 |
. . . . . . 7
⊢ (((𝐵 ↑m
(ℵ‘𝐴)) ≈
(card‘(𝐵
↑m (ℵ‘𝐴))) ∧ (card‘(𝐵 ↑m (ℵ‘𝐴))) ≺ ((card‘(𝐵 ↑m
(ℵ‘𝐴)))
↑m (cf‘(card‘(𝐵 ↑m (ℵ‘𝐴)))))) → (𝐵 ↑m (ℵ‘𝐴)) ≺ ((card‘(𝐵 ↑m
(ℵ‘𝐴)))
↑m (cf‘(card‘(𝐵 ↑m (ℵ‘𝐴)))))) |
| 49 | 3, 47, 48 | sylancr 587 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 2o
≼ 𝐵) → (𝐵 ↑m
(ℵ‘𝐴)) ≺
((card‘(𝐵
↑m (ℵ‘𝐴))) ↑m
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴)))))) |
| 50 | | fvex 6919 |
. . . . . . . . 9
⊢
(cf‘(card‘(𝐵 ↑m (ℵ‘𝐴)))) ∈ V |
| 51 | 50 | enref 9025 |
. . . . . . . 8
⊢
(cf‘(card‘(𝐵 ↑m (ℵ‘𝐴)))) ≈
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴)))) |
| 52 | | mapen 9181 |
. . . . . . . 8
⊢
(((card‘(𝐵
↑m (ℵ‘𝐴))) ≈ (𝐵 ↑m (ℵ‘𝐴)) ∧
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴)))) ≈ (cf‘(card‘(𝐵 ↑m
(ℵ‘𝐴)))))
→ ((card‘(𝐵
↑m (ℵ‘𝐴))) ↑m
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴))))) ≈ ((𝐵 ↑m (ℵ‘𝐴)) ↑m
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴)))))) |
| 53 | 2, 51, 52 | mp2an 692 |
. . . . . . 7
⊢
((card‘(𝐵
↑m (ℵ‘𝐴))) ↑m
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴))))) ≈ ((𝐵 ↑m (ℵ‘𝐴)) ↑m
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴))))) |
| 54 | | cfpwsdom.1 |
. . . . . . . 8
⊢ 𝐵 ∈ V |
| 55 | | mapxpen 9183 |
. . . . . . . 8
⊢ ((𝐵 ∈ V ∧
(ℵ‘𝐴) ∈ On
∧ (cf‘(card‘(𝐵 ↑m (ℵ‘𝐴)))) ∈ V) → ((𝐵 ↑m
(ℵ‘𝐴))
↑m (cf‘(card‘(𝐵 ↑m (ℵ‘𝐴))))) ≈ (𝐵 ↑m ((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴))))))) |
| 56 | 54, 17, 50, 55 | mp3an 1463 |
. . . . . . 7
⊢ ((𝐵 ↑m
(ℵ‘𝐴))
↑m (cf‘(card‘(𝐵 ↑m (ℵ‘𝐴))))) ≈ (𝐵 ↑m ((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴)))))) |
| 57 | 53, 56 | entri 9048 |
. . . . . 6
⊢
((card‘(𝐵
↑m (ℵ‘𝐴))) ↑m
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴))))) ≈ (𝐵 ↑m ((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴)))))) |
| 58 | | sdomentr 9151 |
. . . . . 6
⊢ (((𝐵 ↑m
(ℵ‘𝐴)) ≺
((card‘(𝐵
↑m (ℵ‘𝐴))) ↑m
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴))))) ∧ ((card‘(𝐵 ↑m (ℵ‘𝐴))) ↑m
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴))))) ≈ (𝐵 ↑m ((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴))))))) → (𝐵 ↑m (ℵ‘𝐴)) ≺ (𝐵 ↑m ((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴))))))) |
| 59 | 49, 57, 58 | sylancl 586 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 2o
≼ 𝐵) → (𝐵 ↑m
(ℵ‘𝐴)) ≺
(𝐵 ↑m
((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴))))))) |
| 60 | 4 | xpdom2 9107 |
. . . . . . . . . 10
⊢
((cf‘(card‘(𝐵 ↑m (ℵ‘𝐴)))) ≼
(ℵ‘𝐴) →
((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴))))) ≼ ((ℵ‘𝐴) × (ℵ‘𝐴))) |
| 61 | 16 | biimpi 216 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ On → ω
⊆ (ℵ‘𝐴)) |
| 62 | | infxpen 10054 |
. . . . . . . . . . 11
⊢
(((ℵ‘𝐴)
∈ On ∧ ω ⊆ (ℵ‘𝐴)) → ((ℵ‘𝐴) × (ℵ‘𝐴)) ≈ (ℵ‘𝐴)) |
| 63 | 17, 61, 62 | sylancr 587 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On →
((ℵ‘𝐴) ×
(ℵ‘𝐴)) ≈
(ℵ‘𝐴)) |
| 64 | | domentr 9053 |
. . . . . . . . . 10
⊢
((((ℵ‘𝐴)
× (cf‘(card‘(𝐵 ↑m (ℵ‘𝐴))))) ≼
((ℵ‘𝐴) ×
(ℵ‘𝐴)) ∧
((ℵ‘𝐴) ×
(ℵ‘𝐴)) ≈
(ℵ‘𝐴)) →
((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴))))) ≼ (ℵ‘𝐴)) |
| 65 | 60, 63, 64 | syl2an 596 |
. . . . . . . . 9
⊢
(((cf‘(card‘(𝐵 ↑m (ℵ‘𝐴)))) ≼
(ℵ‘𝐴) ∧
𝐴 ∈ On) →
((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴))))) ≼ (ℵ‘𝐴)) |
| 66 | | nsuceq0 6467 |
. . . . . . . . . . 11
⊢ suc
1o ≠ ∅ |
| 67 | | dom0 9142 |
. . . . . . . . . . 11
⊢ (suc
1o ≼ ∅ ↔ suc 1o =
∅) |
| 68 | 66, 67 | nemtbir 3038 |
. . . . . . . . . 10
⊢ ¬
suc 1o ≼ ∅ |
| 69 | | df-2o 8507 |
. . . . . . . . . . . . . 14
⊢
2o = suc 1o |
| 70 | 69 | breq1i 5150 |
. . . . . . . . . . . . 13
⊢
(2o ≼ 𝐵 ↔ suc 1o ≼ 𝐵) |
| 71 | | breq2 5147 |
. . . . . . . . . . . . 13
⊢ (𝐵 = ∅ → (suc
1o ≼ 𝐵
↔ suc 1o ≼ ∅)) |
| 72 | 70, 71 | bitrid 283 |
. . . . . . . . . . . 12
⊢ (𝐵 = ∅ → (2o
≼ 𝐵 ↔ suc
1o ≼ ∅)) |
| 73 | 72 | biimpcd 249 |
. . . . . . . . . . 11
⊢
(2o ≼ 𝐵 → (𝐵 = ∅ → suc 1o ≼
∅)) |
| 74 | 73 | adantld 490 |
. . . . . . . . . 10
⊢
(2o ≼ 𝐵 → ((((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑m
(ℵ‘𝐴))))) =
∅ ∧ 𝐵 = ∅)
→ suc 1o ≼ ∅)) |
| 75 | 68, 74 | mtoi 199 |
. . . . . . . . 9
⊢
(2o ≼ 𝐵 → ¬ (((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴))))) = ∅ ∧ 𝐵 = ∅)) |
| 76 | | mapdom2 9188 |
. . . . . . . . 9
⊢
((((ℵ‘𝐴)
× (cf‘(card‘(𝐵 ↑m (ℵ‘𝐴))))) ≼
(ℵ‘𝐴) ∧
¬ (((ℵ‘𝐴)
× (cf‘(card‘(𝐵 ↑m (ℵ‘𝐴))))) = ∅ ∧ 𝐵 = ∅)) → (𝐵 ↑m
((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴)))))) ≼ (𝐵 ↑m (ℵ‘𝐴))) |
| 77 | 65, 75, 76 | syl2an 596 |
. . . . . . . 8
⊢
((((cf‘(card‘(𝐵 ↑m (ℵ‘𝐴)))) ≼
(ℵ‘𝐴) ∧
𝐴 ∈ On) ∧
2o ≼ 𝐵)
→ (𝐵
↑m ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑m
(ℵ‘𝐴))))))
≼ (𝐵
↑m (ℵ‘𝐴))) |
| 78 | | domnsym 9139 |
. . . . . . . 8
⊢ ((𝐵 ↑m
((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴)))))) ≼ (𝐵 ↑m (ℵ‘𝐴)) → ¬ (𝐵 ↑m
(ℵ‘𝐴)) ≺
(𝐵 ↑m
((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴))))))) |
| 79 | 77, 78 | syl 17 |
. . . . . . 7
⊢
((((cf‘(card‘(𝐵 ↑m (ℵ‘𝐴)))) ≼
(ℵ‘𝐴) ∧
𝐴 ∈ On) ∧
2o ≼ 𝐵)
→ ¬ (𝐵
↑m (ℵ‘𝐴)) ≺ (𝐵 ↑m ((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴))))))) |
| 80 | 79 | expl 457 |
. . . . . 6
⊢
((cf‘(card‘(𝐵 ↑m (ℵ‘𝐴)))) ≼
(ℵ‘𝐴) →
((𝐴 ∈ On ∧
2o ≼ 𝐵)
→ ¬ (𝐵
↑m (ℵ‘𝐴)) ≺ (𝐵 ↑m ((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴)))))))) |
| 81 | 80 | com12 32 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 2o
≼ 𝐵) →
((cf‘(card‘(𝐵
↑m (ℵ‘𝐴)))) ≼ (ℵ‘𝐴) → ¬ (𝐵 ↑m
(ℵ‘𝐴)) ≺
(𝐵 ↑m
((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴)))))))) |
| 82 | 59, 81 | mt2d 136 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 2o
≼ 𝐵) → ¬
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴)))) ≼ (ℵ‘𝐴)) |
| 83 | | domtri 10596 |
. . . . . 6
⊢
(((cf‘(card‘(𝐵 ↑m (ℵ‘𝐴)))) ∈ V ∧
(ℵ‘𝐴) ∈ V)
→ ((cf‘(card‘(𝐵 ↑m (ℵ‘𝐴)))) ≼
(ℵ‘𝐴) ↔
¬ (ℵ‘𝐴)
≺ (cf‘(card‘(𝐵 ↑m (ℵ‘𝐴)))))) |
| 84 | 50, 4, 83 | mp2an 692 |
. . . . 5
⊢
((cf‘(card‘(𝐵 ↑m (ℵ‘𝐴)))) ≼
(ℵ‘𝐴) ↔
¬ (ℵ‘𝐴)
≺ (cf‘(card‘(𝐵 ↑m (ℵ‘𝐴))))) |
| 85 | 84 | biimpri 228 |
. . . 4
⊢ (¬
(ℵ‘𝐴) ≺
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴)))) → (cf‘(card‘(𝐵 ↑m
(ℵ‘𝐴))))
≼ (ℵ‘𝐴)) |
| 86 | 82, 85 | nsyl2 141 |
. . 3
⊢ ((𝐴 ∈ On ∧ 2o
≼ 𝐵) →
(ℵ‘𝐴) ≺
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴))))) |
| 87 | 86 | ex 412 |
. 2
⊢ (𝐴 ∈ On → (2o
≼ 𝐵 →
(ℵ‘𝐴) ≺
(cf‘(card‘(𝐵
↑m (ℵ‘𝐴)))))) |
| 88 | | fndm 6671 |
. . . . . 6
⊢ (ℵ
Fn On → dom ℵ = On) |
| 89 | 34, 88 | ax-mp 5 |
. . . . 5
⊢ dom
ℵ = On |
| 90 | 89 | eleq2i 2833 |
. . . 4
⊢ (𝐴 ∈ dom ℵ ↔ 𝐴 ∈ On) |
| 91 | | ndmfv 6941 |
. . . 4
⊢ (¬
𝐴 ∈ dom ℵ →
(ℵ‘𝐴) =
∅) |
| 92 | 90, 91 | sylnbir 331 |
. . 3
⊢ (¬
𝐴 ∈ On →
(ℵ‘𝐴) =
∅) |
| 93 | | 1n0 8526 |
. . . . . 6
⊢
1o ≠ ∅ |
| 94 | | 1oex 8516 |
. . . . . . 7
⊢
1o ∈ V |
| 95 | 94 | 0sdom 9147 |
. . . . . 6
⊢ (∅
≺ 1o ↔ 1o ≠ ∅) |
| 96 | 93, 95 | mpbir 231 |
. . . . 5
⊢ ∅
≺ 1o |
| 97 | | id 22 |
. . . . . 6
⊢
((ℵ‘𝐴) =
∅ → (ℵ‘𝐴) = ∅) |
| 98 | | oveq2 7439 |
. . . . . . . . . . 11
⊢
((ℵ‘𝐴) =
∅ → (𝐵
↑m (ℵ‘𝐴)) = (𝐵 ↑m
∅)) |
| 99 | | map0e 8922 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ V → (𝐵 ↑m ∅) =
1o) |
| 100 | 54, 99 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝐵 ↑m ∅) =
1o |
| 101 | 98, 100 | eqtrdi 2793 |
. . . . . . . . . 10
⊢
((ℵ‘𝐴) =
∅ → (𝐵
↑m (ℵ‘𝐴)) = 1o) |
| 102 | 101 | fveq2d 6910 |
. . . . . . . . 9
⊢
((ℵ‘𝐴) =
∅ → (card‘(𝐵 ↑m (ℵ‘𝐴))) =
(card‘1o)) |
| 103 | | 1onn 8678 |
. . . . . . . . . 10
⊢
1o ∈ ω |
| 104 | | cardnn 10003 |
. . . . . . . . . 10
⊢
(1o ∈ ω → (card‘1o) =
1o) |
| 105 | 103, 104 | ax-mp 5 |
. . . . . . . . 9
⊢
(card‘1o) = 1o |
| 106 | 102, 105 | eqtrdi 2793 |
. . . . . . . 8
⊢
((ℵ‘𝐴) =
∅ → (card‘(𝐵 ↑m (ℵ‘𝐴))) =
1o) |
| 107 | 106 | fveq2d 6910 |
. . . . . . 7
⊢
((ℵ‘𝐴) =
∅ → (cf‘(card‘(𝐵 ↑m (ℵ‘𝐴)))) =
(cf‘1o)) |
| 108 | | df-1o 8506 |
. . . . . . . . 9
⊢
1o = suc ∅ |
| 109 | 108 | fveq2i 6909 |
. . . . . . . 8
⊢
(cf‘1o) = (cf‘suc ∅) |
| 110 | | 0elon 6438 |
. . . . . . . . 9
⊢ ∅
∈ On |
| 111 | | cfsuc 10297 |
. . . . . . . . 9
⊢ (∅
∈ On → (cf‘suc ∅) = 1o) |
| 112 | 110, 111 | ax-mp 5 |
. . . . . . . 8
⊢
(cf‘suc ∅) = 1o |
| 113 | 109, 112 | eqtri 2765 |
. . . . . . 7
⊢
(cf‘1o) = 1o |
| 114 | 107, 113 | eqtrdi 2793 |
. . . . . 6
⊢
((ℵ‘𝐴) =
∅ → (cf‘(card‘(𝐵 ↑m (ℵ‘𝐴)))) =
1o) |
| 115 | 97, 114 | breq12d 5156 |
. . . . 5
⊢
((ℵ‘𝐴) =
∅ → ((ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑m
(ℵ‘𝐴)))) ↔
∅ ≺ 1o)) |
| 116 | 96, 115 | mpbiri 258 |
. . . 4
⊢
((ℵ‘𝐴) =
∅ → (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑m
(ℵ‘𝐴))))) |
| 117 | 116 | a1d 25 |
. . 3
⊢
((ℵ‘𝐴) =
∅ → (2o ≼ 𝐵 → (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑m
(ℵ‘𝐴)))))) |
| 118 | 92, 117 | syl 17 |
. 2
⊢ (¬
𝐴 ∈ On →
(2o ≼ 𝐵
→ (ℵ‘𝐴)
≺ (cf‘(card‘(𝐵 ↑m (ℵ‘𝐴)))))) |
| 119 | 87, 118 | pm2.61i 182 |
1
⊢
(2o ≼ 𝐵 → (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑m
(ℵ‘𝐴))))) |