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

Theorem infxpenc2lem2OLD 8353
 Description: Lemma for infxpenc2OLD 8355. (Contributed by Mario Carneiro, 30-May-2015.) Obsolete version of infxpenc2lem2 8349 as of 7-Jul-2019. (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
infxpenc2OLD.1
infxpenc2OLD.2
infxpenc2OLD.3
infxpenc2OLD.4
infxpenc2OLD.5
infxpenc2OLD.k
infxpenc2OLD.h CNF CNF
infxpenc2OLD.l
infxpenc2OLD.x
infxpenc2OLD.y
infxpenc2OLD.j CNF CNF
infxpenc2OLD.z
infxpenc2OLD.t
infxpenc2OLD.g
Assertion
Ref Expression
infxpenc2lem2OLD
Distinct variable groups:   ,,,,,,   ,,,,   ,,,,,   ,,,   ,   ,,   ,,
Allowed substitution hints:   (,,)   ()   (,,,,,,)   (,,,)   (,,,,,)   (,,,,,,)   (,,,,,,)   (,,,,,,)   (,,,,,,)   (,)   (,,,,)   (,,,,)   (,,,,,,)

Proof of Theorem infxpenc2lem2OLD
StepHypRef Expression
1 infxpenc2OLD.1 . . 3
2 mptexg 6079 . . 3
31, 2syl 17 . 2
41adantr 463 . . . . . . 7
5 simprl 756 . . . . . . 7
6 onelon 4846 . . . . . . 7
74, 5, 6syl2anc 659 . . . . . 6
8 simprr 758 . . . . . 6
9 infxpenc2OLD.2 . . . . . . . 8
10 infxpenc2OLD.3 . . . . . . . 8
111, 9, 10infxpenc2lem1 8348 . . . . . . 7
1211simpld 457 . . . . . 6
13 infxpenc2OLD.4 . . . . . . 7
1413adantr 463 . . . . . 6
15 infxpenc2OLD.5 . . . . . . 7
1615adantr 463 . . . . . 6
1711simprd 461 . . . . . 6
18 infxpenc2OLD.k . . . . . 6
19 infxpenc2OLD.h . . . . . 6 CNF CNF
20 infxpenc2OLD.l . . . . . 6
21 infxpenc2OLD.x . . . . . 6
22 infxpenc2OLD.y . . . . . 6
23 infxpenc2OLD.j . . . . . 6 CNF CNF
24 infxpenc2OLD.z . . . . . 6
25 infxpenc2OLD.t . . . . . 6
26 infxpenc2OLD.g . . . . . 6
277, 8, 12, 14, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26infxpencOLD 8352 . . . . 5
28 f1of 5755 . . . . . . . . 9
2927, 28syl 17 . . . . . . . 8
30 vex 3061 . . . . . . . . 9
3130, 30xpex 6542 . . . . . . . 8
32 fex 6082 . . . . . . . 8
3329, 31, 32sylancl 660 . . . . . . 7
34 eqid 2402 . . . . . . . 8
3534fvmpt2 5897 . . . . . . 7
365, 33, 35syl2anc 659 . . . . . 6
37 f1oeq1 5746 . . . . . 6
3836, 37syl 17 . . . . 5
3927, 38mpbird 232 . . . 4
4039expr 613 . . 3
4140ralrimiva 2817 . 2
42 nfmpt1 4483 . . . . 5
4342nfeq2 2581 . . . 4
44 fveq1 5804 . . . . . 6
45 f1oeq1 5746 . . . . . 6
4644, 45syl 17 . . . . 5
4746imbi2d 314 . . . 4
4843, 47ralbid 2837 . . 3
4948spcegv 3144 . 2
503, 41, 49sylc 59 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 367   wceq 1405  wex 1633   wcel 1842  wral 2753  wrex 2754  crab 2757  cvv 3058   cdif 3410   wss 3413  c0 3737  cop 3977   cmpt 4452   cid 4732  con0 4821   cxp 4940  ccnv 4941   crn 4943   cres 4944  cima 4945   ccom 4946  wf 5521  wf1o 5524  cfv 5525  (class class class)co 6234   cmpt2 6236  com 6638  c1o 7080  c2o 7081   coa 7084   comu 7085   coe 7086   cmap 7377  cfn 7474   CNF ccnf 8030 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4506  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629  ax-un 6530  ax-inf2 8011 This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-fal 1411  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-reu 2760  df-rmo 2761  df-rab 2762  df-v 3060  df-sbc 3277  df-csb 3373  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-pss 3429  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-tp 3976  df-op 3978  df-uni 4191  df-int 4227  df-iun 4272  df-br 4395  df-opab 4453  df-mpt 4454  df-tr 4489  df-eprel 4733  df-id 4737  df-po 4743  df-so 4744  df-fr 4781  df-se 4782  df-we 4783  df-ord 4824  df-on 4825  df-lim 4826  df-suc 4827  df-xp 4948  df-rel 4949  df-cnv 4950  df-co 4951  df-dm 4952  df-rn 4953  df-res 4954  df-ima 4955  df-iota 5489  df-fun 5527  df-fn 5528  df-f 5529  df-f1 5530  df-fo 5531  df-f1o 5532  df-fv 5533  df-isom 5534  df-riota 6196  df-ov 6237  df-oprab 6238  df-mpt2 6239  df-om 6639  df-1st 6738  df-2nd 6739  df-supp 6857  df-recs 6999  df-rdg 7033  df-seqom 7070  df-1o 7087  df-2o 7088  df-oadd 7091  df-omul 7092  df-oexp 7093  df-er 7268  df-map 7379  df-en 7475  df-dom 7476  df-sdom 7477  df-fin 7478  df-fsupp 7784  df-oi 7889  df-cnf 8031 This theorem is referenced by:  infxpenc2lem3OLD  8354
 Copyright terms: Public domain W3C validator