Metamath Proof Explorer

Theorem cfpwsdom

Description: A corollary of Konig's Theorem konigth . Theorem 11.29 of TakeutiZaring p. 108. (Contributed by Mario Carneiro, 20-Mar-2013)

Ref Expression
Hypothesis cfpwsdom.1 ⊢ 𝐵 ∈ V
Assertion cfpwsdom ( 2o ≼ 𝐵 → ( ℵ ‘ 𝐴 ) ≺ ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cfpwsdom.1 ⊢ 𝐵 ∈ V
2 ovex ⊢ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ∈ V
3 2 cardid ⊢ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ≈ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) )
4 3 ensymi ⊢ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ≈ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) )
5 fvex ⊢ ( ℵ ‘ 𝐴 ) ∈ V
6 5 canth2 ⊢ ( ℵ ‘ 𝐴 ) ≺ 𝒫 ( ℵ ‘ 𝐴 )
7 5 pw2en ⊢ 𝒫 ( ℵ ‘ 𝐴 ) ≈ ( 2o ↑m ( ℵ ‘ 𝐴 ) )
8 sdomentr ⊢ ( ( ( ℵ ‘ 𝐴 ) ≺ 𝒫 ( ℵ ‘ 𝐴 ) ∧ 𝒫 ( ℵ ‘ 𝐴 ) ≈ ( 2o ↑m ( ℵ ‘ 𝐴 ) ) ) → ( ℵ ‘ 𝐴 ) ≺ ( 2o ↑m ( ℵ ‘ 𝐴 ) ) )
9 6 7 8 mp2an ⊢ ( ℵ ‘ 𝐴 ) ≺ ( 2o ↑m ( ℵ ‘ 𝐴 ) )
10 mapdom1 ⊢ ( 2o ≼ 𝐵 → ( 2o ↑m ( ℵ ‘ 𝐴 ) ) ≼ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) )
11 sdomdomtr ⊢ ( ( ( ℵ ‘ 𝐴 ) ≺ ( 2o ↑m ( ℵ ‘ 𝐴 ) ) ∧ ( 2o ↑m ( ℵ ‘ 𝐴 ) ) ≼ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) → ( ℵ ‘ 𝐴 ) ≺ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) )
12 9 10 11 sylancr ⊢ ( 2o ≼ 𝐵 → ( ℵ ‘ 𝐴 ) ≺ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) )
13 ficard ⊢ ( ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ∈ V → ( ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ∈ Fin ↔ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ∈ ω ) )
14 2 13 ax-mp ⊢ ( ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ∈ Fin ↔ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ∈ ω )
15 fict ⊢ ( ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ∈ Fin → ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ≼ ω )
16 14 15 sylbir ⊢ ( ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ∈ ω → ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ≼ ω )
17 alephgeom ⊢ ( 𝐴 ∈ On ↔ ω ⊆ ( ℵ ‘ 𝐴 ) )
18 alephon ⊢ ( ℵ ‘ 𝐴 ) ∈ On
19 ssdomg ⊢ ( ( ℵ ‘ 𝐴 ) ∈ On → ( ω ⊆ ( ℵ ‘ 𝐴 ) → ω ≼ ( ℵ ‘ 𝐴 ) ) )
20 18 19 ax-mp ⊢ ( ω ⊆ ( ℵ ‘ 𝐴 ) → ω ≼ ( ℵ ‘ 𝐴 ) )
21 17 20 sylbi ⊢ ( 𝐴 ∈ On → ω ≼ ( ℵ ‘ 𝐴 ) )
22 domtr ⊢ ( ( ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ≼ ω ∧ ω ≼ ( ℵ ‘ 𝐴 ) ) → ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ≼ ( ℵ ‘ 𝐴 ) )
23 16 21 22 syl2an ⊢ ( ( ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ∈ ω ∧ 𝐴 ∈ On ) → ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ≼ ( ℵ ‘ 𝐴 ) )
24 domnsym ⊢ ( ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ≼ ( ℵ ‘ 𝐴 ) → ¬ ( ℵ ‘ 𝐴 ) ≺ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) )
25 23 24 syl ⊢ ( ( ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ∈ ω ∧ 𝐴 ∈ On ) → ¬ ( ℵ ‘ 𝐴 ) ≺ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) )
26 25 expcom ⊢ ( 𝐴 ∈ On → ( ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ∈ ω → ¬ ( ℵ ‘ 𝐴 ) ≺ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) )
27 26 con2d ⊢ ( 𝐴 ∈ On → ( ( ℵ ‘ 𝐴 ) ≺ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) → ¬ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ∈ ω ) )
28 cardidm ⊢ ( card ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) = ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) )
29 iscard3 ⊢ ( ( card ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) = ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ↔ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ∈ ( ω ∪ ran ℵ ) )
30 elun ⊢ ( ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ∈ ( ω ∪ ran ℵ ) ↔ ( ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ∈ ω ∨ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ∈ ran ℵ ) )
31 df-or ⊢ ( ( ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ∈ ω ∨ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ∈ ran ℵ ) ↔ ( ¬ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ∈ ω → ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ∈ ran ℵ ) )
32 29 30 31 3bitri ⊢ ( ( card ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) = ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ↔ ( ¬ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ∈ ω → ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ∈ ran ℵ ) )
33 28 32 mpbi ⊢ ( ¬ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ∈ ω → ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ∈ ran ℵ )
34 12 27 33 syl56 ⊢ ( 𝐴 ∈ On → ( 2o ≼ 𝐵 → ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ∈ ran ℵ ) )
35 alephfnon ⊢ ℵ Fn On
36 fvelrnb ⊢ ( ℵ Fn On → ( ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ∈ ran ℵ ↔ ∃ 𝑥 ∈ On ( ℵ ‘ 𝑥 ) = ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) )
37 35 36 ax-mp ⊢ ( ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ∈ ran ℵ ↔ ∃ 𝑥 ∈ On ( ℵ ‘ 𝑥 ) = ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) )
38 34 37 syl6ib ⊢ ( 𝐴 ∈ On → ( 2o ≼ 𝐵 → ∃ 𝑥 ∈ On ( ℵ ‘ 𝑥 ) = ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) )
39 eqid ⊢ ( 𝑦 ∈ ( cf ‘ ( ℵ ‘ 𝑥 ) ) ↦ ( har ‘ ( 𝑧 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ( cf ‘ ( ℵ ‘ 𝑥 ) ) ↦ ( har ‘ ( 𝑧 ‘ 𝑦 ) ) )
40 39 pwcfsdom ⊢ ( ℵ ‘ 𝑥 ) ≺ ( ( ℵ ‘ 𝑥 ) ↑m ( cf ‘ ( ℵ ‘ 𝑥 ) ) )
41 id ⊢ ( ( ℵ ‘ 𝑥 ) = ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) → ( ℵ ‘ 𝑥 ) = ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) )
42 fveq2 ⊢ ( ( ℵ ‘ 𝑥 ) = ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) → ( cf ‘ ( ℵ ‘ 𝑥 ) ) = ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) )
43 41 42 oveq12d ⊢ ( ( ℵ ‘ 𝑥 ) = ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) → ( ( ℵ ‘ 𝑥 ) ↑m ( cf ‘ ( ℵ ‘ 𝑥 ) ) ) = ( ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ↑m ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) )
44 41 43 breq12d ⊢ ( ( ℵ ‘ 𝑥 ) = ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) → ( ( ℵ ‘ 𝑥 ) ≺ ( ( ℵ ‘ 𝑥 ) ↑m ( cf ‘ ( ℵ ‘ 𝑥 ) ) ) ↔ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ≺ ( ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ↑m ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) ) )
45 40 44 mpbii ⊢ ( ( ℵ ‘ 𝑥 ) = ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) → ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ≺ ( ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ↑m ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) )
46 45 rexlimivw ⊢ ( ∃ 𝑥 ∈ On ( ℵ ‘ 𝑥 ) = ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) → ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ≺ ( ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ↑m ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) )
47 38 46 syl6 ⊢ ( 𝐴 ∈ On → ( 2o ≼ 𝐵 → ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ≺ ( ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ↑m ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) ) )
48 47 imp ⊢ ( ( 𝐴 ∈ On ∧ 2o ≼ 𝐵 ) → ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ≺ ( ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ↑m ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) )
49 ensdomtr ⊢ ( ( ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ≈ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ∧ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ≺ ( ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ↑m ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) ) → ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ≺ ( ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ↑m ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) )
50 4 48 49 sylancr ⊢ ( ( 𝐴 ∈ On ∧ 2o ≼ 𝐵 ) → ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ≺ ( ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ↑m ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) )
51 fvex ⊢ ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ∈ V
52 51 enref ⊢ ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ≈ ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) )
53 mapen ⊢ ( ( ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ≈ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ∧ ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ≈ ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) → ( ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ↑m ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) ≈ ( ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ↑m ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) )
54 3 52 53 mp2an ⊢ ( ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ↑m ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) ≈ ( ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ↑m ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) )
55 mapxpen ⊢ ( ( 𝐵 ∈ V ∧ ( ℵ ‘ 𝐴 ) ∈ On ∧ ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ∈ V ) → ( ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ↑m ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) ≈ ( 𝐵 ↑m ( ( ℵ ‘ 𝐴 ) × ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) ) )
56 1 18 51 55 mp3an ⊢ ( ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ↑m ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) ≈ ( 𝐵 ↑m ( ( ℵ ‘ 𝐴 ) × ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) )
57 54 56 entri ⊢ ( ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ↑m ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) ≈ ( 𝐵 ↑m ( ( ℵ ‘ 𝐴 ) × ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) )
58 sdomentr ⊢ ( ( ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ≺ ( ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ↑m ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) ∧ ( ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ↑m ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) ≈ ( 𝐵 ↑m ( ( ℵ ‘ 𝐴 ) × ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) ) ) → ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ≺ ( 𝐵 ↑m ( ( ℵ ‘ 𝐴 ) × ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) ) )
59 50 57 58 sylancl ⊢ ( ( 𝐴 ∈ On ∧ 2o ≼ 𝐵 ) → ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ≺ ( 𝐵 ↑m ( ( ℵ ‘ 𝐴 ) × ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) ) )
60 5 xpdom2 ⊢ ( ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ≼ ( ℵ ‘ 𝐴 ) → ( ( ℵ ‘ 𝐴 ) × ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) ≼ ( ( ℵ ‘ 𝐴 ) × ( ℵ ‘ 𝐴 ) ) )
61 17 biimpi ⊢ ( 𝐴 ∈ On → ω ⊆ ( ℵ ‘ 𝐴 ) )
62 infxpen ⊢ ( ( ( ℵ ‘ 𝐴 ) ∈ On ∧ ω ⊆ ( ℵ ‘ 𝐴 ) ) → ( ( ℵ ‘ 𝐴 ) × ( ℵ ‘ 𝐴 ) ) ≈ ( ℵ ‘ 𝐴 ) )
63 18 61 62 sylancr ⊢ ( 𝐴 ∈ On → ( ( ℵ ‘ 𝐴 ) × ( ℵ ‘ 𝐴 ) ) ≈ ( ℵ ‘ 𝐴 ) )
64 domentr ⊢ ( ( ( ( ℵ ‘ 𝐴 ) × ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) ≼ ( ( ℵ ‘ 𝐴 ) × ( ℵ ‘ 𝐴 ) ) ∧ ( ( ℵ ‘ 𝐴 ) × ( ℵ ‘ 𝐴 ) ) ≈ ( ℵ ‘ 𝐴 ) ) → ( ( ℵ ‘ 𝐴 ) × ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) ≼ ( ℵ ‘ 𝐴 ) )
65 60 63 64 syl2an ⊢ ( ( ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ≼ ( ℵ ‘ 𝐴 ) ∧ 𝐴 ∈ On ) → ( ( ℵ ‘ 𝐴 ) × ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) ≼ ( ℵ ‘ 𝐴 ) )
66 nsuceq0 ⊢ suc 1o ≠ ∅
67 dom0 ⊢ ( suc 1o ≼ ∅ ↔ suc 1o = ∅ )
68 66 67 nemtbir ⊢ ¬ suc 1o ≼ ∅
69 df-2o ⊢ 2o = suc 1o
70 69 breq1i ⊢ ( 2o ≼ 𝐵 ↔ suc 1o ≼ 𝐵 )
71 breq2 ⊢ ( 𝐵 = ∅ → ( suc 1o ≼ 𝐵 ↔ suc 1o ≼ ∅ ) )
72 70 71 syl5bb ⊢ ( 𝐵 = ∅ → ( 2o ≼ 𝐵 ↔ suc 1o ≼ ∅ ) )
73 72 biimpcd ⊢ ( 2o ≼ 𝐵 → ( 𝐵 = ∅ → suc 1o ≼ ∅ ) )
74 73 adantld ⊢ ( 2o ≼ 𝐵 → ( ( ( ( ℵ ‘ 𝐴 ) × ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) = ∅ ∧ 𝐵 = ∅ ) → suc 1o ≼ ∅ ) )
75 68 74 mtoi ⊢ ( 2o ≼ 𝐵 → ¬ ( ( ( ℵ ‘ 𝐴 ) × ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) = ∅ ∧ 𝐵 = ∅ ) )
76 mapdom2 ⊢ ( ( ( ( ℵ ‘ 𝐴 ) × ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) ≼ ( ℵ ‘ 𝐴 ) ∧ ¬ ( ( ( ℵ ‘ 𝐴 ) × ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) = ∅ ∧ 𝐵 = ∅ ) ) → ( 𝐵 ↑m ( ( ℵ ‘ 𝐴 ) × ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) ) ≼ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) )
77 65 75 76 syl2an ⊢ ( ( ( ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ≼ ( ℵ ‘ 𝐴 ) ∧ 𝐴 ∈ On ) ∧ 2o ≼ 𝐵 ) → ( 𝐵 ↑m ( ( ℵ ‘ 𝐴 ) × ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) ) ≼ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) )
78 domnsym ⊢ ( ( 𝐵 ↑m ( ( ℵ ‘ 𝐴 ) × ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) ) ≼ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) → ¬ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ≺ ( 𝐵 ↑m ( ( ℵ ‘ 𝐴 ) × ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) ) )
79 77 78 syl ⊢ ( ( ( ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ≼ ( ℵ ‘ 𝐴 ) ∧ 𝐴 ∈ On ) ∧ 2o ≼ 𝐵 ) → ¬ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ≺ ( 𝐵 ↑m ( ( ℵ ‘ 𝐴 ) × ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) ) )
80 79 expl ⊢ ( ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ≼ ( ℵ ‘ 𝐴 ) → ( ( 𝐴 ∈ On ∧ 2o ≼ 𝐵 ) → ¬ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ≺ ( 𝐵 ↑m ( ( ℵ ‘ 𝐴 ) × ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) ) ) )
81 80 com12 ⊢ ( ( 𝐴 ∈ On ∧ 2o ≼ 𝐵 ) → ( ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ≼ ( ℵ ‘ 𝐴 ) → ¬ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ≺ ( 𝐵 ↑m ( ( ℵ ‘ 𝐴 ) × ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) ) ) )
82 59 81 mt2d ⊢ ( ( 𝐴 ∈ On ∧ 2o ≼ 𝐵 ) → ¬ ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ≼ ( ℵ ‘ 𝐴 ) )
83 domtri ⊢ ( ( ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ∈ V ∧ ( ℵ ‘ 𝐴 ) ∈ V ) → ( ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ≼ ( ℵ ‘ 𝐴 ) ↔ ¬ ( ℵ ‘ 𝐴 ) ≺ ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) )
84 51 5 83 mp2an ⊢ ( ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ≼ ( ℵ ‘ 𝐴 ) ↔ ¬ ( ℵ ‘ 𝐴 ) ≺ ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) )
85 84 biimpri ⊢ ( ¬ ( ℵ ‘ 𝐴 ) ≺ ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) → ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ≼ ( ℵ ‘ 𝐴 ) )
86 82 85 nsyl2 ⊢ ( ( 𝐴 ∈ On ∧ 2o ≼ 𝐵 ) → ( ℵ ‘ 𝐴 ) ≺ ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) )
87 86 ex ⊢ ( 𝐴 ∈ On → ( 2o ≼ 𝐵 → ( ℵ ‘ 𝐴 ) ≺ ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) )
88 fndm ⊢ ( ℵ Fn On → dom ℵ = On )
89 35 88 ax-mp ⊢ dom ℵ = On
90 89 eleq2i ⊢ ( 𝐴 ∈ dom ℵ ↔ 𝐴 ∈ On )
91 ndmfv ⊢ ( ¬ 𝐴 ∈ dom ℵ → ( ℵ ‘ 𝐴 ) = ∅ )
92 90 91 sylnbir ⊢ ( ¬ 𝐴 ∈ On → ( ℵ ‘ 𝐴 ) = ∅ )
93 1n0 ⊢ 1o ≠ ∅
94 1oex ⊢ 1o ∈ V
95 94 0sdom ⊢ ( ∅ ≺ 1o ↔ 1o ≠ ∅ )
96 93 95 mpbir ⊢ ∅ ≺ 1o
97 id ⊢ ( ( ℵ ‘ 𝐴 ) = ∅ → ( ℵ ‘ 𝐴 ) = ∅ )
98 oveq2 ⊢ ( ( ℵ ‘ 𝐴 ) = ∅ → ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) = ( 𝐵 ↑m ∅ ) )
99 map0e ⊢ ( 𝐵 ∈ V → ( 𝐵 ↑m ∅ ) = 1o )
100 1 99 ax-mp ⊢ ( 𝐵 ↑m ∅ ) = 1o
101 98 100 eqtrdi ⊢ ( ( ℵ ‘ 𝐴 ) = ∅ → ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) = 1o )
102 101 fveq2d ⊢ ( ( ℵ ‘ 𝐴 ) = ∅ → ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) = ( card ‘ 1o ) )
103 1onn ⊢ 1o ∈ ω
104 cardnn ⊢ ( 1o ∈ ω → ( card ‘ 1o ) = 1o )
105 103 104 ax-mp ⊢ ( card ‘ 1o ) = 1o
106 102 105 eqtrdi ⊢ ( ( ℵ ‘ 𝐴 ) = ∅ → ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) = 1o )
107 106 fveq2d ⊢ ( ( ℵ ‘ 𝐴 ) = ∅ → ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) = ( cf ‘ 1o ) )
108 df-1o ⊢ 1o = suc ∅
109 108 fveq2i ⊢ ( cf ‘ 1o ) = ( cf ‘ suc ∅ )
110 0elon ⊢ ∅ ∈ On
111 cfsuc ⊢ ( ∅ ∈ On → ( cf ‘ suc ∅ ) = 1o )
112 110 111 ax-mp ⊢ ( cf ‘ suc ∅ ) = 1o
113 109 112 eqtri ⊢ ( cf ‘ 1o ) = 1o
114 107 113 eqtrdi ⊢ ( ( ℵ ‘ 𝐴 ) = ∅ → ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) = 1o )
115 97 114 breq12d ⊢ ( ( ℵ ‘ 𝐴 ) = ∅ → ( ( ℵ ‘ 𝐴 ) ≺ ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ↔ ∅ ≺ 1o ) )
116 96 115 mpbiri ⊢ ( ( ℵ ‘ 𝐴 ) = ∅ → ( ℵ ‘ 𝐴 ) ≺ ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) )
117 116 a1d ⊢ ( ( ℵ ‘ 𝐴 ) = ∅ → ( 2o ≼ 𝐵 → ( ℵ ‘ 𝐴 ) ≺ ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) )
118 92 117 syl ⊢ ( ¬ 𝐴 ∈ On → ( 2o ≼ 𝐵 → ( ℵ ‘ 𝐴 ) ≺ ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) ) )
119 87 118 pm2.61i ⊢ ( 2o ≼ 𝐵 → ( ℵ ‘ 𝐴 ) ≺ ( cf ‘ ( card ‘ ( 𝐵 ↑m ( ℵ ‘ 𝐴 ) ) ) ) )