MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  inar1 Unicode version

Theorem inar1 8821
Description: for a strongly inaccessible cardinal is equipotent to . (Contributed by Mario Carneiro, 6-Jun-2013.)
Assertion
Ref Expression
inar1

Proof of Theorem inar1
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 inawina 8736 . . . . . 6
2 winaon 8734 . . . . . 6
31, 2syl 16 . . . . 5
4 winalim 8741 . . . . . 6
51, 4syl 16 . . . . 5
6 r1lim 7865 . . . . 5
73, 5, 6syl2anc 644 . . . 4
8 onelon 4765 . . . . . . . . 9
93, 8sylan 459 . . . . . . . 8
10 eleq1 2549 . . . . . . . . . . 11
11 fveq2 5708 . . . . . . . . . . . 12
1211breq1d 4328 . . . . . . . . . . 11
1310, 12imbi12d 313 . . . . . . . . . 10
14 eleq1 2549 . . . . . . . . . . 11
15 fveq2 5708 . . . . . . . . . . . 12
1615breq1d 4328 . . . . . . . . . . 11
1714, 16imbi12d 313 . . . . . . . . . 10
18 eleq1 2549 . . . . . . . . . . 11
19 fveq2 5708 . . . . . . . . . . . 12
2019breq1d 4328 . . . . . . . . . . 11
2118, 20imbi12d 313 . . . . . . . . . 10
22 ne0i 3679 . . . . . . . . . . . . 13
23 0sdomg 7401 . . . . . . . . . . . . 13
2422, 23syl5ibr 214 . . . . . . . . . . . 12
25 r10 7861 . . . . . . . . . . . . 13
2625breq1i 4325 . . . . . . . . . . . 12
2724, 26syl6ibr 220 . . . . . . . . . . 11
281, 2, 273syl 19 . . . . . . . . . 10
29 eloni 4750 . . . . . . . . . . . . . . 15
30 ordtr 4754 . . . . . . . . . . . . . . 15
3129, 30syl 16 . . . . . . . . . . . . . 14
32 trsuc 4825 . . . . . . . . . . . . . . 15
3332ex 425 . . . . . . . . . . . . . 14
343, 31, 333syl 19 . . . . . . . . . . . . 13
3534adantl 454 . . . . . . . . . . . 12
36 r1suc 7863 . . . . . . . . . . . . . . 15
37 fvex 5718 . . . . . . . . . . . . . . . . . 18
3837cardid 8593 . . . . . . . . . . . . . . . . 17
3938ensymi 7321 . . . . . . . . . . . . . . . 16
40 pwen 7445 . . . . . . . . . . . . . . . 16
4139, 40ax-mp 5 . . . . . . . . . . . . . . 15
4236, 41syl6eqbr 4355 . . . . . . . . . . . . . 14
43 winacard 8738 . . . . . . . . . . . . . . . . . . 19
4443eleq2d 2556 . . . . . . . . . . . . . . . . . 18
45 cardsdom 8601 . . . . . . . . . . . . . . . . . . 19
4637, 2, 45sylancr 646 . . . . . . . . . . . . . . . . . 18
4744, 46bitr3d 248 . . . . . . . . . . . . . . . . 17
481, 47syl 16 . . . . . . . . . . . . . . . 16
49 elina 8733 . . . . . . . . . . . . . . . . . 18
5049simp3bi 979 . . . . . . . . . . . . . . . . 17
51 pweq 3896 . . . . . . . . . . . . . . . . . . 19
5251breq1d 4328 . . . . . . . . . . . . . . . . . 18
5352rspccv 3110 . . . . . . . . . . . . . . . . 17
5450, 53syl 16 . . . . . . . . . . . . . . . 16
5548, 54sylbird 228 . . . . . . . . . . . . . . 15
5655imp 420 . . . . . . . . . . . . . 14
57 ensdomtr 7408 . . . . . . . . . . . . . 14
5842, 56, 57syl2an 465 . . . . . . . . . . . . 13
5958expr 600 . . . . . . . . . . . 12
6035, 59imim12d 71 . . . . . . . . . . 11
6160ex 425 . . . . . . . . . 10
62 vex 3018 . . . . . . . . . . . . . . . 16
63 r1lim 7865 . . . . . . . . . . . . . . . 16
6462, 63mpan 653 . . . . . . . . . . . . . . 15
65 nfcv 2625 . . . . . . . . . . . . . . . . . . 19
66 nfcv 2625 . . . . . . . . . . . . . . . . . . . 20
67 nfcv 2625 . . . . . . . . . . . . . . . . . . . 20
68 nfiu1 4226 . . . . . . . . . . . . . . . . . . . 20
6966, 67, 68nfbr 4362 . . . . . . . . . . . . . . . . . . 19
70 fveq2 5708 . . . . . . . . . . . . . . . . . . . 20
7170breq1d 4328 . . . . . . . . . . . . . . . . . . 19
72 fvex 5718 . . . . . . . . . . . . . . . . . . . . . 22
7362, 72iunex 6563 . . . . . . . . . . . . . . . . . . . . 21
74 ssiun2 4239 . . . . . . . . . . . . . . . . . . . . 21
75 ssdomg 7317 . . . . . . . . . . . . . . . . . . . . 21
7673, 74, 75mpsyl 62 . . . . . . . . . . . . . . . . . . . 20
77 endomtr 7329 . . . . . . . . . . . . . . . . . . . 20
7839, 76, 77sylancr 646 . . . . . . . . . . . . . . . . . . 19
7965, 69, 71, 78vtoclgaf 3075 . . . . . . . . . . . . . . . . . 18
8079rgen 2825 . . . . . . . . . . . . . . . . 17
81 iundom 8588 . . . . . . . . . . . . . . . . 17
8262, 80, 81mp2an 655 . . . . . . . . . . . . . . . 16
8362, 73unex 6388 . . . . . . . . . . . . . . . . . . . 20
84 ssun2 3557 . . . . . . . . . . . . . . . . . . . 20
85 ssdomg 7317 . . . . . . . . . . . . . . . . . . . 20
8683, 84, 85mp2 9 . . . . . . . . . . . . . . . . . . 19
8762xpdom2 7368 . . . . . . . . . . . . . . . . . . 19
8886, 87ax-mp 5 . . . . . . . . . . . . . . . . . 18
89 ssun1 3556 . . . . . . . . . . . . . . . . . . . 20
90 ssdomg 7317 . . . . . . . . . . . . . . . . . . . 20
9183, 89, 90mp2 9 . . . . . . . . . . . . . . . . . . 19
9283xpdom1 7372 . . . . . . . . . . . . . . . . . . 19
9391, 92ax-mp 5 . . . . . . . . . . . . . . . . . 18
94 domtr 7324 . . . . . . . . . . . . . . . . . 18
9588, 93, 94mp2an 655 . . . . . . . . . . . . . . . . 17
96 limomss 6491 . . . . . . . . . . . . . . . . . . . 20
9796, 89syl6ss 3405 . . . . . . . . . . . . . . . . . . 19
98 ssdomg 7317 . . . . . . . . . . . . . . . . . . 19
9983, 97, 98mpsyl 62 . . . . . . . . . . . . . . . . . 18
100 infxpidm 8608 . . . . . . . . . . . . . . . . . 18
10199, 100syl 16 . . . . . . . . . . . . . . . . 17
102 domentr 7330 . . . . . . . . . . . . . . . . 17
10395, 101, 102sylancr 646 . . . . . . . . . . . . . . . 16
104 domtr 7324 . . . . . . . . . . . . . . . 16
10582, 103, 104sylancr 646 . . . . . . . . . . . . . . 15
10664, 105eqbrtrd 4338 . . . . . . . . . . . . . 14
107106ad2antlr 709 . . . . . . . . . . . . 13
108 eleq1a 2558 . . . . . . . . . . . . . . . . . . 19
109 ordirr 4758 . . . . . . . . . . . . . . . . . . . 20
1103, 29, 1093syl 19 . . . . . . . . . . . . . . . . . . 19
111108, 110nsyli 136 . . . . . . . . . . . . . . . . . 18
112111imp 420 . . . . . . . . . . . . . . . . 17
113112ad2ant2r 729 . . . . . . . . . . . . . . . 16
114 simpll 732 . . . . . . . . . . . . . . . . 17
115 limord 4799 . . . . . . . . . . . . . . . . . . . . . . . . 25
11662elon 4749 . . . . . . . . . . . . . . . . . . . . . . . . 25
117115, 116sylibr 205 . . . . . . . . . . . . . . . . . . . . . . . 24
118117ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . 23
119 cardf 8596 . . . . . . . . . . . . . . . . . . . . . . . . 25
120 r1fnon 7860 . . . . . . . . . . . . . . . . . . . . . . . . . 26
121 dffn2 5578 . . . . . . . . . . . . . . . . . . . . . . . . . 26
122120, 121mpbi 201 . . . . . . . . . . . . . . . . . . . . . . . . 25
123 fco 5586 . . . . . . . . . . . . . . . . . . . . . . . . 25
124119, 122, 123mp2an 655 . . . . . . . . . . . . . . . . . . . . . . . 24
125 onss 6412 . . . . . . . . . . . . . . . . . . . . . . . 24
126 fssres 5595 . . . . . . . . . . . . . . . . . . . . . . . 24
127124, 125, 126sylancr 646 . . . . . . . . . . . . . . . . . . . . . . 23
128 ffn 5577 . . . . . . . . . . . . . . . . . . . . . . 23
129118, 127, 1283syl 19 . . . . . . . . . . . . . . . . . . . . . 22
1303ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
131 simpr 449 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
132 simplll 736 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
133 ontr1 4786 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
134133imp 420 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
135130, 131, 132, 134syl12anc 1190 . . . . . . . . . . . . . . . . . . . . . . . . . 26
13637, 130, 45sylancr 646 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
1371, 43syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
138137ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
139138eleq2d 2556 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
140136, 139bitr3d 248 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
141140biimpd 200 . . . . . . . . . . . . . . . . . . . . . . . . . 26
142135, 141embantd 53 . . . . . . . . . . . . . . . . . . . . . . . . 25
143117ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
144 fvres 5721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
145144adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
146 onelon 4765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
147 fvco3 5784 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
148122, 146, 147sylancr 646 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
149145, 148eqtrd 2521 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
150143, 149sylan 459 . . . . . . . . . . . . . . . . . . . . . . . . . 26
151150eleq1d 2555 . . . . . . . . . . . . . . . . . . . . . . . . 25
152142, 151sylibrd 227 . . . . . . . . . . . . . . . . . . . . . . . 24
153152ralimdva 2838 . . . . . . . . . . . . . . . . . . . . . . 23
154153impr 604 . . . . . . . . . . . . . . . . . . . . . 22
155 ffnfv 5884 . . . . . . . . . . . . . . . . . . . . . 22
156129, 154, 155sylanbrc 647 . . . . . . . . . . . . . . . . . . . . 21
157 eleq2 2550 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
158157biimpa 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26
159 eliun 4201 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
160 cardon 8000 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
161160onelssi 4849 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
162149sseq2d 3421 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
163161, 162syl5ibr 214 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
164163reximdva 2872 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
165159, 164syl5bi 210 . . . . . . . . . . . . . . . . . . . . . . . . . 26
166158, 165syl5 31 . . . . . . . . . . . . . . . . . . . . . . . . 25
167166expdimp 428 . . . . . . . . . . . . . . . . . . . . . . . 24
168167ralrimiv 2842 . . . . . . . . . . . . . . . . . . . . . . 23
169168ex 425 . . . . . . . . . . . . . . . . . . . . . 22
170118, 169syl 16 . . . . . . . . . . . . . . . . . . . . 21
171 ffun 5579 . . . . . . . . . . . . . . . . . . . . . . . 24
172124, 171ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23
173 resfunexg 5958 . . . . . . . . . . . . . . . . . . . . . . 23
174172, 62, 173mp2an 655 . . . . . . . . . . . . . . . . . . . . . 22
175 feq1 5560 . . . . . . . . . . . . . . . . . . . . . . 23
176 fveq1 5707 . . . . . . . . . . . . . . . . . . . . . . . . . 26
177176sseq2d 3421 . . . . . . . . . . . . . . . . . . . . . . . . 25
178177rexbidv 2780 . . . . . . . . . . . . . . . . . . . . . . . 24
179178ralbidv 2779 . . . . . . . . . . . . . . . . . . . . . . 23
180175, 179anbi12d 693 . . . . . . . . . . . . . . . . . . . . . 22
181174, 180spcev 3104 . . . . . . . . . . . . . . . . . . . . 21
182156, 170, 181ee12an 1382 . . . . . . . . . . . . . . . . . . . 20
1833ad2antrl 710 . . . . . . . . . . . . . . . . . . . . 21
184 cfflb 8310 . . . . . . . . . . . . . . . . . . . . 21
185183, 118, 184syl2anc 644 . . . . . . . . . . . . . . . . . . . 20
186182, 185syld 43 . . . . . . . . . . . . . . . . . . 19
18749simp2bi 978 . . . . . . . . . . . . . . . . . . . . 21
188187sseq1d 3420 . . . . . . . . . . . . . . . . . . . 20
189188ad2antrl 710 . . . . . . . . . . . . . . . . . . 19
190186, 189sylibd 207 . . . . . . . . . . . . . . . . . 18
191 ontri1 4774 . . . . . . . . . . . . . . . . . . 19
192183, 118, 191syl2anc 644 . . . . . . . . . . . . . . . . . 18
193190,