Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mppspstlem Structured version   Visualization version   Unicode version

Theorem mppspstlem 30281
 Description: Lemma for mppspst 30284. (Contributed by Mario Carneiro, 18-Jul-2016.)
Hypotheses
Ref Expression
mppsval.p mPreSt
mppsval.j mPPSt
mppsval.c mCls
Assertion
Ref Expression
mppspstlem
Distinct variable groups:   ,,,   ,,,   ,,,
Allowed substitution hints:   (,,)

Proof of Theorem mppspstlem
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 df-oprab 6312 . 2
2 df-ot 3968 . . . . . . . . . 10
32eqeq2i 2483 . . . . . . . . 9
43biimpri 211 . . . . . . . 8
54eleq1d 2533 . . . . . . 7
65biimpar 493 . . . . . 6
76adantrr 731 . . . . 5
87exlimiv 1784 . . . 4
98exlimivv 1786 . . 3
109abssi 3490 . 2
111, 10eqsstri 3448 1
 Colors of variables: wff setvar class Syntax hints:   wa 376   wceq 1452  wex 1671   wcel 1904  cab 2457   wss 3390  cop 3965  cotp 3967  cfv 5589  (class class class)co 6308  coprab 6309  mPreStcmpst 30183  mClscmcls 30187  mPPStcmpps 30188 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-in 3397  df-ss 3404  df-ot 3968  df-oprab 6312 This theorem is referenced by:  mppsval  30282  mppspst  30284
 Copyright terms: Public domain W3C validator