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

Theorem canthp1lem2 9052
Description: Lemma for canthp1 9053. (Contributed by Mario Carneiro, 18-May-2015.)
Hypotheses
Ref Expression
canthp1lem2.1
canthp1lem2.2
canthp1lem2.3
canthp1lem2.4
canthp1lem2.5
canthp1lem2.6
Assertion
Ref Expression
canthp1lem2
Distinct variable groups:   , , ,   , , ,   , , ,   , , ,   , , ,

Proof of Theorem canthp1lem2
StepHypRef Expression
1 canthp1lem2.1 . . . . . 6
2 relsdom 7543 . . . . . . 7
32brrelex2i 5046 . . . . . 6
41, 3syl 16 . . . . 5
5 pwexg 4636 . . . . 5
64, 5syl 16 . . . 4
7 canthp1lem2.2 . . . 4
8 f1oeng 7554 . . . 4
96, 7, 8syl2anc 661 . . 3
10 ensym 7584 . . 3
119, 10syl 16 . 2
12 canth2g 7691 . . . . . . . . . . 11
134, 12syl 16 . . . . . . . . . 10
14 sdomen2 7682 . . . . . . . . . . 11
159, 14syl 16 . . . . . . . . . 10
1613, 15mpbid 210 . . . . . . . . 9
17 sdomnen 7564 . . . . . . . . 9
1816, 17syl 16 . . . . . . . 8
19 omelon 8084 . . . . . . . . . . . 12
20 onenon 8351 . . . . . . . . . . . 12
2119, 20ax-mp 5 . . . . . . . . . . 11
22 canthp1lem2.3 . . . . . . . . . . . . . . . . . . . 20
23 dff1o3 5827 . . . . . . . . . . . . . . . . . . . . . . 23
2423simprbi 464 . . . . . . . . . . . . . . . . . . . . . 22
257, 24syl 16 . . . . . . . . . . . . . . . . . . . . 21
26 f1ofo 5828 . . . . . . . . . . . . . . . . . . . . . . 23
277, 26syl 16 . . . . . . . . . . . . . . . . . . . . . 22
28 f1ofn 5822 . . . . . . . . . . . . . . . . . . . . . . 23
29 fnresdm 5695 . . . . . . . . . . . . . . . . . . . . . . 23
30 foeq1 5796 . . . . . . . . . . . . . . . . . . . . . . 23
317, 28, 29, 304syl 21 . . . . . . . . . . . . . . . . . . . . . 22
3227, 31mpbird 232 . . . . . . . . . . . . . . . . . . . . 21
33 fvex 5881 . . . . . . . . . . . . . . . . . . . . . . . 24
34 f1osng 5859 . . . . . . . . . . . . . . . . . . . . . . . 24
354, 33, 34sylancl 662 . . . . . . . . . . . . . . . . . . . . . . 23
367, 28syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
37 pwidg 4025 . . . . . . . . . . . . . . . . . . . . . . . . . 26
384, 37syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
39 fnressn 6083 . . . . . . . . . . . . . . . . . . . . . . . . 25
4036, 38, 39syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . 24
41 f1oeq1 5812 . . . . . . . . . . . . . . . . . . . . . . . 24
4240, 41syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
4335, 42mpbird 232 . . . . . . . . . . . . . . . . . . . . . 22
44 f1ofo 5828 . . . . . . . . . . . . . . . . . . . . . 22
4543, 44syl 16 . . . . . . . . . . . . . . . . . . . . 21
46 resdif 5841 . . . . . . . . . . . . . . . . . . . . 21
4725, 32, 45, 46syl3anc 1228 . . . . . . . . . . . . . . . . . . . 20
48 f1oco 5843 . . . . . . . . . . . . . . . . . . . 20
4922, 47, 48syl2anc 661 . . . . . . . . . . . . . . . . . . 19
50 resco 5516 . . . . . . . . . . . . . . . . . . . 20
51 f1oeq1 5812 . . . . . . . . . . . . . . . . . . . 20
5250, 51ax-mp 5 . . . . . . . . . . . . . . . . . . 19
5349, 52sylibr 212 . . . . . . . . . . . . . . . . . 18
54 f1of 5821 . . . . . . . . . . . . . . . . . 18
5553, 54syl 16 . . . . . . . . . . . . . . . . 17
56 0elpw 4621 . . . . . . . . . . . . . . . . . . . . 21
5756a1i 11 . . . . . . . . . . . . . . . . . . . 20
58 sdom0 7669 . . . . . . . . . . . . . . . . . . . . . . . 24
59 breq2 4456 . . . . . . . . . . . . . . . . . . . . . . . 24
6058, 59mtbii 302 . . . . . . . . . . . . . . . . . . . . . . 23
6160necon2ai 2692 . . . . . . . . . . . . . . . . . . . . . 22
621, 61syl 16 . . . . . . . . . . . . . . . . . . . . 21
6362ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20
64 eldifsn 4155 . . . . . . . . . . . . . . . . . . . 20
6557, 63, 64sylanbrc 664 . . . . . . . . . . . . . . . . . . 19
66 simplr 755 . . . . . . . . . . . . . . . . . . . 20
67 simpr 461 . . . . . . . . . . . . . . . . . . . . 21
6867neqned 2660 . . . . . . . . . . . . . . . . . . . 20
69 eldifsn 4155 . . . . . . . . . . . . . . . . . . . 20
7066, 68, 69sylanbrc 664 . . . . . . . . . . . . . . . . . . 19
7165, 70ifclda 3973 . . . . . . . . . . . . . . . . . 18
72 eqid 2457 . . . . . . . . . . . . . . . . . 18
7371, 72fmptd 6055 . . . . . . . . . . . . . . . . 17
74 fco 5746 . . . . . . . . . . . . . . . . 17
7555, 73, 74syl2anc 661 . . . . . . . . . . . . . . . 16
76 frn 5742 . . . . . . . . . . . . . . . . . . . 20
7773, 76syl 16 . . . . . . . . . . . . . . . . . . 19
78 cores 5515 . . . . . . . . . . . . . . . . . . 19
7977, 78syl 16 . . . . . . . . . . . . . . . . . 18
80 canthp1lem2.4 . . . . . . . . . . . . . . . . . 18
8179, 80syl6eqr 2516 . . . . . . . . . . . . . . . . 17
8281feq1d 5722 . . . . . . . . . . . . . . . 16
8375, 82mpbid 210 . . . . . . . . . . . . . . 15
84 inss1 3717 . . . . . . . . . . . . . . . 16
8584a1i 11 . . . . . . . . . . . . . . 15
86 canthp1lem2.5 . . . . . . . . . . . . . . . 16
87 canthp1lem2.6 . . . . . . . . . . . . . . . 16
88 eqid 2457 . . . . . . . . . . . . . . . 16
8986, 87, 88canth4 9046 . . . . . . . . . . . . . . 15
904, 83, 85, 89syl3anc 1228 . . . . . . . . . . . . . 14
9190simp1d 1008 . . . . . . . . . . . . 13
9290simp2d 1009 . . . . . . . . . . . . . . . . 17
9392pssned 3601 . . . . . . . . . . . . . . . 16
9493necomd 2728 . . . . . . . . . . . . . . 15
9590simp3d 1010 . . . . . . . . . . . . . . . . . . . . . . 23
9680fveq1i 5872 . . . . . . . . . . . . . . . . . . . . . . 23
9780fveq1i 5872 . . . . . . . . . . . . . . . . . . . . . . 23
9895, 96, 973eqtr3g 2521 . . . . . . . . . . . . . . . . . . . . . 22
99 elpw2g 4615 . . . . . . . . . . . . . . . . . . . . . . . . 25
1004, 99syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
10191, 100mpbird 232 . . . . . . . . . . . . . . . . . . . . . . 23
102 fvco3 5950 . . . . . . . . . . . . . . . . . . . . . . 23
10373, 101, 102syl2anc 661 . . . . . . . . . . . . . . . . . . . . . 22
10492pssssd 3600 . . . . . . . . . . . . . . . . . . . . . . . . 25
105104, 91sstrd 3513 . . . . . . . . . . . . . . . . . . . . . . . 24
106 elpw2g 4615 . . . . . . . . . . . . . . . . . . . . . . . . 25
1074, 106syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
108105, 107mpbird 232 . . . . . . . . . . . . . . . . . . . . . . 23
109 fvco3 5950 . . . . . . . . . . . . . . . . . . . . . . 23
11073, 108, 109syl2anc 661 . . . . . . . . . . . . . . . . . . . . . 22
11198, 103, 1103eqtr3d 2506 . . . . . . . . . . . . . . . . . . . . 21
112111adantr 465 . . . . . . . . . . . . . . . . . . . 20
113 ifcl 3983 . . . . . . . . . . . . . . . . . . . . . . . 24
11456, 101, 113sylancr 663 . . . . . . . . . . . . . . . . . . . . . . 23
115 eqeq1 2461 . . . . . . . . . . . . . . . . . . . . . . . . 25
116 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25
117115, 116ifbieq2d 3966 . . . . . . . . . . . . . . . . . . . . . . . 24
118117, 72fvmptg 5954 . . . . . . . . . . . . . . . . . . . . . . 23
119101, 114, 118syl2anc 661 . . . . . . . . . . . . . . . . . . . . . 22
120 pssne 3599 . . . . . . . . . . . . . . . . . . . . . . . 24
121120neneqd 2659 . . . . . . . . . . . . . . . . . . . . . . 23
122121iffalsed 3952 . . . . . . . . . . . . . . . . . . . . . 22
123119, 122sylan9eq 2518 . . . . . . . . . . . . . . . . . . . . 21
124123fveq2d 5875 . . . . . . . . . . . . . . . . . . . 20
125 ifcl 3983 . . . . . . . . . . . . . . . . . . . . . . . . 25
12656, 108, 125sylancr 663 . . . . . . . . . . . . . . . . . . . . . . . 24
127 eqeq1 2461 . . . . . . . . . . . . . . . . . . . . . . . . . 26
128 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26
129127, 128ifbieq2d 3966 . . . . . . . . . . . . . . . . . . . . . . . . 25
130129, 72fvmptg 5954 . . . . . . . . . . . . . . . . . . . . . . . 24
131108, 126, 130syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . 23
132131adantr 465 . . . . . . . . . . . . . . . . . . . . . 22
133 sspsstr 3608 . . . . . . . . . . . . . . . . . . . . . . . . . 26
134104, 133sylan 471 . . . . . . . . . . . . . . . . . . . . . . . . 25
135134pssned 3601 . . . . . . . . . . . . . . . . . . . . . . . 24
136135neneqd 2659 . . . . . . . . . . . . . . . . . . . . . . 23
137136iffalsed 3952 . . . . . . . . . . . . . . . . . . . . . 22
138132, 137eqtrd 2498 . . . . . . . . . . . . . . . . . . . . 21
139138fveq2d 5875 . . . . . . . . . . . . . . . . . . . 20
140112, 124, 1393eqtr3d 2506 . . . . . . . . . . . . . . . . . . 19
141101, 120anim12i 566 . . . . . . . . . . . . . . . . . . . . 21
142 eldifsn 4155 . . . . . . . . . . . . . . . . . . . . 21
143141, 142sylibr 212 . . . . . . . . . . . . . . . . . . . 20
144 fvres 5885 . . . . . . . . . . . . . . . . . . . 20
145143, 144syl 16 . . . . . . . . . . . . . . . . . . 19
146108adantr 465 . . . . . . . . . . . . . . . . . . . . 21
147 eldifsn 4155 . . . . . . . . . . . . . . . . . . . . 21
148146, 135, 147sylanbrc 664 . . . . . . . . . . . . . . . . . . . 20
149 fvres 5885 . . . . . . . . . . . . . . . . . . . 20
150148, 149syl 16 . . . . . . . . . . . . . . . . . . 19
151140, 145, 1503eqtr4d 2508 . . . . . . . . . . . . . . . . . 18
152 f1of1 5820 . . . . . . . . . . . . . . . . . . . . 21
15353, 152syl 16 . . . . . . . . . . . . . . . . . . . 20
154153adantr 465 . . . . . . . . . . . . . . . . . . 19
155 f1fveq 6170 . . . . . . . . . . . . . . . . . . 19
156154, 143, 148, 155syl12anc 1226 . . . . . . . . . . . . . . . . . 18
157151, 156mpbid 210 . . . . . . . . . . . . . . . . 17
158157ex 434 . . . . . . . . . . . . . . . 16
159158necon3ad 2667 . . . . . . . . . . . . . . 15
16094, 159mpd 15 . . . . . . . . . . . . . 14
161 npss 3613 . . . . . . . . . . . . . 14
162160, 161sylib 196 . . . . . . . . . . . . 13
16391, 162mpd 15 . . . . . . . . . . . 12
164 eqid 2457 . . . . . . . . . . . . . . . . . . . 20
165 eqid 2457 . . . . . . . . . . . . . . . . . . . 20
166164, 165pm3.2i 455 . . . . . . . . . . . . . . . . . . 19
16784sseli 3499 . . . . . . . . . . . . . . . . . . . . 21
168 ffvelrn 6029 . . . . . . . . . . . . . . . . . . . . 21
16983, 167, 168syl2an 477 . . . . . . . . . . . . . . . . . . . 20
17086, 4, 169, 87fpwwe 9045 . . . . . . . . . . . . . . . . . . 19
171166, 170mpbiri 233 . . . . . . . . . . . . . . . . . 18
172171simpld 459 . . . . . . . . . . . . . . . . 17
17386, 4fpwwelem 9044 . . . . . . . . . . . . . . . . 17
174172, 173mpbid 210 . . . . . . . . . . . . . . . 16
175174simprd 463 . . . . . . . . . . . . . . 15
176175simpld 459 . . . . . . . . . . . . . 14
177 fvex 5881 . . . . . . . . . . . . . . 15
178 weeq1 4872 . . . . . . . . . . . . . . 15
179177, 178spcev 3201 . . . . . . . . . . . . . 14
180176, 179syl 16 . . . . . . . . . . . . 13
181 ween 8437 . . . . . . . . . . . . 13
182180, 181sylibr 212 . . . . . . . . . . . 12
183163, 182eqeltrrd 2546 . . . . . . . . . . 11
184 domtri2 8391 . . . . . . . . . . 11
18521, 183, 184sylancr 663 . . . . . . . . . 10
186 infcda1 8594 . . . . . . . . . 10
187185, 186syl6bir 229 . . . . . . . . 9
188 ensym 7584 . . . . . . . . 9
189187, 188syl6 33 . . . . . . . 8
19018, 189mt3d 125 . . . . . . 7
191 2onn 7308 . . . . . . . 8
192 nnsdom 8091 . . . . . . . 8
193191, 192ax-mp 5 . . . . . . 7
194 cdafi 8591 . . . . . . 7
195190, 193, 194sylancl 662 . . . . . 6
196 isfinite 8090 . . . . . 6
197195, 196sylibr 212 . . . . 5
198 sssucid 4960 . . . . . . . . . 10
199 df-2o 7150 . . . . . . . . . 10
200198, 199sseqtr4i 3536 . . . . . . . . 9
201 xpss1 5116 . . . . . . . . 9
202200, 201ax-mp 5 . . . . . . . 8
203 unss2 3674 . . . . . . . 8
204202, 203mp1i 12 . . . . . . 7
205 ssun2 3667 . . . . . . . . 9
206 1onn 7307 . . . . . . . . . . . . 13
207206elexi 3119 . . . . . . . . . . . 12
208207sucid 4962 . . . . . . . . . . 11
209208, 199eleqtrri 2544 . . . . . . . . . 10
210207snid 4057 . . . . . . . . . 10
211 opelxpi 5036 . . . . . . . . . 10
212209, 210, 211mp2an 672 . . . . . . . . 9
213205, 212sselii 3500 . . . . . . . 8