Metamath Proof Explorer


Theorem pwcfsdom

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

Ref Expression
Hypothesis pwcfsdom.1 H = y cf A har f y
Assertion pwcfsdom A A cf A

Proof

Step Hyp Ref Expression
1 pwcfsdom.1 H = y cf A har f y
2 onzsl A On A = x On A = suc x A V Lim A
3 2 biimpi A On A = x On A = suc x A V Lim A
4 cfom cf ω = ω
5 aleph0 = ω
6 5 fveq2i cf = cf ω
7 4 6 5 3eqtr4i cf =
8 2fveq3 A = cf A = cf
9 fveq2 A = A =
10 7 8 9 3eqtr4a A = cf A = A
11 fvex A V
12 11 canth2 A 𝒫 A
13 11 pw2en 𝒫 A 2 𝑜 A
14 sdomentr A 𝒫 A 𝒫 A 2 𝑜 A A 2 𝑜 A
15 12 13 14 mp2an A 2 𝑜 A
16 alephon A On
17 alephgeom A On ω A
18 omelon ω On
19 2onn 2 𝑜 ω
20 onelss ω On 2 𝑜 ω 2 𝑜 ω
21 18 19 20 mp2 2 𝑜 ω
22 sstr 2 𝑜 ω ω A 2 𝑜 A
23 21 22 mpan ω A 2 𝑜 A
24 17 23 sylbi A On 2 𝑜 A
25 ssdomg A On 2 𝑜 A 2 𝑜 A
26 16 24 25 mpsyl A On 2 𝑜 A
27 mapdom1 2 𝑜 A 2 𝑜 A A A
28 26 27 syl A On 2 𝑜 A A A
29 sdomdomtr A 2 𝑜 A 2 𝑜 A A A A A A
30 15 28 29 sylancr A On A A A
31 oveq2 cf A = A A cf A = A A
32 31 breq2d cf A = A A A cf A A A A
33 30 32 syl5ibrcom A On cf A = A A A cf A
34 10 33 syl5 A On A = A A cf A
35 alephreg cf suc x = suc x
36 2fveq3 A = suc x cf A = cf suc x
37 fveq2 A = suc x A = suc x
38 35 36 37 3eqtr4a A = suc x cf A = A
39 38 rexlimivw x On A = suc x cf A = A
40 39 33 syl5 A On x On A = suc x A A cf A
41 cfsmo A On f f : cf A A Smo f z A w cf A z f w
42 limelon A V Lim A A On
43 ffn f : cf A A f Fn cf A
44 fnrnfv f Fn cf A ran f = y | x cf A y = f x
45 44 unieqd f Fn cf A ran f = y | x cf A y = f x
46 43 45 syl f : cf A A ran f = y | x cf A y = f x
47 fvex f x V
48 47 dfiun2 x cf A f x = y | x cf A y = f x
49 46 48 eqtr4di f : cf A A ran f = x cf A f x
50 49 ad2antrl A On f : cf A A z A w cf A z f w ran f = x cf A f x
51 fnfvelrn f Fn cf A w cf A f w ran f
52 43 51 sylan f : cf A A w cf A f w ran f
53 sseq2 y = f w z y z f w
54 53 rspcev f w ran f z f w y ran f z y
55 52 54 sylan f : cf A A w cf A z f w y ran f z y
56 55 rexlimdva2 f : cf A A w cf A z f w y ran f z y
57 56 ralimdv f : cf A A z A w cf A z f w z A y ran f z y
58 57 imp f : cf A A z A w cf A z f w z A y ran f z y
59 58 adantl A On f : cf A A z A w cf A z f w z A y ran f z y
60 alephislim A On Lim A
61 60 biimpi A On Lim A
62 frn f : cf A A ran f A
63 62 adantr f : cf A A z A w cf A z f w ran f A
64 coflim Lim A ran f A ran f = A z A y ran f z y
65 61 63 64 syl2an A On f : cf A A z A w cf A z f w ran f = A z A y ran f z y
66 59 65 mpbird A On f : cf A A z A w cf A z f w ran f = A
67 50 66 eqtr3d A On f : cf A A z A w cf A z f w x cf A f x = A
68 ffvelrn f : cf A A x cf A f x A
69 16 oneli f x A f x On
70 harcard card har f x = har f x
71 iscard card har f x = har f x har f x On y har f x y har f x
72 71 simprbi card har f x = har f x y har f x y har f x
73 70 72 ax-mp y har f x y har f x
74 domrefg f x V f x f x
75 47 74 ax-mp f x f x
76 elharval f x har f x f x On f x f x
77 76 biimpri f x On f x f x f x har f x
78 75 77 mpan2 f x On f x har f x
79 breq1 y = f x y har f x f x har f x
80 79 rspccv y har f x y har f x f x har f x f x har f x
81 73 78 80 mpsyl f x On f x har f x
82 68 69 81 3syl f : cf A A x cf A f x har f x
83 harcl har f x On
84 2fveq3 y = x har f y = har f x
85 84 1 fvmptg x cf A har f x On H x = har f x
86 83 85 mpan2 x cf A H x = har f x
87 86 breq2d x cf A f x H x f x har f x
88 87 adantl f : cf A A x cf A f x H x f x har f x
89 82 88 mpbird f : cf A A x cf A f x H x
90 89 ralrimiva f : cf A A x cf A f x H x
91 fvex cf A V
92 eqid x cf A f x = x cf A f x
93 eqid x cf A H x = x cf A H x
94 91 92 93 konigth x cf A f x H x x cf A f x x cf A H x
95 90 94 syl f : cf A A x cf A f x x cf A H x
96 95 ad2antrl A On f : cf A A z A w cf A z f w x cf A f x x cf A H x
97 67 96 eqbrtrrd A On f : cf A A z A w cf A z f w A x cf A H x
98 42 97 sylan A V Lim A f : cf A A z A w cf A z f w A x cf A H x
99 ovex A cf A V
100 68 ex f : cf A A x cf A f x A
101 alephlim A V Lim A A = y A y
102 101 eleq2d A V Lim A f x A f x y A y
103 eliun f x y A y y A f x y
104 alephcard card y = y
105 104 eleq2i f x card y f x y
106 cardsdomelir f x card y f x y
107 105 106 sylbir f x y f x y
108 elharval y har f x y On y f x
109 108 simprbi y har f x y f x
110 domnsym y f x ¬ f x y
111 109 110 syl y har f x ¬ f x y
112 111 con2i f x y ¬ y har f x
113 alephon y On
114 ontri1 har f x On y On har f x y ¬ y har f x
115 83 113 114 mp2an har f x y ¬ y har f x
116 112 115 sylibr f x y har f x y
117 107 116 syl f x y har f x y
118 alephord2i A On y A y A
119 118 imp A On y A y A
120 ontr2 har f x On A On har f x y y A har f x A
121 83 16 120 mp2an har f x y y A har f x A
122 117 119 121 syl2anr A On y A f x y har f x A
123 122 rexlimdva2 A On y A f x y har f x A
124 103 123 syl5bi A On f x y A y har f x A
125 42 124 syl A V Lim A f x y A y har f x A
126 102 125 sylbid A V Lim A f x A har f x A
127 100 126 sylan9r A V Lim A f : cf A A x cf A har f x A
128 127 imp A V Lim A f : cf A A x cf A har f x A
129 84 cbvmptv y cf A har f y = x cf A har f x
130 1 129 eqtri H = x cf A har f x
131 128 130 fmptd A V Lim A f : cf A A H : cf A A
132 ffvelrn H : cf A A x cf A H x A
133 onelss A On H x A H x A
134 16 132 133 mpsyl H : cf A A x cf A H x A
135 134 ralrimiva H : cf A A x cf A H x A
136 ss2ixp x cf A H x A x cf A H x x cf A A
137 91 11 ixpconst x cf A A = A cf A
138 136 137 sseqtrdi x cf A H x A x cf A H x A cf A
139 131 135 138 3syl A V Lim A f : cf A A x cf A H x A cf A
140 ssdomg A cf A V x cf A H x A cf A x cf A H x A cf A
141 99 139 140 mpsyl A V Lim A f : cf A A x cf A H x A cf A
142 141 adantrr A V Lim A f : cf A A z A w cf A z f w x cf A H x A cf A
143 sdomdomtr A x cf A H x x cf A H x A cf A A A cf A
144 98 142 143 syl2anc A V Lim A f : cf A A z A w cf A z f w A A cf A
145 144 expcom f : cf A A z A w cf A z f w A V Lim A A A cf A
146 145 3adant2 f : cf A A Smo f z A w cf A z f w A V Lim A A A cf A
147 146 exlimiv f f : cf A A Smo f z A w cf A z f w A V Lim A A A cf A
148 16 41 147 mp2b A V Lim A A A cf A
149 148 a1i A On A V Lim A A A cf A
150 34 40 149 3jaod A On A = x On A = suc x A V Lim A A A cf A
151 3 150 mpd A On A A cf A
152 alephfnon Fn On
153 152 fndmi dom = On
154 153 eleq2i A dom A On
155 ndmfv ¬ A dom A =
156 1n0 1 𝑜
157 1oex 1 𝑜 V
158 157 0sdom 1 𝑜 1 𝑜
159 156 158 mpbir 1 𝑜
160 id A = A =
161 fveq2 A = cf A = cf
162 cf0 cf =
163 161 162 eqtrdi A = cf A =
164 160 163 oveq12d A = A cf A =
165 0ex V
166 map0e V = 1 𝑜
167 165 166 ax-mp = 1 𝑜
168 164 167 eqtrdi A = A cf A = 1 𝑜
169 160 168 breq12d A = A A cf A 1 𝑜
170 159 169 mpbiri A = A A cf A
171 155 170 syl ¬ A dom A A cf A
172 154 171 sylnbir ¬ A On A A cf A
173 151 172 pm2.61i A A cf A