Step | Hyp | Ref
| Expression |
1 | | ovex 7048 |
. . . . . . . . 9
⊢ (𝐵 ↑𝑚
(ℵ‘𝐴)) ∈
V |
2 | 1 | cardid 9815 |
. . . . . . . 8
⊢
(card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ≈ (𝐵 ↑𝑚
(ℵ‘𝐴)) |
3 | 2 | ensymi 8407 |
. . . . . . 7
⊢ (𝐵 ↑𝑚
(ℵ‘𝐴)) ≈
(card‘(𝐵
↑𝑚 (ℵ‘𝐴))) |
4 | | fvex 6551 |
. . . . . . . . . . . . . 14
⊢
(ℵ‘𝐴)
∈ V |
5 | 4 | canth2 8517 |
. . . . . . . . . . . . 13
⊢
(ℵ‘𝐴)
≺ 𝒫 (ℵ‘𝐴) |
6 | 4 | pw2en 8471 |
. . . . . . . . . . . . 13
⊢ 𝒫
(ℵ‘𝐴) ≈
(2o ↑𝑚 (ℵ‘𝐴)) |
7 | | sdomentr 8498 |
. . . . . . . . . . . . 13
⊢
(((ℵ‘𝐴)
≺ 𝒫 (ℵ‘𝐴) ∧ 𝒫 (ℵ‘𝐴) ≈ (2o
↑𝑚 (ℵ‘𝐴))) → (ℵ‘𝐴) ≺ (2o
↑𝑚 (ℵ‘𝐴))) |
8 | 5, 6, 7 | mp2an 688 |
. . . . . . . . . . . 12
⊢
(ℵ‘𝐴)
≺ (2o ↑𝑚 (ℵ‘𝐴)) |
9 | | mapdom1 8529 |
. . . . . . . . . . . 12
⊢
(2o ≼ 𝐵 → (2o
↑𝑚 (ℵ‘𝐴)) ≼ (𝐵 ↑𝑚
(ℵ‘𝐴))) |
10 | | sdomdomtr 8497 |
. . . . . . . . . . . 12
⊢
(((ℵ‘𝐴)
≺ (2o ↑𝑚 (ℵ‘𝐴)) ∧ (2o
↑𝑚 (ℵ‘𝐴)) ≼ (𝐵 ↑𝑚
(ℵ‘𝐴))) →
(ℵ‘𝐴) ≺
(𝐵
↑𝑚 (ℵ‘𝐴))) |
11 | 8, 9, 10 | sylancr 587 |
. . . . . . . . . . 11
⊢
(2o ≼ 𝐵 → (ℵ‘𝐴) ≺ (𝐵 ↑𝑚
(ℵ‘𝐴))) |
12 | | ficard 9833 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ↑𝑚
(ℵ‘𝐴)) ∈ V
→ ((𝐵
↑𝑚 (ℵ‘𝐴)) ∈ Fin ↔ (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) ∈
ω)) |
13 | 1, 12 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ↑𝑚
(ℵ‘𝐴)) ∈
Fin ↔ (card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ∈ ω) |
14 | | fict 8962 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ↑𝑚
(ℵ‘𝐴)) ∈
Fin → (𝐵
↑𝑚 (ℵ‘𝐴)) ≼ ω) |
15 | 13, 14 | sylbir 236 |
. . . . . . . . . . . . . . 15
⊢
((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ∈ ω → (𝐵 ↑𝑚
(ℵ‘𝐴)) ≼
ω) |
16 | | alephgeom 9354 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ On ↔ ω
⊆ (ℵ‘𝐴)) |
17 | | alephon 9341 |
. . . . . . . . . . . . . . . . 17
⊢
(ℵ‘𝐴)
∈ On |
18 | | ssdomg 8403 |
. . . . . . . . . . . . . . . . 17
⊢
((ℵ‘𝐴)
∈ On → (ω ⊆ (ℵ‘𝐴) → ω ≼
(ℵ‘𝐴))) |
19 | 17, 18 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (ω
⊆ (ℵ‘𝐴)
→ ω ≼ (ℵ‘𝐴)) |
20 | 16, 19 | sylbi 218 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ On → ω
≼ (ℵ‘𝐴)) |
21 | | domtr 8410 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ↑𝑚
(ℵ‘𝐴)) ≼
ω ∧ ω ≼ (ℵ‘𝐴)) → (𝐵 ↑𝑚
(ℵ‘𝐴)) ≼
(ℵ‘𝐴)) |
22 | 15, 20, 21 | syl2an 595 |
. . . . . . . . . . . . . 14
⊢
(((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ∈ ω ∧ 𝐴 ∈ On) → (𝐵 ↑𝑚
(ℵ‘𝐴)) ≼
(ℵ‘𝐴)) |
23 | | domnsym 8490 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ↑𝑚
(ℵ‘𝐴)) ≼
(ℵ‘𝐴) →
¬ (ℵ‘𝐴)
≺ (𝐵
↑𝑚 (ℵ‘𝐴))) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ∈ ω ∧ 𝐴 ∈ On) → ¬
(ℵ‘𝐴) ≺
(𝐵
↑𝑚 (ℵ‘𝐴))) |
25 | 24 | expcom 414 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ On →
((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ∈ ω → ¬
(ℵ‘𝐴) ≺
(𝐵
↑𝑚 (ℵ‘𝐴)))) |
26 | 25 | con2d 136 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ On →
((ℵ‘𝐴) ≺
(𝐵
↑𝑚 (ℵ‘𝐴)) → ¬ (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) ∈
ω)) |
27 | | cardidm 9234 |
. . . . . . . . . . . 12
⊢
(card‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))) =
(card‘(𝐵
↑𝑚 (ℵ‘𝐴))) |
28 | | iscard3 9365 |
. . . . . . . . . . . . 13
⊢
((card‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))) =
(card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ↔ (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) ∈
(ω ∪ ran ℵ)) |
29 | | elun 4046 |
. . . . . . . . . . . . 13
⊢
((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ∈ (ω ∪ ran ℵ)
↔ ((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ∈ ω ∨ (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) ∈
ran ℵ)) |
30 | | df-or 843 |
. . . . . . . . . . . . 13
⊢
(((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ∈ ω ∨ (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) ∈
ran ℵ) ↔ (¬ (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) ∈
ω → (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) ∈
ran ℵ)) |
31 | 28, 29, 30 | 3bitri 298 |
. . . . . . . . . . . 12
⊢
((card‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))) =
(card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ↔ (¬ (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) ∈
ω → (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) ∈
ran ℵ)) |
32 | 27, 31 | mpbi 231 |
. . . . . . . . . . 11
⊢ (¬
(card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ∈ ω → (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) ∈
ran ℵ) |
33 | 11, 26, 32 | syl56 36 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On → (2o
≼ 𝐵 →
(card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ∈ ran ℵ)) |
34 | | alephfnon 9337 |
. . . . . . . . . . 11
⊢ ℵ
Fn On |
35 | | fvelrnb 6594 |
. . . . . . . . . . 11
⊢ (ℵ
Fn On → ((card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) ∈
ran ℵ ↔ ∃𝑥
∈ On (ℵ‘𝑥)
= (card‘(𝐵
↑𝑚 (ℵ‘𝐴))))) |
36 | 34, 35 | ax-mp 5 |
. . . . . . . . . 10
⊢
((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ∈ ran ℵ ↔ ∃𝑥 ∈ On (ℵ‘𝑥) = (card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))) |
37 | 33, 36 | syl6ib 252 |
. . . . . . . . 9
⊢ (𝐴 ∈ On → (2o
≼ 𝐵 →
∃𝑥 ∈ On
(ℵ‘𝑥) =
(card‘(𝐵
↑𝑚 (ℵ‘𝐴))))) |
38 | | eqid 2795 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈
(cf‘(ℵ‘𝑥)) ↦ (har‘(𝑧‘𝑦))) = (𝑦 ∈ (cf‘(ℵ‘𝑥)) ↦ (har‘(𝑧‘𝑦))) |
39 | 38 | pwcfsdom 9851 |
. . . . . . . . . . 11
⊢
(ℵ‘𝑥)
≺ ((ℵ‘𝑥)
↑𝑚 (cf‘(ℵ‘𝑥))) |
40 | | id 22 |
. . . . . . . . . . . 12
⊢
((ℵ‘𝑥) =
(card‘(𝐵
↑𝑚 (ℵ‘𝐴))) → (ℵ‘𝑥) = (card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))) |
41 | | fveq2 6538 |
. . . . . . . . . . . . 13
⊢
((ℵ‘𝑥) =
(card‘(𝐵
↑𝑚 (ℵ‘𝐴))) → (cf‘(ℵ‘𝑥)) =
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴))))) |
42 | 40, 41 | oveq12d 7034 |
. . . . . . . . . . . 12
⊢
((ℵ‘𝑥) =
(card‘(𝐵
↑𝑚 (ℵ‘𝐴))) → ((ℵ‘𝑥) ↑𝑚
(cf‘(ℵ‘𝑥))) = ((card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))
↑𝑚 (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))))) |
43 | 40, 42 | breq12d 4975 |
. . . . . . . . . . 11
⊢
((ℵ‘𝑥) =
(card‘(𝐵
↑𝑚 (ℵ‘𝐴))) → ((ℵ‘𝑥) ≺ ((ℵ‘𝑥) ↑𝑚
(cf‘(ℵ‘𝑥))) ↔ (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) ≺
((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ↑𝑚
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴))))))) |
44 | 39, 43 | mpbii 234 |
. . . . . . . . . 10
⊢
((ℵ‘𝑥) =
(card‘(𝐵
↑𝑚 (ℵ‘𝐴))) → (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) ≺
((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ↑𝑚
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴)))))) |
45 | 44 | rexlimivw 3245 |
. . . . . . . . 9
⊢
(∃𝑥 ∈ On
(ℵ‘𝑥) =
(card‘(𝐵
↑𝑚 (ℵ‘𝐴))) → (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) ≺
((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ↑𝑚
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴)))))) |
46 | 37, 45 | syl6 35 |
. . . . . . . 8
⊢ (𝐴 ∈ On → (2o
≼ 𝐵 →
(card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ≺ ((card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))
↑𝑚 (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))))) |
47 | 46 | imp 407 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 2o
≼ 𝐵) →
(card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ≺ ((card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))
↑𝑚 (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))))) |
48 | | ensdomtr 8500 |
. . . . . . 7
⊢ (((𝐵 ↑𝑚
(ℵ‘𝐴)) ≈
(card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ∧ (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) ≺
((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ↑𝑚
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴)))))) → (𝐵 ↑𝑚
(ℵ‘𝐴)) ≺
((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ↑𝑚
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴)))))) |
49 | 3, 47, 48 | sylancr 587 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 2o
≼ 𝐵) → (𝐵 ↑𝑚
(ℵ‘𝐴)) ≺
((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ↑𝑚
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴)))))) |
50 | | fvex 6551 |
. . . . . . . . 9
⊢
(cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))) ∈
V |
51 | 50 | enref 8390 |
. . . . . . . 8
⊢
(cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))
≈ (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))) |
52 | | mapen 8528 |
. . . . . . . 8
⊢
(((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ≈ (𝐵 ↑𝑚
(ℵ‘𝐴)) ∧
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴)))) ≈ (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))))
→ ((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ↑𝑚
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴))))) ≈ ((𝐵 ↑𝑚
(ℵ‘𝐴))
↑𝑚 (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))))) |
53 | 2, 51, 52 | mp2an 688 |
. . . . . . 7
⊢
((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ↑𝑚
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴))))) ≈ ((𝐵 ↑𝑚
(ℵ‘𝐴))
↑𝑚 (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))) |
54 | | cfpwsdom.1 |
. . . . . . . 8
⊢ 𝐵 ∈ V |
55 | | mapxpen 8530 |
. . . . . . . 8
⊢ ((𝐵 ∈ V ∧
(ℵ‘𝐴) ∈ On
∧ (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))) ∈
V) → ((𝐵
↑𝑚 (ℵ‘𝐴)) ↑𝑚
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴))))) ≈ (𝐵 ↑𝑚
((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴))))))) |
56 | 54, 17, 50, 55 | mp3an 1453 |
. . . . . . 7
⊢ ((𝐵 ↑𝑚
(ℵ‘𝐴))
↑𝑚 (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))))
≈ (𝐵
↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))))) |
57 | 53, 56 | entri 8411 |
. . . . . 6
⊢
((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ↑𝑚
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴))))) ≈ (𝐵 ↑𝑚
((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴)))))) |
58 | | sdomentr 8498 |
. . . . . 6
⊢ (((𝐵 ↑𝑚
(ℵ‘𝐴)) ≺
((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ↑𝑚
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴))))) ∧ ((card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))
↑𝑚 (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))))
≈ (𝐵
↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))))))
→ (𝐵
↑𝑚 (ℵ‘𝐴)) ≺ (𝐵 ↑𝑚
((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴))))))) |
59 | 49, 57, 58 | sylancl 586 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 2o
≼ 𝐵) → (𝐵 ↑𝑚
(ℵ‘𝐴)) ≺
(𝐵
↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))))) |
60 | 4 | xpdom2 8459 |
. . . . . . . . . 10
⊢
((cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))
≼ (ℵ‘𝐴)
→ ((ℵ‘𝐴)
× (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))))
≼ ((ℵ‘𝐴)
× (ℵ‘𝐴))) |
61 | 16 | biimpi 217 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ On → ω
⊆ (ℵ‘𝐴)) |
62 | | infxpen 9286 |
. . . . . . . . . . 11
⊢
(((ℵ‘𝐴)
∈ On ∧ ω ⊆ (ℵ‘𝐴)) → ((ℵ‘𝐴) × (ℵ‘𝐴)) ≈ (ℵ‘𝐴)) |
63 | 17, 61, 62 | sylancr 587 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On →
((ℵ‘𝐴) ×
(ℵ‘𝐴)) ≈
(ℵ‘𝐴)) |
64 | | domentr 8416 |
. . . . . . . . . 10
⊢
((((ℵ‘𝐴)
× (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))))
≼ ((ℵ‘𝐴)
× (ℵ‘𝐴))
∧ ((ℵ‘𝐴)
× (ℵ‘𝐴))
≈ (ℵ‘𝐴))
→ ((ℵ‘𝐴)
× (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))))
≼ (ℵ‘𝐴)) |
65 | 60, 63, 64 | syl2an 595 |
. . . . . . . . 9
⊢
(((cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))
≼ (ℵ‘𝐴)
∧ 𝐴 ∈ On) →
((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴))))) ≼ (ℵ‘𝐴)) |
66 | | nsuceq0 6146 |
. . . . . . . . . . 11
⊢ suc
1o ≠ ∅ |
67 | | dom0 8492 |
. . . . . . . . . . 11
⊢ (suc
1o ≼ ∅ ↔ suc 1o =
∅) |
68 | 66, 67 | nemtbir 3080 |
. . . . . . . . . 10
⊢ ¬
suc 1o ≼ ∅ |
69 | | df-2o 7954 |
. . . . . . . . . . . . . 14
⊢
2o = suc 1o |
70 | 69 | breq1i 4969 |
. . . . . . . . . . . . 13
⊢
(2o ≼ 𝐵 ↔ suc 1o ≼ 𝐵) |
71 | | breq2 4966 |
. . . . . . . . . . . . 13
⊢ (𝐵 = ∅ → (suc
1o ≼ 𝐵
↔ suc 1o ≼ ∅)) |
72 | 70, 71 | syl5bb 284 |
. . . . . . . . . . . 12
⊢ (𝐵 = ∅ → (2o
≼ 𝐵 ↔ suc
1o ≼ ∅)) |
73 | 72 | biimpcd 250 |
. . . . . . . . . . 11
⊢
(2o ≼ 𝐵 → (𝐵 = ∅ → suc 1o ≼
∅)) |
74 | 73 | adantld 491 |
. . . . . . . . . 10
⊢
(2o ≼ 𝐵 → ((((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))) =
∅ ∧ 𝐵 = ∅)
→ suc 1o ≼ ∅)) |
75 | 68, 74 | mtoi 200 |
. . . . . . . . 9
⊢
(2o ≼ 𝐵 → ¬ (((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴))))) = ∅ ∧ 𝐵 = ∅)) |
76 | | mapdom2 8535 |
. . . . . . . . 9
⊢
((((ℵ‘𝐴)
× (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))))
≼ (ℵ‘𝐴)
∧ ¬ (((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))) =
∅ ∧ 𝐵 = ∅))
→ (𝐵
↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))))
≼ (𝐵
↑𝑚 (ℵ‘𝐴))) |
77 | 65, 75, 76 | syl2an 595 |
. . . . . . . 8
⊢
((((cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))
≼ (ℵ‘𝐴)
∧ 𝐴 ∈ On) ∧
2o ≼ 𝐵)
→ (𝐵
↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))))
≼ (𝐵
↑𝑚 (ℵ‘𝐴))) |
78 | | domnsym 8490 |
. . . . . . . 8
⊢ ((𝐵 ↑𝑚
((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴)))))) ≼ (𝐵 ↑𝑚
(ℵ‘𝐴)) →
¬ (𝐵
↑𝑚 (ℵ‘𝐴)) ≺ (𝐵 ↑𝑚
((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴))))))) |
79 | 77, 78 | syl 17 |
. . . . . . 7
⊢
((((cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))
≼ (ℵ‘𝐴)
∧ 𝐴 ∈ On) ∧
2o ≼ 𝐵)
→ ¬ (𝐵
↑𝑚 (ℵ‘𝐴)) ≺ (𝐵 ↑𝑚
((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴))))))) |
80 | 79 | expl 458 |
. . . . . 6
⊢
((cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))
≼ (ℵ‘𝐴)
→ ((𝐴 ∈ On ∧
2o ≼ 𝐵)
→ ¬ (𝐵
↑𝑚 (ℵ‘𝐴)) ≺ (𝐵 ↑𝑚
((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴)))))))) |
81 | 80 | com12 32 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 2o
≼ 𝐵) →
((cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴)))) ≼ (ℵ‘𝐴) → ¬ (𝐵 ↑𝑚
(ℵ‘𝐴)) ≺
(𝐵
↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))))))) |
82 | 59, 81 | mt2d 138 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 2o
≼ 𝐵) → ¬
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴)))) ≼ (ℵ‘𝐴)) |
83 | | domtri 9824 |
. . . . . 6
⊢
(((cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))) ∈
V ∧ (ℵ‘𝐴)
∈ V) → ((cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))
≼ (ℵ‘𝐴)
↔ ¬ (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))))) |
84 | 50, 4, 83 | mp2an 688 |
. . . . 5
⊢
((cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))
≼ (ℵ‘𝐴)
↔ ¬ (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))) |
85 | 84 | biimpri 229 |
. . . 4
⊢ (¬
(ℵ‘𝐴) ≺
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴)))) → (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))
≼ (ℵ‘𝐴)) |
86 | 82, 85 | nsyl2 143 |
. . 3
⊢ ((𝐴 ∈ On ∧ 2o
≼ 𝐵) →
(ℵ‘𝐴) ≺
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴))))) |
87 | 86 | ex 413 |
. 2
⊢ (𝐴 ∈ On → (2o
≼ 𝐵 →
(ℵ‘𝐴) ≺
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴)))))) |
88 | | fndm 6325 |
. . . . . 6
⊢ (ℵ
Fn On → dom ℵ = On) |
89 | 34, 88 | ax-mp 5 |
. . . . 5
⊢ dom
ℵ = On |
90 | 89 | eleq2i 2874 |
. . . 4
⊢ (𝐴 ∈ dom ℵ ↔ 𝐴 ∈ On) |
91 | | ndmfv 6568 |
. . . 4
⊢ (¬
𝐴 ∈ dom ℵ →
(ℵ‘𝐴) =
∅) |
92 | 90, 91 | sylnbir 332 |
. . 3
⊢ (¬
𝐴 ∈ On →
(ℵ‘𝐴) =
∅) |
93 | | 1n0 7970 |
. . . . . 6
⊢
1o ≠ ∅ |
94 | | 1oex 7961 |
. . . . . . 7
⊢
1o ∈ V |
95 | 94 | 0sdom 8495 |
. . . . . 6
⊢ (∅
≺ 1o ↔ 1o ≠ ∅) |
96 | 93, 95 | mpbir 232 |
. . . . 5
⊢ ∅
≺ 1o |
97 | | id 22 |
. . . . . 6
⊢
((ℵ‘𝐴) =
∅ → (ℵ‘𝐴) = ∅) |
98 | | oveq2 7024 |
. . . . . . . . . . 11
⊢
((ℵ‘𝐴) =
∅ → (𝐵
↑𝑚 (ℵ‘𝐴)) = (𝐵 ↑𝑚
∅)) |
99 | | map0e 8296 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ V → (𝐵 ↑𝑚
∅) = 1o) |
100 | 54, 99 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝐵 ↑𝑚
∅) = 1o |
101 | 98, 100 | syl6eq 2847 |
. . . . . . . . . 10
⊢
((ℵ‘𝐴) =
∅ → (𝐵
↑𝑚 (ℵ‘𝐴)) = 1o) |
102 | 101 | fveq2d 6542 |
. . . . . . . . 9
⊢
((ℵ‘𝐴) =
∅ → (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) =
(card‘1o)) |
103 | | 1onn 8115 |
. . . . . . . . . 10
⊢
1o ∈ ω |
104 | | cardnn 9238 |
. . . . . . . . . 10
⊢
(1o ∈ ω → (card‘1o) =
1o) |
105 | 103, 104 | ax-mp 5 |
. . . . . . . . 9
⊢
(card‘1o) = 1o |
106 | 102, 105 | syl6eq 2847 |
. . . . . . . 8
⊢
((ℵ‘𝐴) =
∅ → (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) =
1o) |
107 | 106 | fveq2d 6542 |
. . . . . . 7
⊢
((ℵ‘𝐴) =
∅ → (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))) =
(cf‘1o)) |
108 | | df-1o 7953 |
. . . . . . . . 9
⊢
1o = suc ∅ |
109 | 108 | fveq2i 6541 |
. . . . . . . 8
⊢
(cf‘1o) = (cf‘suc ∅) |
110 | | 0elon 6119 |
. . . . . . . . 9
⊢ ∅
∈ On |
111 | | cfsuc 9525 |
. . . . . . . . 9
⊢ (∅
∈ On → (cf‘suc ∅) = 1o) |
112 | 110, 111 | ax-mp 5 |
. . . . . . . 8
⊢
(cf‘suc ∅) = 1o |
113 | 109, 112 | eqtri 2819 |
. . . . . . 7
⊢
(cf‘1o) = 1o |
114 | 107, 113 | syl6eq 2847 |
. . . . . 6
⊢
((ℵ‘𝐴) =
∅ → (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))) =
1o) |
115 | 97, 114 | breq12d 4975 |
. . . . 5
⊢
((ℵ‘𝐴) =
∅ → ((ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))) ↔
∅ ≺ 1o)) |
116 | 96, 115 | mpbiri 259 |
. . . 4
⊢
((ℵ‘𝐴) =
∅ → (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))) |
117 | 116 | a1d 25 |
. . 3
⊢
((ℵ‘𝐴) =
∅ → (2o ≼ 𝐵 → (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))))) |
118 | 92, 117 | syl 17 |
. 2
⊢ (¬
𝐴 ∈ On →
(2o ≼ 𝐵
→ (ℵ‘𝐴)
≺ (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))))) |
119 | 87, 118 | pm2.61i 183 |
1
⊢
(2o ≼ 𝐵 → (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))) |