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 ⊢B∈V
Assertion cfpwsdom ⊢2𝑜≼B→ℵ⁡A≺cf⁡card⁡Bℵ⁡A

Proof

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