Step | Hyp | Ref
| Expression |
1 | | ovex 6577 |
. . . . . . . . 9
⊢ (𝐵 ↑𝑚
(ℵ‘𝐴)) ∈
V |
2 | 1 | cardid 9248 |
. . . . . . . 8
⊢
(card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ≈ (𝐵 ↑𝑚
(ℵ‘𝐴)) |
3 | 2 | ensymi 7892 |
. . . . . . 7
⊢ (𝐵 ↑𝑚
(ℵ‘𝐴)) ≈
(card‘(𝐵
↑𝑚 (ℵ‘𝐴))) |
4 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢
(ℵ‘𝐴)
∈ V |
5 | 4 | canth2 7998 |
. . . . . . . . . . . . 13
⊢
(ℵ‘𝐴)
≺ 𝒫 (ℵ‘𝐴) |
6 | 4 | pw2en 7952 |
. . . . . . . . . . . . 13
⊢ 𝒫
(ℵ‘𝐴) ≈
(2𝑜 ↑𝑚 (ℵ‘𝐴)) |
7 | | sdomentr 7979 |
. . . . . . . . . . . . 13
⊢
(((ℵ‘𝐴)
≺ 𝒫 (ℵ‘𝐴) ∧ 𝒫 (ℵ‘𝐴) ≈ (2𝑜
↑𝑚 (ℵ‘𝐴))) → (ℵ‘𝐴) ≺ (2𝑜
↑𝑚 (ℵ‘𝐴))) |
8 | 5, 6, 7 | mp2an 704 |
. . . . . . . . . . . 12
⊢
(ℵ‘𝐴)
≺ (2𝑜 ↑𝑚 (ℵ‘𝐴)) |
9 | | mapdom1 8010 |
. . . . . . . . . . . 12
⊢
(2𝑜 ≼ 𝐵 → (2𝑜
↑𝑚 (ℵ‘𝐴)) ≼ (𝐵 ↑𝑚
(ℵ‘𝐴))) |
10 | | sdomdomtr 7978 |
. . . . . . . . . . . 12
⊢
(((ℵ‘𝐴)
≺ (2𝑜 ↑𝑚 (ℵ‘𝐴)) ∧ (2𝑜
↑𝑚 (ℵ‘𝐴)) ≼ (𝐵 ↑𝑚
(ℵ‘𝐴))) →
(ℵ‘𝐴) ≺
(𝐵
↑𝑚 (ℵ‘𝐴))) |
11 | 8, 9, 10 | sylancr 694 |
. . . . . . . . . . 11
⊢
(2𝑜 ≼ 𝐵 → (ℵ‘𝐴) ≺ (𝐵 ↑𝑚
(ℵ‘𝐴))) |
12 | | ficard 9266 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ↑𝑚
(ℵ‘𝐴)) ∈ V
→ ((𝐵
↑𝑚 (ℵ‘𝐴)) ∈ Fin ↔ (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) ∈
ω)) |
13 | 1, 12 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ↑𝑚
(ℵ‘𝐴)) ∈
Fin ↔ (card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ∈ ω) |
14 | | isfinite 8432 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ↑𝑚
(ℵ‘𝐴)) ∈
Fin ↔ (𝐵
↑𝑚 (ℵ‘𝐴)) ≺ ω) |
15 | | sdomdom 7869 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ↑𝑚
(ℵ‘𝐴)) ≺
ω → (𝐵
↑𝑚 (ℵ‘𝐴)) ≼ ω) |
16 | 14, 15 | sylbi 206 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ↑𝑚
(ℵ‘𝐴)) ∈
Fin → (𝐵
↑𝑚 (ℵ‘𝐴)) ≼ ω) |
17 | 13, 16 | sylbir 224 |
. . . . . . . . . . . . . . 15
⊢
((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ∈ ω → (𝐵 ↑𝑚
(ℵ‘𝐴)) ≼
ω) |
18 | | alephgeom 8788 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ On ↔ ω
⊆ (ℵ‘𝐴)) |
19 | | alephon 8775 |
. . . . . . . . . . . . . . . . 17
⊢
(ℵ‘𝐴)
∈ On |
20 | | ssdomg 7887 |
. . . . . . . . . . . . . . . . 17
⊢
((ℵ‘𝐴)
∈ On → (ω ⊆ (ℵ‘𝐴) → ω ≼
(ℵ‘𝐴))) |
21 | 19, 20 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (ω
⊆ (ℵ‘𝐴)
→ ω ≼ (ℵ‘𝐴)) |
22 | 18, 21 | sylbi 206 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ On → ω
≼ (ℵ‘𝐴)) |
23 | | domtr 7895 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ↑𝑚
(ℵ‘𝐴)) ≼
ω ∧ ω ≼ (ℵ‘𝐴)) → (𝐵 ↑𝑚
(ℵ‘𝐴)) ≼
(ℵ‘𝐴)) |
24 | 17, 22, 23 | syl2an 493 |
. . . . . . . . . . . . . 14
⊢
(((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ∈ ω ∧ 𝐴 ∈ On) → (𝐵 ↑𝑚
(ℵ‘𝐴)) ≼
(ℵ‘𝐴)) |
25 | | domnsym 7971 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ↑𝑚
(ℵ‘𝐴)) ≼
(ℵ‘𝐴) →
¬ (ℵ‘𝐴)
≺ (𝐵
↑𝑚 (ℵ‘𝐴))) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ∈ ω ∧ 𝐴 ∈ On) → ¬
(ℵ‘𝐴) ≺
(𝐵
↑𝑚 (ℵ‘𝐴))) |
27 | 26 | expcom 450 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ On →
((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ∈ ω → ¬
(ℵ‘𝐴) ≺
(𝐵
↑𝑚 (ℵ‘𝐴)))) |
28 | 27 | con2d 128 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ On →
((ℵ‘𝐴) ≺
(𝐵
↑𝑚 (ℵ‘𝐴)) → ¬ (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) ∈
ω)) |
29 | | cardidm 8668 |
. . . . . . . . . . . 12
⊢
(card‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))) =
(card‘(𝐵
↑𝑚 (ℵ‘𝐴))) |
30 | | iscard3 8799 |
. . . . . . . . . . . . 13
⊢
((card‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))) =
(card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ↔ (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) ∈
(ω ∪ ran ℵ)) |
31 | | elun 3715 |
. . . . . . . . . . . . 13
⊢
((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ∈ (ω ∪ ran ℵ)
↔ ((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ∈ ω ∨ (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) ∈
ran ℵ)) |
32 | | df-or 384 |
. . . . . . . . . . . . 13
⊢
(((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ∈ ω ∨ (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) ∈
ran ℵ) ↔ (¬ (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) ∈
ω → (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) ∈
ran ℵ)) |
33 | 30, 31, 32 | 3bitri 285 |
. . . . . . . . . . . 12
⊢
((card‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))) =
(card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ↔ (¬ (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) ∈
ω → (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) ∈
ran ℵ)) |
34 | 29, 33 | mpbi 219 |
. . . . . . . . . . 11
⊢ (¬
(card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ∈ ω → (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) ∈
ran ℵ) |
35 | 11, 28, 34 | syl56 35 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On →
(2𝑜 ≼ 𝐵 → (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) ∈
ran ℵ)) |
36 | | alephfnon 8771 |
. . . . . . . . . . 11
⊢ ℵ
Fn On |
37 | | fvelrnb 6153 |
. . . . . . . . . . 11
⊢ (ℵ
Fn On → ((card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) ∈
ran ℵ ↔ ∃𝑥
∈ On (ℵ‘𝑥)
= (card‘(𝐵
↑𝑚 (ℵ‘𝐴))))) |
38 | 36, 37 | ax-mp 5 |
. . . . . . . . . 10
⊢
((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ∈ ran ℵ ↔ ∃𝑥 ∈ On (ℵ‘𝑥) = (card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))) |
39 | 35, 38 | syl6ib 240 |
. . . . . . . . 9
⊢ (𝐴 ∈ On →
(2𝑜 ≼ 𝐵 → ∃𝑥 ∈ On (ℵ‘𝑥) = (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))) |
40 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈
(cf‘(ℵ‘𝑥)) ↦ (har‘(𝑧‘𝑦))) = (𝑦 ∈ (cf‘(ℵ‘𝑥)) ↦ (har‘(𝑧‘𝑦))) |
41 | 40 | pwcfsdom 9284 |
. . . . . . . . . . 11
⊢
(ℵ‘𝑥)
≺ ((ℵ‘𝑥)
↑𝑚 (cf‘(ℵ‘𝑥))) |
42 | | id 22 |
. . . . . . . . . . . 12
⊢
((ℵ‘𝑥) =
(card‘(𝐵
↑𝑚 (ℵ‘𝐴))) → (ℵ‘𝑥) = (card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))) |
43 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢
((ℵ‘𝑥) =
(card‘(𝐵
↑𝑚 (ℵ‘𝐴))) → (cf‘(ℵ‘𝑥)) =
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴))))) |
44 | 42, 43 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢
((ℵ‘𝑥) =
(card‘(𝐵
↑𝑚 (ℵ‘𝐴))) → ((ℵ‘𝑥) ↑𝑚
(cf‘(ℵ‘𝑥))) = ((card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))
↑𝑚 (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))))) |
45 | 42, 44 | breq12d 4596 |
. . . . . . . . . . 11
⊢
((ℵ‘𝑥) =
(card‘(𝐵
↑𝑚 (ℵ‘𝐴))) → ((ℵ‘𝑥) ≺ ((ℵ‘𝑥) ↑𝑚
(cf‘(ℵ‘𝑥))) ↔ (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) ≺
((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ↑𝑚
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴))))))) |
46 | 41, 45 | mpbii 222 |
. . . . . . . . . 10
⊢
((ℵ‘𝑥) =
(card‘(𝐵
↑𝑚 (ℵ‘𝐴))) → (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) ≺
((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ↑𝑚
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴)))))) |
47 | 46 | rexlimivw 3011 |
. . . . . . . . 9
⊢
(∃𝑥 ∈ On
(ℵ‘𝑥) =
(card‘(𝐵
↑𝑚 (ℵ‘𝐴))) → (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) ≺
((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ↑𝑚
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴)))))) |
48 | 39, 47 | syl6 34 |
. . . . . . . 8
⊢ (𝐴 ∈ On →
(2𝑜 ≼ 𝐵 → (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) ≺
((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ↑𝑚
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴))))))) |
49 | 48 | imp 444 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧
2𝑜 ≼ 𝐵) → (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) ≺
((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ↑𝑚
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴)))))) |
50 | | ensdomtr 7981 |
. . . . . . 7
⊢ (((𝐵 ↑𝑚
(ℵ‘𝐴)) ≈
(card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ∧ (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) ≺
((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ↑𝑚
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴)))))) → (𝐵 ↑𝑚
(ℵ‘𝐴)) ≺
((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ↑𝑚
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴)))))) |
51 | 3, 49, 50 | sylancr 694 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧
2𝑜 ≼ 𝐵) → (𝐵 ↑𝑚
(ℵ‘𝐴)) ≺
((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ↑𝑚
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴)))))) |
52 | | fvex 6113 |
. . . . . . . . 9
⊢
(cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))) ∈
V |
53 | 52 | enref 7874 |
. . . . . . . 8
⊢
(cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))
≈ (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))) |
54 | | mapen 8009 |
. . . . . . . 8
⊢
(((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ≈ (𝐵 ↑𝑚
(ℵ‘𝐴)) ∧
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴)))) ≈ (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))))
→ ((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ↑𝑚
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴))))) ≈ ((𝐵 ↑𝑚
(ℵ‘𝐴))
↑𝑚 (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))))) |
55 | 2, 53, 54 | mp2an 704 |
. . . . . . 7
⊢
((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ↑𝑚
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴))))) ≈ ((𝐵 ↑𝑚
(ℵ‘𝐴))
↑𝑚 (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))) |
56 | | cfpwsdom.1 |
. . . . . . . 8
⊢ 𝐵 ∈ V |
57 | | mapxpen 8011 |
. . . . . . . 8
⊢ ((𝐵 ∈ V ∧
(ℵ‘𝐴) ∈ On
∧ (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))) ∈
V) → ((𝐵
↑𝑚 (ℵ‘𝐴)) ↑𝑚
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴))))) ≈ (𝐵 ↑𝑚
((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴))))))) |
58 | 56, 19, 52, 57 | mp3an 1416 |
. . . . . . 7
⊢ ((𝐵 ↑𝑚
(ℵ‘𝐴))
↑𝑚 (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))))
≈ (𝐵
↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))))) |
59 | 55, 58 | entri 7896 |
. . . . . 6
⊢
((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ↑𝑚
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴))))) ≈ (𝐵 ↑𝑚
((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴)))))) |
60 | | sdomentr 7979 |
. . . . . 6
⊢ (((𝐵 ↑𝑚
(ℵ‘𝐴)) ≺
((card‘(𝐵
↑𝑚 (ℵ‘𝐴))) ↑𝑚
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴))))) ∧ ((card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))
↑𝑚 (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))))
≈ (𝐵
↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))))))
→ (𝐵
↑𝑚 (ℵ‘𝐴)) ≺ (𝐵 ↑𝑚
((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴))))))) |
61 | 51, 59, 60 | sylancl 693 |
. . . . 5
⊢ ((𝐴 ∈ On ∧
2𝑜 ≼ 𝐵) → (𝐵 ↑𝑚
(ℵ‘𝐴)) ≺
(𝐵
↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))))) |
62 | 4 | xpdom2 7940 |
. . . . . . . . . 10
⊢
((cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))
≼ (ℵ‘𝐴)
→ ((ℵ‘𝐴)
× (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))))
≼ ((ℵ‘𝐴)
× (ℵ‘𝐴))) |
63 | 18 | biimpi 205 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ On → ω
⊆ (ℵ‘𝐴)) |
64 | | infxpen 8720 |
. . . . . . . . . . 11
⊢
(((ℵ‘𝐴)
∈ On ∧ ω ⊆ (ℵ‘𝐴)) → ((ℵ‘𝐴) × (ℵ‘𝐴)) ≈ (ℵ‘𝐴)) |
65 | 19, 63, 64 | sylancr 694 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On →
((ℵ‘𝐴) ×
(ℵ‘𝐴)) ≈
(ℵ‘𝐴)) |
66 | | domentr 7901 |
. . . . . . . . . 10
⊢
((((ℵ‘𝐴)
× (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))))
≼ ((ℵ‘𝐴)
× (ℵ‘𝐴))
∧ ((ℵ‘𝐴)
× (ℵ‘𝐴))
≈ (ℵ‘𝐴))
→ ((ℵ‘𝐴)
× (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))))
≼ (ℵ‘𝐴)) |
67 | 62, 65, 66 | syl2an 493 |
. . . . . . . . 9
⊢
(((cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))
≼ (ℵ‘𝐴)
∧ 𝐴 ∈ On) →
((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴))))) ≼ (ℵ‘𝐴)) |
68 | | nsuceq0 5722 |
. . . . . . . . . . 11
⊢ suc
1𝑜 ≠ ∅ |
69 | | dom0 7973 |
. . . . . . . . . . 11
⊢ (suc
1𝑜 ≼ ∅ ↔ suc 1𝑜 =
∅) |
70 | 68, 69 | nemtbir 2877 |
. . . . . . . . . 10
⊢ ¬
suc 1𝑜 ≼ ∅ |
71 | | df-2o 7448 |
. . . . . . . . . . . . . 14
⊢
2𝑜 = suc 1𝑜 |
72 | 71 | breq1i 4590 |
. . . . . . . . . . . . 13
⊢
(2𝑜 ≼ 𝐵 ↔ suc 1𝑜 ≼
𝐵) |
73 | | breq2 4587 |
. . . . . . . . . . . . 13
⊢ (𝐵 = ∅ → (suc
1𝑜 ≼ 𝐵 ↔ suc 1𝑜 ≼
∅)) |
74 | 72, 73 | syl5bb 271 |
. . . . . . . . . . . 12
⊢ (𝐵 = ∅ →
(2𝑜 ≼ 𝐵 ↔ suc 1𝑜 ≼
∅)) |
75 | 74 | biimpcd 238 |
. . . . . . . . . . 11
⊢
(2𝑜 ≼ 𝐵 → (𝐵 = ∅ → suc 1𝑜
≼ ∅)) |
76 | 75 | adantld 482 |
. . . . . . . . . 10
⊢
(2𝑜 ≼ 𝐵 → ((((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))) =
∅ ∧ 𝐵 = ∅)
→ suc 1𝑜 ≼ ∅)) |
77 | 70, 76 | mtoi 189 |
. . . . . . . . 9
⊢
(2𝑜 ≼ 𝐵 → ¬ (((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴))))) = ∅ ∧ 𝐵 = ∅)) |
78 | | mapdom2 8016 |
. . . . . . . . 9
⊢
((((ℵ‘𝐴)
× (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))))
≼ (ℵ‘𝐴)
∧ ¬ (((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))) =
∅ ∧ 𝐵 = ∅))
→ (𝐵
↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))))
≼ (𝐵
↑𝑚 (ℵ‘𝐴))) |
79 | 67, 77, 78 | syl2an 493 |
. . . . . . . 8
⊢
((((cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))
≼ (ℵ‘𝐴)
∧ 𝐴 ∈ On) ∧
2𝑜 ≼ 𝐵) → (𝐵 ↑𝑚
((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴)))))) ≼ (𝐵 ↑𝑚
(ℵ‘𝐴))) |
80 | | domnsym 7971 |
. . . . . . . 8
⊢ ((𝐵 ↑𝑚
((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴)))))) ≼ (𝐵 ↑𝑚
(ℵ‘𝐴)) →
¬ (𝐵
↑𝑚 (ℵ‘𝐴)) ≺ (𝐵 ↑𝑚
((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴))))))) |
81 | 79, 80 | syl 17 |
. . . . . . 7
⊢
((((cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))
≼ (ℵ‘𝐴)
∧ 𝐴 ∈ On) ∧
2𝑜 ≼ 𝐵) → ¬ (𝐵 ↑𝑚
(ℵ‘𝐴)) ≺
(𝐵
↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))))) |
82 | 81 | expl 646 |
. . . . . 6
⊢
((cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))
≼ (ℵ‘𝐴)
→ ((𝐴 ∈ On ∧
2𝑜 ≼ 𝐵) → ¬ (𝐵 ↑𝑚
(ℵ‘𝐴)) ≺
(𝐵
↑𝑚 ((ℵ‘𝐴) × (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))))))) |
83 | 82 | com12 32 |
. . . . 5
⊢ ((𝐴 ∈ On ∧
2𝑜 ≼ 𝐵) → ((cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))
≼ (ℵ‘𝐴)
→ ¬ (𝐵
↑𝑚 (ℵ‘𝐴)) ≺ (𝐵 ↑𝑚
((ℵ‘𝐴) ×
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴)))))))) |
84 | 61, 83 | mt2d 130 |
. . . 4
⊢ ((𝐴 ∈ On ∧
2𝑜 ≼ 𝐵) → ¬ (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))
≼ (ℵ‘𝐴)) |
85 | | domtri 9257 |
. . . . . 6
⊢
(((cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))) ∈
V ∧ (ℵ‘𝐴)
∈ V) → ((cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))
≼ (ℵ‘𝐴)
↔ ¬ (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))))) |
86 | 52, 4, 85 | mp2an 704 |
. . . . 5
⊢
((cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))
≼ (ℵ‘𝐴)
↔ ¬ (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))) |
87 | 86 | biimpri 217 |
. . . 4
⊢ (¬
(ℵ‘𝐴) ≺
(cf‘(card‘(𝐵
↑𝑚 (ℵ‘𝐴)))) → (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))
≼ (ℵ‘𝐴)) |
88 | 84, 87 | nsyl2 141 |
. . 3
⊢ ((𝐴 ∈ On ∧
2𝑜 ≼ 𝐵) → (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))) |
89 | 88 | ex 449 |
. 2
⊢ (𝐴 ∈ On →
(2𝑜 ≼ 𝐵 → (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))))) |
90 | | fndm 5904 |
. . . . . 6
⊢ (ℵ
Fn On → dom ℵ = On) |
91 | 36, 90 | ax-mp 5 |
. . . . 5
⊢ dom
ℵ = On |
92 | 91 | eleq2i 2680 |
. . . 4
⊢ (𝐴 ∈ dom ℵ ↔ 𝐴 ∈ On) |
93 | | ndmfv 6128 |
. . . 4
⊢ (¬
𝐴 ∈ dom ℵ →
(ℵ‘𝐴) =
∅) |
94 | 92, 93 | sylnbir 320 |
. . 3
⊢ (¬
𝐴 ∈ On →
(ℵ‘𝐴) =
∅) |
95 | | 1n0 7462 |
. . . . . 6
⊢
1𝑜 ≠ ∅ |
96 | | 1onn 7606 |
. . . . . . . 8
⊢
1𝑜 ∈ ω |
97 | 96 | elexi 3186 |
. . . . . . 7
⊢
1𝑜 ∈ V |
98 | 97 | 0sdom 7976 |
. . . . . 6
⊢ (∅
≺ 1𝑜 ↔ 1𝑜 ≠
∅) |
99 | 95, 98 | mpbir 220 |
. . . . 5
⊢ ∅
≺ 1𝑜 |
100 | | id 22 |
. . . . . 6
⊢
((ℵ‘𝐴) =
∅ → (ℵ‘𝐴) = ∅) |
101 | | oveq2 6557 |
. . . . . . . . . . 11
⊢
((ℵ‘𝐴) =
∅ → (𝐵
↑𝑚 (ℵ‘𝐴)) = (𝐵 ↑𝑚
∅)) |
102 | | map0e 7781 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ V → (𝐵 ↑𝑚
∅) = 1𝑜) |
103 | 56, 102 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝐵 ↑𝑚
∅) = 1𝑜 |
104 | 101, 103 | syl6eq 2660 |
. . . . . . . . . 10
⊢
((ℵ‘𝐴) =
∅ → (𝐵
↑𝑚 (ℵ‘𝐴)) = 1𝑜) |
105 | 104 | fveq2d 6107 |
. . . . . . . . 9
⊢
((ℵ‘𝐴) =
∅ → (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) =
(card‘1𝑜)) |
106 | | cardnn 8672 |
. . . . . . . . . 10
⊢
(1𝑜 ∈ ω →
(card‘1𝑜) = 1𝑜) |
107 | 96, 106 | ax-mp 5 |
. . . . . . . . 9
⊢
(card‘1𝑜) =
1𝑜 |
108 | 105, 107 | syl6eq 2660 |
. . . . . . . 8
⊢
((ℵ‘𝐴) =
∅ → (card‘(𝐵 ↑𝑚
(ℵ‘𝐴))) =
1𝑜) |
109 | 108 | fveq2d 6107 |
. . . . . . 7
⊢
((ℵ‘𝐴) =
∅ → (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))) =
(cf‘1𝑜)) |
110 | | df-1o 7447 |
. . . . . . . . 9
⊢
1𝑜 = suc ∅ |
111 | 110 | fveq2i 6106 |
. . . . . . . 8
⊢
(cf‘1𝑜) = (cf‘suc
∅) |
112 | | 0elon 5695 |
. . . . . . . . 9
⊢ ∅
∈ On |
113 | | cfsuc 8962 |
. . . . . . . . 9
⊢ (∅
∈ On → (cf‘suc ∅) =
1𝑜) |
114 | 112, 113 | ax-mp 5 |
. . . . . . . 8
⊢
(cf‘suc ∅) = 1𝑜 |
115 | 111, 114 | eqtri 2632 |
. . . . . . 7
⊢
(cf‘1𝑜) =
1𝑜 |
116 | 109, 115 | syl6eq 2660 |
. . . . . 6
⊢
((ℵ‘𝐴) =
∅ → (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))) =
1𝑜) |
117 | 100, 116 | breq12d 4596 |
. . . . 5
⊢
((ℵ‘𝐴) =
∅ → ((ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))) ↔
∅ ≺ 1𝑜)) |
118 | 99, 117 | mpbiri 247 |
. . . 4
⊢
((ℵ‘𝐴) =
∅ → (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))) |
119 | 118 | a1d 25 |
. . 3
⊢
((ℵ‘𝐴) =
∅ → (2𝑜 ≼ 𝐵 → (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))))) |
120 | 94, 119 | syl 17 |
. 2
⊢ (¬
𝐴 ∈ On →
(2𝑜 ≼ 𝐵 → (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴)))))) |
121 | 89, 120 | pm2.61i 175 |
1
⊢
(2𝑜 ≼ 𝐵 → (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑𝑚
(ℵ‘𝐴))))) |