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

Theorem ptcmplem2 21068
 Description: Lemma for ptcmp 21073. (Contributed by Mario Carneiro, 26-Aug-2015.)
Hypotheses
Ref Expression
ptcmp.1
ptcmp.2
ptcmp.3
ptcmp.4
ptcmp.5 UFL
ptcmplem2.5
ptcmplem2.6
ptcmplem2.7
Assertion
Ref Expression
ptcmplem2
Distinct variable groups:   ,,,,,   ,,,,   ,,,   ,,,   ,,,,,   ,,,,,   ,,,,,
Allowed substitution hints:   (,)   ()   (,)

Proof of Theorem ptcmplem2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ptcmplem2.7 . . . 4
2 0ss 3763 . . . . . . 7
3 0fin 7799 . . . . . . 7
4 elfpw 7876 . . . . . . 7
52, 3, 4mpbir2an 931 . . . . . 6
6 unieq 4206 . . . . . . . . 9
7 uni0 4225 . . . . . . . . 9
86, 7syl6eq 2501 . . . . . . . 8
98eqeq2d 2461 . . . . . . 7
109rspcev 3150 . . . . . 6
115, 10mpan 676 . . . . 5
1211necon3bi 2650 . . . 4
131, 12syl 17 . . 3
14 n0 3741 . . 3
1513, 14sylib 200 . 2
16 ptcmp.2 . . . . . . 7
17 fveq2 5865 . . . . . . . . 9
1817unieqd 4208 . . . . . . . 8
1918cbvixpv 7540 . . . . . . 7
2016, 19eqtri 2473 . . . . . 6
21 inss2 3653 . . . . . . . 8 UFL
22 ptcmp.5 . . . . . . . 8 UFL
2321, 22sseldi 3430 . . . . . . 7
2423adantr 467 . . . . . 6
2520, 24syl5eqelr 2534 . . . . 5
26 ssrab2 3514 . . . . . 6
2713adantr 467 . . . . . . 7
2820, 27syl5eqner 2699 . . . . . 6
29 eqid 2451 . . . . . . 7
3029resixpfo 7560 . . . . . 6
3126, 28, 30sylancr 669 . . . . 5
32 fonum 8489 . . . . 5
3325, 31, 32syl2anc 667 . . . 4
34 vex 3048 . . . . . . . . . . 11
35 difexg 4551 . . . . . . . . . . 11
3634, 35mp1i 13 . . . . . . . . . 10
37 dmexg 6724 . . . . . . . . . 10
38 uniexg 6588 . . . . . . . . . 10
3936, 37, 383syl 18 . . . . . . . . 9
4039ralrimivw 2803 . . . . . . . 8
41 eqid 2451 . . . . . . . . 9
4241fnmpt 5704 . . . . . . . 8
4340, 42syl 17 . . . . . . 7
44 dffn4 5799 . . . . . . 7
4543, 44sylib 200 . . . . . 6
46 fonum 8489 . . . . . 6
4724, 45, 46syl2anc 667 . . . . 5
48 ssdif0 3823 . . . . . . . . . . . 12
49 simpr 463 . . . . . . . . . . . . . . 15
50 simpr 463 . . . . . . . . . . . . . . . . . . . 20
5150, 20syl6eleq 2539 . . . . . . . . . . . . . . . . . . 19
52 vex 3048 . . . . . . . . . . . . . . . . . . . . 21
5352elixp 7529 . . . . . . . . . . . . . . . . . . . 20
5453simprbi 466 . . . . . . . . . . . . . . . . . . 19
5551, 54syl 17 . . . . . . . . . . . . . . . . . 18
5655r19.21bi 2757 . . . . . . . . . . . . . . . . 17
5756snssd 4117 . . . . . . . . . . . . . . . 16
5857adantr 467 . . . . . . . . . . . . . . 15
5949, 58eqssd 3449 . . . . . . . . . . . . . 14
60 fvex 5875 . . . . . . . . . . . . . . 15
6160ensn1 7633 . . . . . . . . . . . . . 14
6259, 61syl6eqbr 4440 . . . . . . . . . . . . 13
6362ex 436 . . . . . . . . . . . 12
6448, 63syl5bir 222 . . . . . . . . . . 11
6564con3d 139 . . . . . . . . . 10
66 neq0 3742 . . . . . . . . . 10
6765, 66syl6ib 230 . . . . . . . . 9
68 eldifi 3555 . . . . . . . . . . . . 13
69 simplr 762 . . . . . . . . . . . . . . . . . 18
70 iftrue 3887 . . . . . . . . . . . . . . . . . . 19
7170, 18eleq12d 2523 . . . . . . . . . . . . . . . . . 18
7269, 71syl5ibrcom 226 . . . . . . . . . . . . . . . . 17
7350, 16syl6eleq 2539 . . . . . . . . . . . . . . . . . . . . 21
7452elixp 7529 . . . . . . . . . . . . . . . . . . . . . 22
7574simprbi 466 . . . . . . . . . . . . . . . . . . . . 21
7673, 75syl 17 . . . . . . . . . . . . . . . . . . . 20
7776ad2antrr 732 . . . . . . . . . . . . . . . . . . 19
7877r19.21bi 2757 . . . . . . . . . . . . . . . . . 18
79 iffalse 3890 . . . . . . . . . . . . . . . . . . 19
8079eleq1d 2513 . . . . . . . . . . . . . . . . . 18
8178, 80syl5ibrcom 226 . . . . . . . . . . . . . . . . 17
8272, 81pm2.61d 162 . . . . . . . . . . . . . . . 16
8382ralrimiva 2802 . . . . . . . . . . . . . . 15
84 ptcmp.3 . . . . . . . . . . . . . . . . 17
8584ad3antrrr 736 . . . . . . . . . . . . . . . 16
86 mptelixpg 7559 . . . . . . . . . . . . . . . 16
8785, 86syl 17 . . . . . . . . . . . . . . 15
8883, 87mpbird 236 . . . . . . . . . . . . . 14
8988, 16syl6eleqr 2540 . . . . . . . . . . . . 13
9068, 89sylan2 477 . . . . . . . . . . . 12
91 vex 3048 . . . . . . . . . . . . . 14
9291unisn 4213 . . . . . . . . . . . . 13
93 simplr 762 . . . . . . . . . . . . . . . . . . . 20
94 eleq1 2517 . . . . . . . . . . . . . . . . . . . 20
9593, 94syl5ibrcom 226 . . . . . . . . . . . . . . . . . . 19
9695pm4.71rd 641 . . . . . . . . . . . . . . . . . 18
97 equequ1 1867 . . . . . . . . . . . . . . . . . . . . . . . 24
98 fveq2 5865 . . . . . . . . . . . . . . . . . . . . . . . 24
9997, 98ifbieq2d 3906 . . . . . . . . . . . . . . . . . . . . . . 23
100 eqid 2451 . . . . . . . . . . . . . . . . . . . . . . 23
101 vex 3048 . . . . . . . . . . . . . . . . . . . . . . . 24
102 fvex 5875 . . . . . . . . . . . . . . . . . . . . . . . 24
103101, 102ifex 3949 . . . . . . . . . . . . . . . . . . . . . . 23
10499, 100, 103fvmpt 5948 . . . . . . . . . . . . . . . . . . . . . 22
105104neeq1d 2683 . . . . . . . . . . . . . . . . . . . . 21
106105adantl 468 . . . . . . . . . . . . . . . . . . . 20
107 iffalse 3890 . . . . . . . . . . . . . . . . . . . . . 22
108107necon1ai 2651 . . . . . . . . . . . . . . . . . . . . 21
109 eldifsni 4098 . . . . . . . . . . . . . . . . . . . . . . 23
110109ad2antlr 733 . . . . . . . . . . . . . . . . . . . . . 22
111 iftrue 3887 . . . . . . . . . . . . . . . . . . . . . . 23
112 fveq2 5865 . . . . . . . . . . . . . . . . . . . . . . 23
113111, 112neeq12d 2685 . . . . . . . . . . . . . . . . . . . . . 22
114110, 113syl5ibrcom 226 . . . . . . . . . . . . . . . . . . . . 21
115108, 114impbid2 208 . . . . . . . . . . . . . . . . . . . 20
116106, 115bitrd 257 . . . . . . . . . . . . . . . . . . 19
117116pm5.32da 647 . . . . . . . . . . . . . . . . . 18
11896, 117bitr4d 260 . . . . . . . . . . . . . . . . 17
119118abbidv 2569 . . . . . . . . . . . . . . . 16
120 df-sn 3969 . . . . . . . . . . . . . . . 16
121 df-rab 2746 . . . . . . . . . . . . . . . 16
122119, 120, 1213eqtr4g 2510 . . . . . . . . . . . . . . 15
123 fvex 5875 . . . . . . . . . . . . . . . . . . 19
124101, 123ifex 3949 . . . . . . . . . . . . . . . . . 18
125124rgenw 2749 . . . . . . . . . . . . . . . . 17
126100fnmpt 5704 . . . . . . . . . . . . . . . . 17
127125, 126mp1i 13 . . . . . . . . . . . . . . . 16
128 ixpfn 7528 . . . . . . . . . . . . . . . . . 18
12973, 128syl 17 . . . . . . . . . . . . . . . . 17
130129ad2antrr 732 . . . . . . . . . . . . . . . 16
131 fndmdif 5986 . . . . . . . . . . . . . . . 16
132127, 130, 131syl2anc 667 . . . . . . . . . . . . . . 15
133122, 132eqtr4d 2488 . . . . . . . . . . . . . 14
134133unieqd 4208 . . . . . . . . . . . . 13
13592, 134syl5eqr 2499 . . . . . . . . . . . 12
136 difeq1 3544 . . . . . . . . . . . . . . . 16
137136dmeqd 5037 . . . . . . . . . . . . . . 15
138137unieqd 4208 . . . . . . . . . . . . . 14
139138eqeq2d 2461 . . . . . . . . . . . . 13
140139rspcev 3150 . . . . . . . . . . . 12
14190, 135, 140syl2anc 667 . . . . . . . . . . 11
142141ex 436 . . . . . . . . . 10
143142exlimdv 1779 . . . . . . . . 9
14467, 143syld 45 . . . . . . . 8
145144expimpd 608 . . . . . . 7
14618breq1d 4412 . . . . . . . . 9
147146notbid 296 . . . . . . . 8
148147elrab 3196 . . . . . . 7
14941elrnmpt 5081 . . . . . . . 8
15091, 149ax-mp 5 . . . . . . 7
151145, 148, 1503imtr4g 274 . . . . . 6
152151ssrdv 3438 . . . . 5
153 ssnum 8470 . . . . 5
15447, 152, 153syl2anc 667 . . . 4
155 xpnum 8385 . . . 4
15633, 154, 155syl2anc 667 . . 3
15784adantr 467 . . . . 5
158 rabexg 4553 . . . . 5
159157, 158syl 17 . . . 4
160 fvex 5875 . . . . . . 7
161160uniex 6587 . . . . . 6
162161rgenw 2749 . . . . 5
163 iunexg 6769 . . . . 5
164159, 162, 163sylancl 668 . . . 4
165 resixp 7557 . . . . . 6
16626, 51, 165sylancr 669 . . . . 5
167 ne0i 3737 . . . . 5
168166, 167syl 17 . . . 4
169 ixpiunwdom 8106 . . . 4 *
170159, 164, 168, 169syl3anc 1268 . . 3 *
171 numwdom 8490 . . 3 *
172156, 170, 171syl2anc 667 . 2
17315, 172exlimddv 1781 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 188   wa 371   wceq 1444  wex 1663   wcel 1887  cab 2437   wne 2622  wral 2737  wrex 2738  crab 2741  cvv 3045   cdif 3401   cin 3403   wss 3404  c0 3731  cif 3881  cpw 3951  csn 3968  cuni 4198  ciun 4278   class class class wbr 4402   cmpt 4461   cxp 4832  ccnv 4833   cdm 4834   crn 4835   cres 4836  cima 4837   wfn 5577  wf 5578  wfo 5580  cfv 5582   cmpt2 6292  c1o 7175  cixp 7522   cen 7566  cfn 7569   * cwdom 8072  ccrd 8369  ccmp 20401  UFLcufl 20915 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-rep 4515  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-reu 2744  df-rmo 2745  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-pss 3420  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-int 4235  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-tr 4498  df-eprel 4745  df-id 4749  df-po 4755  df-so 4756  df-fr 4793  df-se 4794  df-we 4795  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-pred 5380  df-ord 5426  df-on 5427  df-lim 5428  df-suc 5429  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-isom 5591  df-riota 6252  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-om 6693  df-1st 6793  df-2nd 6794  df-wrecs 7028  df-recs 7090  df-rdg 7128  df-1o 7182  df-oadd 7186  df-omul 7187  df-er 7363  df-map 7474  df-ixp 7523  df-en 7570  df-dom 7571  df-fin 7573  df-wdom 8074  df-card 8373  df-acn 8376 This theorem is referenced by:  ptcmplem3  21069
 Copyright terms: Public domain W3C validator