Users' Mathboxes 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  |-  P  =  (mPreSt `  T )
mppsval.j  |-  J  =  (mPPSt `  T )
mppsval.c  |-  C  =  (mCls `  T )
Assertion
Ref Expression
mppspstlem  |-  { <. <.
d ,  h >. ,  a >.  |  ( <. d ,  h ,  a >.  e.  P  /\  a  e.  (
d C h ) ) }  C_  P
Distinct variable groups:    a, d, h, C    P, a, d, h    T, a, d, h
Allowed substitution hints:    J( h, a, d)

Proof of Theorem mppspstlem
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 df-oprab 6312 . 2  |-  { <. <.
d ,  h >. ,  a >.  |  ( <. d ,  h ,  a >.  e.  P  /\  a  e.  (
d C h ) ) }  =  {
x  |  E. d E. h E. a ( x  =  <. <. d ,  h >. ,  a >.  /\  ( <. d ,  h ,  a >.  e.  P  /\  a  e.  (
d C h ) ) ) }
2 df-ot 3968 . . . . . . . . . 10  |-  <. d ,  h ,  a >.  =  <. <. d ,  h >. ,  a >.
32eqeq2i 2483 . . . . . . . . 9  |-  ( x  =  <. d ,  h ,  a >.  <->  x  =  <. <. d ,  h >. ,  a >. )
43biimpri 211 . . . . . . . 8  |-  ( x  =  <. <. d ,  h >. ,  a >.  ->  x  =  <. d ,  h ,  a >. )
54eleq1d 2533 . . . . . . 7  |-  ( x  =  <. <. d ,  h >. ,  a >.  ->  (
x  e.  P  <->  <. d ,  h ,  a >.  e.  P ) )
65biimpar 493 . . . . . 6  |-  ( ( x  =  <. <. d ,  h >. ,  a >.  /\  <. d ,  h ,  a >.  e.  P
)  ->  x  e.  P )
76adantrr 731 . . . . 5  |-  ( ( x  =  <. <. d ,  h >. ,  a >.  /\  ( <. d ,  h ,  a >.  e.  P  /\  a  e.  (
d C h ) ) )  ->  x  e.  P )
87exlimiv 1784 . . . 4  |-  ( E. a ( x  = 
<. <. d ,  h >. ,  a >.  /\  ( <. d ,  h ,  a >.  e.  P  /\  a  e.  (
d C h ) ) )  ->  x  e.  P )
98exlimivv 1786 . . 3  |-  ( E. d E. h E. a ( x  = 
<. <. d ,  h >. ,  a >.  /\  ( <. d ,  h ,  a >.  e.  P  /\  a  e.  (
d C h ) ) )  ->  x  e.  P )
109abssi 3490 . 2  |-  { x  |  E. d E. h E. a ( x  = 
<. <. d ,  h >. ,  a >.  /\  ( <. d ,  h ,  a >.  e.  P  /\  a  e.  (
d C h ) ) ) }  C_  P
111, 10eqsstri 3448 1  |-  { <. <.
d ,  h >. ,  a >.  |  ( <. d ,  h ,  a >.  e.  P  /\  a  e.  (
d C h ) ) }  C_  P
Colors of variables: wff setvar class
Syntax hints:    /\ wa 376    = wceq 1452   E.wex 1671    e. wcel 1904   {cab 2457    C_ 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