Metamath Proof Explorer

Theorem mpstssv

Description: A pre-statement is an ordered triple. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypothesis mpstssv.p 
|- P = ( mPreSt ` T )
Assertion mpstssv 
|- P C_ ( ( _V X. _V ) X. _V )

Proof

Step Hyp Ref Expression
1 mpstssv.p 
 |-  P = ( mPreSt ` T )
2 eqid 
 |-  ( mDV ` T ) = ( mDV ` T )
3 eqid 
 |-  ( mEx ` T ) = ( mEx ` T )
4 2 3 1 mpstval 
 |-  P = ( ( { d e. ~P ( mDV ` T ) | `' d = d } X. ( ~P ( mEx ` T ) i^i Fin ) ) X. ( mEx ` T ) )
5 xpss 
 |-  ( { d e. ~P ( mDV ` T ) | `' d = d } X. ( ~P ( mEx ` T ) i^i Fin ) ) C_ ( _V X. _V )
6 ssv 
 |-  ( mEx ` T ) C_ _V
7 xpss12 
 |-  ( ( ( { d e. ~P ( mDV ` T ) | `' d = d } X. ( ~P ( mEx ` T ) i^i Fin ) ) C_ ( _V X. _V ) /\ ( mEx ` T ) C_ _V ) -> ( ( { d e. ~P ( mDV ` T ) | `' d = d } X. ( ~P ( mEx ` T ) i^i Fin ) ) X. ( mEx ` T ) ) C_ ( ( _V X. _V ) X. _V ) )
8 5 6 7 mp2an 
 |-  ( ( { d e. ~P ( mDV ` T ) | `' d = d } X. ( ~P ( mEx ` T ) i^i Fin ) ) X. ( mEx ` T ) ) C_ ( ( _V X. _V ) X. _V )
9 4 8 eqsstri 
 |-  P C_ ( ( _V X. _V ) X. _V )