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 𝒫 ( ℵ ‘ 𝐴 ) ≈ ( 2om ( ℵ ‘ 𝐴 ) )
8 sdomentr ( ( ( ℵ ‘ 𝐴 ) ≺ 𝒫 ( ℵ ‘ 𝐴 ) ∧ 𝒫 ( ℵ ‘ 𝐴 ) ≈ ( 2om ( ℵ ‘ 𝐴 ) ) ) → ( ℵ ‘ 𝐴 ) ≺ ( 2om ( ℵ ‘ 𝐴 ) ) )
9 6 7 8 mp2an ( ℵ ‘ 𝐴 ) ≺ ( 2om ( ℵ ‘ 𝐴 ) )
10 mapdom1 ( 2o𝐵 → ( 2om ( ℵ ‘ 𝐴 ) ) ≼ ( 𝐵m ( ℵ ‘ 𝐴 ) ) )
11 sdomdomtr ( ( ( ℵ ‘ 𝐴 ) ≺ ( 2om ( ℵ ‘ 𝐴 ) ) ∧ ( 2om ( ℵ ‘ 𝐴 ) ) ≼ ( 𝐵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 ( ℵ ‘ 𝐴 ) ) ) ) )