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

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

Proof of Theorem ptcmplem5
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 inss1 3620 . . 3 UFL UFL
2 ptcmp.5 . . 3 UFL
31, 2sseldi 3400 . 2 UFL
4 ptcmp.1 . . . 4
5 ptcmp.2 . . . 4
6 ptcmp.3 . . . 4
7 ptcmp.4 . . . 4
84, 5, 6, 7, 2ptcmplem1 21004 . . 3
98simpld 460 . 2
108simprd 464 . 2
11 elpwi 3928 . . . . . 6
126ad2antrr 730 . . . . . . . . 9
137ad2antrr 730 . . . . . . . . 9
142ad2antrr 730 . . . . . . . . 9 UFL
15 simplrl 768 . . . . . . . . 9
16 simplrr 769 . . . . . . . . 9
17 simpr 462 . . . . . . . . 9
18 imaeq2 5121 . . . . . . . . . . 11
1918eleq1d 2485 . . . . . . . . . 10
2019cbvrabv 3016 . . . . . . . . 9
214, 5, 12, 13, 14, 15, 16, 17, 20ptcmplem4 21007 . . . . . . . 8
22 iman 425 . . . . . . . 8
2321, 22mpbir 212 . . . . . . 7
2423expr 618 . . . . . 6
2511, 24sylan2 476 . . . . 5
2625adantlr 719 . . . 4
27 selpw 3926 . . . . . . 7
28 eldif 3384 . . . . . . . 8
29 elpwunsn 3978 . . . . . . . 8
3028, 29sylbir 216 . . . . . . 7
3127, 30sylanbr 475 . . . . . 6
3231adantll 718 . . . . 5
33 snssi 4082 . . . . . . . . 9
3433adantl 467 . . . . . . . 8
35 snfi 7599 . . . . . . . . 9
3635a1i 11 . . . . . . . 8
37 elfpw 7824 . . . . . . . 8
3834, 36, 37sylanbrc 668 . . . . . . 7
39 unisng 4173 . . . . . . . . 9
4039eqcomd 2429 . . . . . . . 8
4140adantl 467 . . . . . . 7
42 unieq 4165 . . . . . . . . 9
4342eqeq2d 2433 . . . . . . . 8
4443rspcev 3120 . . . . . . 7
4538, 41, 44syl2anc 665 . . . . . 6
4645a1d 26 . . . . 5
4732, 46syldan 472 . . . 4
4826, 47pm2.61dan 798 . . 3
4948impr 623 . 2
503, 9, 10, 49alexsub 20997 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wa 370   wceq 1437   wcel 1872  wrex 2710  crab 2713   cdif 3371   cun 3372   cin 3373   wss 3374  cpw 3919  csn 3936  cuni 4157   cmpt 4420  ccnv 4790   cdm 4791   crn 4792  cima 4794  wf 5535  cfv 5539   cmpt2 6246  cixp 7472  cfn 7519  cfi 7872  ccrd 8316  ctg 15274  cpt 15275  ccmp 20338  UFLcufl 20852 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-rep 4474  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-nel 2597  df-ral 2714  df-rex 2715  df-reu 2716  df-rmo 2717  df-rab 2718  df-v 3019  df-sbc 3238  df-csb 3334  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-pss 3390  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4158  df-int 4194  df-iun 4239  df-iin 4240  df-br 4362  df-opab 4421  df-mpt 4422  df-tr 4457  df-eprel 4702  df-id 4706  df-po 4712  df-so 4713  df-fr 4750  df-se 4751  df-we 4752  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-pred 5337  df-ord 5383  df-on 5384  df-lim 5385  df-suc 5386  df-iota 5503  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-fv 5547  df-isom 5548  df-riota 6206  df-ov 6247  df-oprab 6248  df-mpt2 6249  df-om 6646  df-1st 6746  df-2nd 6747  df-wrecs 6978  df-recs 7040  df-rdg 7078  df-1o 7132  df-2o 7133  df-oadd 7136  df-omul 7137  df-er 7313  df-map 7424  df-ixp 7473  df-en 7520  df-dom 7521  df-sdom 7522  df-fin 7523  df-fi 7873  df-wdom 8022  df-card 8320  df-acn 8323  df-topgen 15280  df-pt 15281  df-fbas 18905  df-fg 18906  df-top 19858  df-bases 19859  df-topon 19860  df-cld 19971  df-ntr 19972  df-cls 19973  df-nei 20051  df-cmp 20339  df-fil 20798  df-ufil 20853  df-ufl 20854  df-flim 20891  df-fcls 20893 This theorem is referenced by:  ptcmpg  21009
 Copyright terms: Public domain W3C validator