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

Theorem dfac12lem2 8545
Description: Lemma for dfac12 8550. (Contributed by Mario Carneiro, 29-May-2015.)
Hypotheses
Ref Expression
dfac12.1
dfac12.3
dfac12.4
dfac12.5
dfac12.h
dfac12.6
dfac12.8
Assertion
Ref Expression
dfac12lem2
Distinct variable groups:   , ,   , , ,   , , ,   , ,   , , ,   , ,

Proof of Theorem dfac12lem2
StepHypRef Expression
1 dfac12.4 . . . . . . . . . . . . . 14
21tfr1 7085 . . . . . . . . . . . . 13
3 fnfun 5683 . . . . . . . . . . . . 13
42, 3ax-mp 5 . . . . . . . . . . . 12
5 dfac12.5 . . . . . . . . . . . 12
6 funimaexg 5670 . . . . . . . . . . . 12
74, 5, 6sylancr 663 . . . . . . . . . . 11
8 uniexg 6597 . . . . . . . . . . 11
9 rnexg 6732 . . . . . . . . . . 11
107, 8, 93syl 20 . . . . . . . . . 10
11 dfac12.8 . . . . . . . . . . . . . . 15
12 f1f 5786 . . . . . . . . . . . . . . . . 17
13 fssxp 5748 . . . . . . . . . . . . . . . . 17
14 ssv 3523 . . . . . . . . . . . . . . . . . . . 20
15 xpss1 5116 . . . . . . . . . . . . . . . . . . . 20
1614, 15ax-mp 5 . . . . . . . . . . . . . . . . . . 19
17 sstr 3511 . . . . . . . . . . . . . . . . . . 19
1816, 17mpan2 671 . . . . . . . . . . . . . . . . . 18
19 fvex 5881 . . . . . . . . . . . . . . . . . . 19
2019elpw 4018 . . . . . . . . . . . . . . . . . 18
2118, 20sylibr 212 . . . . . . . . . . . . . . . . 17
2212, 13, 213syl 20 . . . . . . . . . . . . . . . 16
2322ralimi 2850 . . . . . . . . . . . . . . 15
2411, 23syl 16 . . . . . . . . . . . . . 14
25 onss 6626 . . . . . . . . . . . . . . . . 17
265, 25syl 16 . . . . . . . . . . . . . . . 16
27 fndm 5685 . . . . . . . . . . . . . . . . 17
282, 27ax-mp 5 . . . . . . . . . . . . . . . 16
2926, 28syl6sseqr 3550 . . . . . . . . . . . . . . 15
30 funimass4 5924 . . . . . . . . . . . . . . 15
314, 29, 30sylancr 663 . . . . . . . . . . . . . 14
3224, 31mpbird 232 . . . . . . . . . . . . 13
33 sspwuni 4416 . . . . . . . . . . . . 13
3432, 33sylib 196 . . . . . . . . . . . 12
35 rnss 5236 . . . . . . . . . . . 12
3634, 35syl 16 . . . . . . . . . . 11
37 rnxpss 5444 . . . . . . . . . . 11
3836, 37syl6ss 3515 . . . . . . . . . 10
39 ssonuni 6622 . . . . . . . . . 10
4010, 38, 39sylc 60 . . . . . . . . 9
41 suceloni 6648 . . . . . . . . 9
4240, 41syl 16 . . . . . . . 8
4342ad2antrr 725 . . . . . . 7
44 rankon 8234 . . . . . . 7
45 omcl 7205 . . . . . . 7
4643, 44, 45sylancl 662 . . . . . 6
47 rankr1ai 8237 . . . . . . . . . . . 12
4847ad2antlr 726 . . . . . . . . . . 11
49 simpr 461 . . . . . . . . . . 11
5048, 49eleqtrd 2547 . . . . . . . . . 10
51 eloni 4893 . . . . . . . . . . . . 13
525, 51syl 16 . . . . . . . . . . . 12
5352ad2antrr 725 . . . . . . . . . . 11
54 ordsucuniel 6659 . . . . . . . . . . 11
5553, 54syl 16 . . . . . . . . . 10
5650, 55mpbid 210 . . . . . . . . 9
5711ad2antrr 725 . . . . . . . . 9
58 fveq2 5871 . . . . . . . . . . . 12
59 f1eq1 5781 . . . . . . . . . . . 12
6058, 59syl 16 . . . . . . . . . . 11
61 fveq2 5871 . . . . . . . . . . . 12
62 f1eq2 5782 . . . . . . . . . . . 12
6361, 62syl 16 . . . . . . . . . . 11
6460, 63bitrd 253 . . . . . . . . . 10
6564rspcv 3206 . . . . . . . . 9
6656, 57, 65sylc 60 . . . . . . . 8
67 f1f 5786 . . . . . . . 8
6866, 67syl 16 . . . . . . 7
69 r1elwf 8235 . . . . . . . . 9
7069ad2antlr 726 . . . . . . . 8
71 rankidb 8239 . . . . . . . 8
7270, 71syl 16 . . . . . . 7
7368, 72ffvelrnd 6032 . . . . . 6
74 oacl 7204 . . . . . 6
7546, 73, 74syl2anc 661 . . . . 5
76 dfac12.3 . . . . . . . 8
77 f1f 5786 . . . . . . . 8
7876, 77syl 16 . . . . . . 7
7978ad2antrr 725 . . . . . 6
80 imassrn 5353 . . . . . . . 8
81 fvex 5881 . . . . . . . . . . . . . . 15
8281rnex 6734 . . . . . . . . . . . . . 14
835ad2antrr 725 . . . . . . . . . . . . . . . . . . 19
84 onuni 6628 . . . . . . . . . . . . . . . . . . 19
85 sucidg 4961 . . . . . . . . . . . . . . . . . . 19
8683, 84, 853syl 20 . . . . . . . . . . . . . . . . . 18
8752adantr 465 . . . . . . . . . . . . . . . . . . . 20
88 orduniorsuc 6665 . . . . . . . . . . . . . . . . . . . 20
8987, 88syl 16 . . . . . . . . . . . . . . . . . . 19
9089orcanai 913 . . . . . . . . . . . . . . . . . 18
9186, 90eleqtrrd 2548 . . . . . . . . . . . . . . . . 17
9211ad2antrr 725 . . . . . . . . . . . . . . . . 17
93 fveq2 5871 . . . . . . . . . . . . . . . . . . . 20
94 f1eq1 5781 . . . . . . . . . . . . . . . . . . . 20
9593, 94syl 16 . . . . . . . . . . . . . . . . . . 19
96 fveq2 5871 . . . . . . . . . . . . . . . . . . . 20
97 f1eq2 5782 . . . . . . . . . . . . . . . . . . . 20
9896, 97syl 16 . . . . . . . . . . . . . . . . . . 19
9995, 98bitrd 253 . . . . . . . . . . . . . . . . . 18
10099rspcv 3206 . . . . . . . . . . . . . . . . 17
10191, 92, 100sylc 60 . . . . . . . . . . . . . . . 16
102 f1f 5786 . . . . . . . . . . . . . . . 16
103 frn 5742 . . . . . . . . . . . . . . . 16
104101, 102, 1033syl 20 . . . . . . . . . . . . . . 15
105 epweon 6619 . . . . . . . . . . . . . . 15
106 wess 4871 . . . . . . . . . . . . . . 15
107104, 105, 106mpisyl 18 . . . . . . . . . . . . . 14
108 eqid 2457 . . . . . . . . . . . . . . 15
109108oiiso 7983 . . . . . . . . . . . . . 14
11082, 107, 109sylancr 663 . . . . . . . . . . . . 13
111 isof1o 6221 . . . . . . . . . . . . 13
112 f1ocnv 5833 . . . . . . . . . . . . 13
113 f1of1 5820 . . . . . . . . . . . . 13
114110, 111, 112, 1134syl 21 . . . . . . . . . . . 12
115 f1f1orn 5832 . . . . . . . . . . . . 13
116 f1of1 5820 . . . . . . . . . . . . 13
117101, 115, 1163syl 20 . . . . . . . . . . . 12
118 f1co 5795 . . . . . . . . . . . 12
119114, 117, 118syl2anc 661 . . . . . . . . . . 11
120 dfac12.h . . . . . . . . . . . 12
121 f1eq1 5781 . . . . . . . . . . . 12
122120, 121ax-mp 5 . . . . . . . . . . 11
123119, 122sylibr 212 . . . . . . . . . 10
124 f1f 5786 . . . . . . . . . 10
125 frn 5742 . . . . . . . . . 10
126123, 124, 1253syl 20 . . . . . . . . 9
127 harcl 8008 . . . . . . . . . . 11
128127onordi 4987 . . . . . . . . . 10
129108oion 7982 . . . . . . . . . . . 12
13082, 129mp1i 12 . . . . . . . . . . 11
131108oien 7984 . . . . . . . . . . . . 13
13282, 107, 131sylancr 663 . . . . . . . . . . . 12
133 fvex 5881 . . . . . . . . . . . . . . 15
134133f1oen 7556 . . . . . . . . . . . . . 14
135 ensym 7584 . . . . . . . . . . . . . 14
136101, 115, 134, 1354syl 21 . . . . . . . . . . . . 13
137 fvex 5881 . . . . . . . . . . . . . 14
138 dfac12.1 . . . . . . . . . . . . . . . 16
139138ad2antrr 725 . . . . . . . . . . . . . . 15
140 dfac12.6 . . . . . . . . . . . . . . . . 17
141140ad2antrr 725 . . . . . . . . . . . . . . . 16
142141, 91sseldd 3504 . . . . . . . . . . . . . . 15
143 r1ord2 8220 . . . . . . . . . . . . . . 15
144139, 142, 143sylc 60 . . . . . . . . . . . . . 14
145 ssdomg 7581 . . . . . . . . . . . . . 14
146137, 144, 145mpsyl 63 . . . . . . . . . . . . 13
147 endomtr 7593 . . . . . . . . . . . . 13
148136, 146, 147syl2anc 661 . . . . . . . . . . . 12
149 endomtr 7593 . . . . . . . . . . . 12
150132, 148, 149syl2anc 661 . . . . . . . . . . 11
151 elharval 8010 . . . . . . . . . . 11
152130, 150, 151sylanbrc 664 . . . . . . . . . 10
153 ordelss 4899 . . . . . . . . . 10
154128, 152, 153sylancr 663 . . . . . . . . 9
155126, 154sstrd 3513 . . . . . . . 8
15680, 155syl5ss 3514 . . . . . . 7
157 fvex 5881 . . . . . . . 8
158157elpw2 4616 . . . . . . 7
159156, 158sylibr 212 . . . . . 6
16079, 159ffvelrnd 6032 . . . . 5
16175, 160ifclda 3973 . . . 4
162161ex 434 . . 3
163 iftrue 3947 . . . . . . . 8
164 iftrue 3947 . . . . . . . 8
165163, 164eqeq12d 2479 . . . . . . 7
166165adantl 466 . . . . . 6
16742ad2antrr 725 . . . . . . 7
168 nsuceq0 4963 . . . . . . . 8
169168a1i 11 . . . . . . 7
17044a1i 11 . . . . . . 7
171 onsucuni 6663 . . . . . . . . . . 11
17238, 171syl 16 . . . . . . . . . 10
173172ad2antrr 725 . . . . . . . . 9
1742a1i 11 . . . . . . . . . . . 12
17526ad2antrr 725 . . . . . . . . . . . 12
176 fnfvima 6150 . . . . . . . . . . . 12