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

Theorem inar1 8764
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 8679 . . . . . 6
2 winaon 8677 . . . . . 6
31, 2syl 16 . . . . 5
4 winalim 8684 . . . . . 6
51, 4syl 16 . . . . 5
6 r1lim 7810 . . . . 5
73, 5, 6syl2anc 644 . . . 4
8 onelon 4747 . . . . . . . . 9
93, 8sylan 459 . . . . . . . 8
10 eleq1 2541 . . . . . . . . . . 11
11 fveq2 5685 . . . . . . . . . . . 12
1211breq1d 4312 . . . . . . . . . . 11
1310, 12imbi12d 313 . . . . . . . . . 10
14 eleq1 2541 . . . . . . . . . . 11
15 fveq2 5685 . . . . . . . . . . . 12
1615breq1d 4312 . . . . . . . . . . 11
1714, 16imbi12d 313 . . . . . . . . . 10
18 eleq1 2541 . . . . . . . . . . 11
19 fveq2 5685 . . . . . . . . . . . 12
2019breq1d 4312 . . . . . . . . . . 11
2118, 20imbi12d 313 . . . . . . . . . 10
22 ne0i 3666 . . . . . . . . . . . . 13
23 0sdomg 7348 . . . . . . . . . . . . 13
2422, 23syl5ibr 214 . . . . . . . . . . . 12
25 r10 7806 . . . . . . . . . . . . 13
2625breq1i 4309 . . . . . . . . . . . 12
2724, 26syl6ibr 220 . . . . . . . . . . 11
281, 2, 273syl 19 . . . . . . . . . 10
29 eloni 4732 . . . . . . . . . . . . . . 15
30 ordtr 4736 . . . . . . . . . . . . . . 15
3129, 30syl 16 . . . . . . . . . . . . . 14
32 trsuc 4807 . . . . . . . . . . . . . . 15
3332ex 425 . . . . . . . . . . . . . 14
343, 31, 333syl 19 . . . . . . . . . . . . 13
3534adantl 454 . . . . . . . . . . . 12
36 r1suc 7808 . . . . . . . . . . . . . . 15
37 fvex 5695 . . . . . . . . . . . . . . . . . 18
3837cardid 8536 . . . . . . . . . . . . . . . . 17
3938ensymi 7269 . . . . . . . . . . . . . . . 16
40 pwen 7392 . . . . . . . . . . . . . . . 16
4139, 40ax-mp 5 . . . . . . . . . . . . . . 15
4236, 41syl6eqbr 4339 . . . . . . . . . . . . . 14
43 winacard 8681 . . . . . . . . . . . . . . . . . . 19
4443eleq2d 2548 . . . . . . . . . . . . . . . . . 18
45 cardsdom 8544 . . . . . . . . . . . . . . . . . . 19
4637, 2, 45sylancr 646 . . . . . . . . . . . . . . . . . 18
4744, 46bitr3d 248 . . . . . . . . . . . . . . . . 17
481, 47syl 16 . . . . . . . . . . . . . . . 16
49 elina 8676 . . . . . . . . . . . . . . . . . 18
5049simp3bi 979 . . . . . . . . . . . . . . . . 17
51 pweq 3881 . . . . . . . . . . . . . . . . . . 19
5251breq1d 4312 . . . . . . . . . . . . . . . . . 18
5352rspccv 3099 . . . . . . . . . . . . . . . . 17
5450, 53syl 16 . . . . . . . . . . . . . . . 16
5548, 54sylbird 228 . . . . . . . . . . . . . . 15
5655imp 420 . . . . . . . . . . . . . 14
57 ensdomtr 7355 . . . . . . . . . . . . . 14
5842, 56, 57syl2an 465 . . . . . . . . . . . . 13
5958expr 600 . . . . . . . . . . . 12
6035, 59imim12d 71 . . . . . . . . . . 11
6160ex 425 . . . . . . . . . 10
62 vex 3009 . . . . . . . . . . . . . . . 16
63 r1lim 7810 . . . . . . . . . . . . . . . 16
6462, 63mpan 653 . . . . . . . . . . . . . . 15
65 nfcv 2617 . . . . . . . . . . . . . . . . . . 19
66 nfcv 2617 . . . . . . . . . . . . . . . . . . . 20
67 nfcv 2617 . . . . . . . . . . . . . . . . . . . 20
68 nfiu1 4210 . . . . . . . . . . . . . . . . . . . 20
6966, 67, 68nfbr 4346 . . . . . . . . . . . . . . . . . . 19
70 fveq2 5685 . . . . . . . . . . . . . . . . . . . 20
7170breq1d 4312 . . . . . . . . . . . . . . . . . . 19
72 fvex 5695 . . . . . . . . . . . . . . . . . . . . . 22
7362, 72iunex 6518 . . . . . . . . . . . . . . . . . . . . 21
74 ssiun2 4223 . . . . . . . . . . . . . . . . . . . . 21
75 ssdomg 7265 . . . . . . . . . . . . . . . . . . . . 21
7673, 74, 75mpsyl 62 . . . . . . . . . . . . . . . . . . . 20
77 endomtr 7277 . . . . . . . . . . . . . . . . . . . 20
7839, 76, 77sylancr 646 . . . . . . . . . . . . . . . . . . 19
7965, 69, 71, 78vtoclgaf 3066 . . . . . . . . . . . . . . . . . 18
8079rgen 2817 . . . . . . . . . . . . . . . . 17
81 iundom 8531 . . . . . . . . . . . . . . . . 17
8262, 80, 81mp2an 655 . . . . . . . . . . . . . . . 16
8362, 73unex 6344 . . . . . . . . . . . . . . . . . . . 20
84 ssun2 3544 . . . . . . . . . . . . . . . . . . . 20
85 ssdomg 7265 . . . . . . . . . . . . . . . . . . . 20
8683, 84, 85mp2 9 . . . . . . . . . . . . . . . . . . 19
8762xpdom2 7315 . . . . . . . . . . . . . . . . . . 19
8886, 87ax-mp 5 . . . . . . . . . . . . . . . . . 18
89 ssun1 3543 . . . . . . . . . . . . . . . . . . . 20
90 ssdomg 7265 . . . . . . . . . . . . . . . . . . . 20
9183, 89, 90mp2 9 . . . . . . . . . . . . . . . . . . 19
9283xpdom1 7319 . . . . . . . . . . . . . . . . . . 19
9391, 92ax-mp 5 . . . . . . . . . . . . . . . . . 18
94 domtr 7272 . . . . . . . . . . . . . . . . . 18
9588, 93, 94mp2an 655 . . . . . . . . . . . . . . . . 17
96 limomss 6446 . . . . . . . . . . . . . . . . . . . 20
9796, 89syl6ss 3393 . . . . . . . . . . . . . . . . . . 19
98 ssdomg 7265 . . . . . . . . . . . . . . . . . . 19
9983, 97, 98mpsyl 62 . . . . . . . . . . . . . . . . . 18
100 infxpidm 8551 . . . . . . . . . . . . . . . . . 18
10199, 100syl 16 . . . . . . . . . . . . . . . . 17
102 domentr 7278 . . . . . . . . . . . . . . . . 17
10395, 101, 102sylancr 646 . . . . . . . . . . . . . . . 16
104 domtr 7272 . . . . . . . . . . . . . . . 16
10582, 103, 104sylancr 646 . . . . . . . . . . . . . . 15
10664, 105eqbrtrd 4322 . . . . . . . . . . . . . 14
107106ad2antlr 709 . . . . . . . . . . . . 13
108 eleq1a 2550 . . . . . . . . . . . . . . . . . . 19
109 ordirr 4740 . . . . . . . . . . . . . . . . . . . 20
1103, 29, 1093syl 19 . . . . . . . . . . . . . . . . . . 19
111108, 110nsyli 136 . . . . . . . . . . . . . . . . . 18
112111imp 420 . . . . . . . . . . . . . . . . 17
113112ad2ant2r 729 . . . . . . . . . . . . . . . 16
114 simpll 732 . . . . . . . . . . . . . . . . 17
115 limord 4781 . . . . . . . . . . . . . . . . . . . . . . . . 25
11662elon 4731 . . . . . . . . . . . . . . . . . . . . . . . . 25
117115, 116sylibr 205 . . . . . . . . . . . . . . . . . . . . . . . 24
118117ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . 23
119 cardf 8539 . . . . . . . . . . . . . . . . . . . . . . . . 25
120 r1fnon 7805 . . . . . . . . . . . . . . . . . . . . . . . . . 26
121 dffn2 5557 . . . . . . . . . . . . . . . . . . . . . . . . . 26
122120, 121mpbi 201 . . . . . . . . . . . . . . . . . . . . . . . . 25
123 fco 5565 . . . . . . . . . . . . . . . . . . . . . . . . 25
124119, 122, 123mp2an 655 . . . . . . . . . . . . . . . . . . . . . . . 24
125 onss 6367 . . . . . . . . . . . . . . . . . . . . . . . 24
126 fssres 5574 . . . . . . . . . . . . . . . . . . . . . . . 24
127124, 125, 126sylancr 646 . . . . . . . . . . . . . . . . . . . . . . 23
128 ffn 5556 . . . . . . . . . . . . . . . . . . . . . . 23
129118, 127, 1283syl 19 . . . . . . . . . . . . . . . . . . . . . 22
1303ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
131 simpr 449 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
132 simplll 736 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
133 ontr1 4768 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
134133imp 420 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
135130, 131, 132, 134syl12anc 1190 . . . . . . . . . . . . . . . . . . . . . . . . . 26
13637, 130, 45sylancr 646 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
1371, 43syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
138137ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
139138eleq2d 2548 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
140136, 139bitr3d 248 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
141140biimpd 200 . . . . . . . . . . . . . . . . . . . . . . . . . 26
142135, 141embantd 53 . . . . . . . . . . . . . . . . . . . . . . . . 25
143117ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
144 fvres 5698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
145144adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
146 onelon 4747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
147 fvco3 5761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
148122, 146, 147sylancr 646 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
149145, 148eqtrd 2513 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
150143, 149sylan 459 . . . . . . . . . . . . . . . . . . . . . . . . . 26
151150eleq1d 2547 . . . . . . . . . . . . . . . . . . . . . . . . 25
152142, 151sylibrd 227 . . . . . . . . . . . . . . . . . . . . . . . 24
153152ralimdva 2830 . . . . . . . . . . . . . . . . . . . . . . 23
154153impr 604 . . . . . . . . . . . . . . . . . . . . . 22
155 ffnfv 5856 . . . . . . . . . . . . . . . . . . . . . 22
156129, 154, 155sylanbrc 647 . . . . . . . . . . . . . . . . . . . . 21
157 eleq2 2542 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
158157biimpa 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26
159 eliun 4185 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
160 cardon 7945 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
161160onelssi 4831 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
162149sseq2d 3409 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
163161, 162syl5ibr 214 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
164163reximdva 2864 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
165159, 164syl5bi 210 . . . . . . . . . . . . . . . . . . . . . . . . . 26
166158, 165syl5 31 . . . . . . . . . . . . . . . . . . . . . . . . 25
167166expdimp 428 . . . . . . . . . . . . . . . . . . . . . . . 24
168167ralrimiv 2834 . . . . . . . . . . . . . . . . . . . . . . 23
169168ex 425 . . . . . . . . . . . . . . . . . . . . . 22
170118, 169syl 16 . . . . . . . . . . . . . . . . . . . . 21
171 ffun 5558 . . . . . . . . . . . . . . . . . . . . . . . 24
172124, 171ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23
173 resfunexg 5922 . . . . . . . . . . . . . . . . . . . . . . 23
174172, 62, 173mp2an 655 . . . . . . . . . . . . . . . . . . . . . 22
175 feq1 5539 . . . . . . . . . . . . . . . . . . . . . . 23
176 fveq1 5684 . . . . . . . . . . . . . . . . . . . . . . . . . 26
177176sseq2d 3409 . . . . . . . . . . . . . . . . . . . . . . . . 25
178177rexbidv 2772 . . . . . . . . . . . . . . . . . . . . . . . 24
179178ralbidv 2771 . . . . . . . . . . . . . . . . . . . . . . 23
180175, 179anbi12d 693 . . . . . . . . . . . . . . . . . . . . . 22
181174, 180spcev 3093 . . . . . . . . . . . . . . . . . . . . 21
182156, 170, 181ee12an 1381 . . . . . . . . . . . . . . . . . . . 20
1833ad2antrl 710 . . . . . . . . . . . . . . . . . . . . 21
184 cfflb 8253 . . . . . . . . . . . . . . . . . . . . 21
185183, 118, 184syl2anc 644 . . . . . . . . . . . . . . . . . . . 20
186182, 185syld 43 . . . . . . . . . . . . . . . . . . 19
18749simp2bi 978 . . . . . . . . . . . . . . . . . . . . 21
188187sseq1d 3408 . . . . . . . . . . . . . . . . . . . 20
189188ad2antrl 710 . . . . . . . . . . . . . . . . . . 19
190186, 189sylibd 207 . . . . . . . . . . . . . . . . . 18
191 ontri1 4756 . . . . . . . . . . . . . . . . . . 19
192183, 118, 191syl2anc 644 . . . . . . . . . . . . . . . . . 18
193190, 192sylibd 207 . . . . . . . . . . . . . . . . 17
194114, 193mt2d 112 . . . . . . . . . . . . . . . 16