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

Theorem inar1 8701
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 8616 . . . . . 6
2 winaon 8614 . . . . . 6
31, 2syl 16 . . . . 5
4 winalim 8621 . . . . . 6
51, 4syl 16 . . . . 5
6 r1lim 7747 . . . . 5
73, 5, 6syl2anc 644 . . . 4
8 onelon 4647 . . . . . . . . 9
93, 8sylan 459 . . . . . . . 8
10 eleq1 2503 . . . . . . . . . . 11
11 fveq2 5775 . . . . . . . . . . . 12
1211breq1d 4253 . . . . . . . . . . 11
1310, 12imbi12d 313 . . . . . . . . . 10
14 eleq1 2503 . . . . . . . . . . 11
15 fveq2 5775 . . . . . . . . . . . 12
1615breq1d 4253 . . . . . . . . . . 11
1714, 16imbi12d 313 . . . . . . . . . 10
18 eleq1 2503 . . . . . . . . . . 11
19 fveq2 5775 . . . . . . . . . . . 12
2019breq1d 4253 . . . . . . . . . . 11
2118, 20imbi12d 313 . . . . . . . . . 10
22 ne0i 3622 . . . . . . . . . . . . 13
23 0sdomg 7285 . . . . . . . . . . . . 13
2422, 23syl5ibr 214 . . . . . . . . . . . 12
25 r10 7743 . . . . . . . . . . . . 13
2625breq1i 4250 . . . . . . . . . . . 12
2724, 26syl6ibr 220 . . . . . . . . . . 11
281, 2, 273syl 19 . . . . . . . . . 10
29 eloni 4632 . . . . . . . . . . . . . . 15
30 ordtr 4636 . . . . . . . . . . . . . . 15
3129, 30syl 16 . . . . . . . . . . . . . 14
32 trsuc 4707 . . . . . . . . . . . . . . 15
3332ex 425 . . . . . . . . . . . . . 14
343, 31, 333syl 19 . . . . . . . . . . . . 13
3534adantl 454 . . . . . . . . . . . 12
36 r1suc 7745 . . . . . . . . . . . . . . 15
37 fvex 5785 . . . . . . . . . . . . . . . . . 18
3837cardid 8473 . . . . . . . . . . . . . . . . 17
3938ensymi 7206 . . . . . . . . . . . . . . . 16
40 pwen 7329 . . . . . . . . . . . . . . . 16
4139, 40ax-mp 5 . . . . . . . . . . . . . . 15
4236, 41syl6eqbr 4280 . . . . . . . . . . . . . 14
43 winacard 8618 . . . . . . . . . . . . . . . . . . 19
4443eleq2d 2510 . . . . . . . . . . . . . . . . . 18
45 cardsdom 8481 . . . . . . . . . . . . . . . . . . 19
4637, 2, 45sylancr 646 . . . . . . . . . . . . . . . . . 18
4744, 46bitr3d 248 . . . . . . . . . . . . . . . . 17
481, 47syl 16 . . . . . . . . . . . . . . . 16
49 elina 8613 . . . . . . . . . . . . . . . . . 18
5049simp3bi 975 . . . . . . . . . . . . . . . . 17
51 pweq 3829 . . . . . . . . . . . . . . . . . . 19
5251breq1d 4253 . . . . . . . . . . . . . . . . . 18
5352rspccv 3058 . . . . . . . . . . . . . . . . 17
5450, 53syl 16 . . . . . . . . . . . . . . . 16
5548, 54sylbird 228 . . . . . . . . . . . . . . 15
5655imp 420 . . . . . . . . . . . . . 14
57 ensdomtr 7292 . . . . . . . . . . . . . 14
5842, 56, 57syl2an 465 . . . . . . . . . . . . 13
5958expr 600 . . . . . . . . . . . 12
6035, 59imim12d 71 . . . . . . . . . . 11
6160ex 425 . . . . . . . . . 10
62 vex 2968 . . . . . . . . . . . . . . . 16
63 r1lim 7747 . . . . . . . . . . . . . . . 16
6462, 63mpan 653 . . . . . . . . . . . . . . 15
65 nfcv 2579 . . . . . . . . . . . . . . . . . . 19
66 nfcv 2579 . . . . . . . . . . . . . . . . . . . 20
67 nfcv 2579 . . . . . . . . . . . . . . . . . . . 20
68 nfiu1 4151 . . . . . . . . . . . . . . . . . . . 20
6966, 67, 68nfbr 4287 . . . . . . . . . . . . . . . . . . 19
70 fveq2 5775 . . . . . . . . . . . . . . . . . . . 20
7170breq1d 4253 . . . . . . . . . . . . . . . . . . 19
72 fvex 5785 . . . . . . . . . . . . . . . . . . . . . 22
7362, 72iunex 6039 . . . . . . . . . . . . . . . . . . . . 21
74 ssiun2 4164 . . . . . . . . . . . . . . . . . . . . 21
75 ssdomg 7202 . . . . . . . . . . . . . . . . . . . . 21
7673, 74, 75mpsyl 62 . . . . . . . . . . . . . . . . . . . 20
77 endomtr 7214 . . . . . . . . . . . . . . . . . . . 20
7839, 76, 77sylancr 646 . . . . . . . . . . . . . . . . . . 19
7965, 69, 71, 78vtoclgaf 3025 . . . . . . . . . . . . . . . . . 18
8079rgen 2778 . . . . . . . . . . . . . . . . 17
81 iundom 8468 . . . . . . . . . . . . . . . . 17
8262, 80, 81mp2an 655 . . . . . . . . . . . . . . . 16
8362, 73unex 4748 . . . . . . . . . . . . . . . . . . . 20
84 ssun2 3500 . . . . . . . . . . . . . . . . . . . 20
85 ssdomg 7202 . . . . . . . . . . . . . . . . . . . 20
8683, 84, 85mp2 9 . . . . . . . . . . . . . . . . . . 19
8762xpdom2 7252 . . . . . . . . . . . . . . . . . . 19
8886, 87ax-mp 5 . . . . . . . . . . . . . . . . . 18
89 ssun1 3499 . . . . . . . . . . . . . . . . . . . 20
90 ssdomg 7202 . . . . . . . . . . . . . . . . . . . 20
9183, 89, 90mp2 9 . . . . . . . . . . . . . . . . . . 19
9283xpdom1 7256 . . . . . . . . . . . . . . . . . . 19
9391, 92ax-mp 5 . . . . . . . . . . . . . . . . . 18
94 domtr 7209 . . . . . . . . . . . . . . . . . 18
9588, 93, 94mp2an 655 . . . . . . . . . . . . . . . . 17
96 limomss 4891 . . . . . . . . . . . . . . . . . . . 20
9796, 89syl6ss 3349 . . . . . . . . . . . . . . . . . . 19
98 ssdomg 7202 . . . . . . . . . . . . . . . . . . 19
9983, 97, 98mpsyl 62 . . . . . . . . . . . . . . . . . 18
100 infxpidm 8488 . . . . . . . . . . . . . . . . . 18
10199, 100syl 16 . . . . . . . . . . . . . . . . 17
102 domentr 7215 . . . . . . . . . . . . . . . . 17
10395, 101, 102sylancr 646 . . . . . . . . . . . . . . . 16
104 domtr 7209 . . . . . . . . . . . . . . . 16
10582, 103, 104sylancr 646 . . . . . . . . . . . . . . 15
10664, 105eqbrtrd 4263 . . . . . . . . . . . . . 14
107106ad2antlr 709 . . . . . . . . . . . . 13
108 eleq1a 2512 . . . . . . . . . . . . . . . . . . 19
109 ordirr 4640 . . . . . . . . . . . . . . . . . . . 20
1103, 29, 1093syl 19 . . . . . . . . . . . . . . . . . . 19
111108, 110nsyli 136 . . . . . . . . . . . . . . . . . 18
112111imp 420 . . . . . . . . . . . . . . . . 17
113112ad2ant2r 729 . . . . . . . . . . . . . . . 16
114 simpll 732 . . . . . . . . . . . . . . . . 17
115 limord 4681 . . . . . . . . . . . . . . . . . . . . . . . . 25
11662elon 4631 . . . . . . . . . . . . . . . . . . . . . . . . 25
117115, 116sylibr 205 . . . . . . . . . . . . . . . . . . . . . . . 24
118117ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . 23
119 cardf 8476 . . . . . . . . . . . . . . . . . . . . . . . . 25
120 r1fnon 7742 . . . . . . . . . . . . . . . . . . . . . . . . . 26
121 dffn2 5639 . . . . . . . . . . . . . . . . . . . . . . . . . 26
122120, 121mpbi 201 . . . . . . . . . . . . . . . . . . . . . . . . 25
123 fco 5647 . . . . . . . . . . . . . . . . . . . . . . . . 25
124119, 122, 123mp2an 655 . . . . . . . . . . . . . . . . . . . . . . . 24
125 onss 4812 . . . . . . . . . . . . . . . . . . . . . . . 24
126 fssres 5657 . . . . . . . . . . . . . . . . . . . . . . . 24
127124, 125, 126sylancr 646 . . . . . . . . . . . . . . . . . . . . . . 23
128 ffn 5638 . . . . . . . . . . . . . . . . . . . . . . 23
129118, 127, 1283syl 19 . . . . . . . . . . . . . . . . . . . . . 22
1303ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
131 simpr 449 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
132 simplll 736 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
133 ontr1 4668 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
134133imp 420 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
135130, 131, 132, 134syl12anc 1183 . . . . . . . . . . . . . . . . . . . . . . . . . 26
13637, 130, 45sylancr 646 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
1371, 43syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
138137ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
139138eleq2d 2510 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
140136, 139bitr3d 248 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
141140biimpd 200 . . . . . . . . . . . . . . . . . . . . . . . . . 26
142135, 141embantd 53 . . . . . . . . . . . . . . . . . . . . . . . . 25
143117ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
144 fvres 5788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
145144adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
146 onelon 4647 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
147 fvco3 5848 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
148122, 146, 147sylancr 646 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
149145, 148eqtrd 2475 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
150143, 149sylan 459 . . . . . . . . . . . . . . . . . . . . . . . . . 26
151150eleq1d 2509 . . . . . . . . . . . . . . . . . . . . . . . . 25
152142, 151sylibrd 227 . . . . . . . . . . . . . . . . . . . . . . . 24
153152ralimdva 2791 . . . . . . . . . . . . . . . . . . . . . . 23
154153impr 604 . . . . . . . . . . . . . . . . . . . . . 22
155 ffnfv 5942 . . . . . . . . . . . . . . . . . . . . . 22
156129, 154, 155sylanbrc 647 . . . . . . . . . . . . . . . . . . . . 21
157 eleq2 2504 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
158157biimpa 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26
159 eliun 4126 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
160 cardon 7882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
161160onelssi 4731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
162149sseq2d 3365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
163161, 162syl5ibr 214 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
164163reximdva 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
165159, 164syl5bi 210 . . . . . . . . . . . . . . . . . . . . . . . . . 26
166158, 165syl5 31 . . . . . . . . . . . . . . . . . . . . . . . . 25
167166expdimp 428 . . . . . . . . . . . . . . . . . . . . . . . 24
168167ralrimiv 2795 . . . . . . . . . . . . . . . . . . . . . . 23
169168ex 425 . . . . . . . . . . . . . . . . . . . . . 22
170118, 169syl 16 . . . . . . . . . . . . . . . . . . . . 21
171 ffun 5640 . . . . . . . . . . . . . . . . . . . . . . . 24
172124, 171ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23
173 resfunexg 6005 . . . . . . . . . . . . . . . . . . . . . . 23
174172, 62, 173mp2an 655 . . . . . . . . . . . . . . . . . . . . . 22
175 feq1 5623 . . . . . . . . . . . . . . . . . . . . . . 23
176 fveq1 5774 . . . . . . . . . . . . . . . . . . . . . . . . . 26
177176sseq2d 3365 . . . . . . . . . . . . . . . . . . . . . . . . 25
178177rexbidv 2733 . . . . . . . . . . . . . . . . . . . . . . . 24
179178ralbidv 2732 . . . . . . . . . . . . . . . . . . . . . . 23
180175, 179anbi12d 693 . . . . . . . . . . . . . . . . . . . . . 22
181174, 180spcev 3052 . . . . . . . . . . . . . . . . . . . . 21
182156, 170, 181ee12an 1373 . . . . . . . . . . . . . . . . . . . 20
1833ad2antrl 710 . . . . . . . . . . . . . . . . . . . . 21
184 cfflb 8190 . . . . . . . . . . . . . . . . . . . . 21
185183, 118, 184syl2anc 644 . . . . . . . . . . . . . . . . . . . 20
186182, 185syld 43 . . . . . . . . . . . . . . . . . . 19
18749simp2bi 974 . . . . . . . . . . . . . . . . . . . . 21
188187sseq1d 3364 . . . . . . . . . . . . . . . . . . . 20
189188ad2antrl 710 . . . . . . . . . . . . . . . . . . 19
190186, 189sylibd 207 . . . . . . . . . . . . . . . . . 18
191 ontri1 4656 . . . . . . . . . . . . . . . . . . 19
192183, 118, 191syl2anc 644 . . . . . . . . . . . . . . . . . 18
193190, 192sylibd 207 . . . . . . . . . . . . . . . . 17
194114, 193mt2d 112 . . . . . . . . . . . . . . . 16