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 Fn On
36 fvelrnb Fn On 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 syl6ib 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 x cf 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 x cf x = card B A cf card B A
44 41 43 breq12d x = card B A x x cf x card B A card B A cf card B A
45 40 44 mpbii x = card B A card B A card B A cf card B A
46 45 rexlimivw x On x = card B A card B A card B A cf card B A
47 38 46 syl6 A On 2 𝑜 B card B A card B A cf card B A
48 47 imp A On 2 𝑜 B card B A card B A cf card B A
49 ensdomtr B A card B A card B A card B A cf card B A B A card B A cf card B A
50 4 48 49 sylancr A On 2 𝑜 B B A card B A cf 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 A cf card B A B A cf card B A
54 3 52 53 mp2an card B A cf card B A B A cf card B A
55 mapxpen B V A On cf card B A V B A cf card B A B A × cf card B A
56 1 18 51 55 mp3an B A cf card B A B A × cf card B A
57 54 56 entri card B A cf card B A B A × cf card B A
58 sdomentr B A card B A cf card B A card B A cf 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 syl5bb 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 Fn On 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 syl6eq 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 syl6eq 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 syl6eq 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