Metamath Proof Explorer

Theorem mppsval

Description: Definition of a provable pre-statement, essentially just a reorganization of the arguments of df-mcls . (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mppsval.p 
|- P = ( mPreSt ` T )
mppsval.j 
|- J = ( mPPSt ` T )
mppsval.c 
|- C = ( mCls ` T )
Assertion mppsval 
|- J = { <. <. d , h >. , a >. | ( <. d , h , a >. e. P /\ a e. ( d C h ) ) }

Proof

Step Hyp Ref Expression
1 mppsval.p 
 |-  P = ( mPreSt ` T )
2 mppsval.j 
 |-  J = ( mPPSt ` T )
3 mppsval.c 
 |-  C = ( mCls ` T )
4 fveq2 
 |-  ( t = T -> ( mPreSt ` t ) = ( mPreSt ` T ) )
5 4 1 eqtr4di 
 |-  ( t = T -> ( mPreSt ` t ) = P )
6 5 eleq2d 
 |-  ( t = T -> ( <. d , h , a >. e. ( mPreSt ` t ) <-> <. d , h , a >. e. P ) )
7 fveq2 
 |-  ( t = T -> ( mCls ` t ) = ( mCls ` T ) )
8 7 3 eqtr4di 
 |-  ( t = T -> ( mCls ` t ) = C )
9 8 oveqd 
 |-  ( t = T -> ( d ( mCls ` t ) h ) = ( d C h ) )
10 9 eleq2d 
 |-  ( t = T -> ( a e. ( d ( mCls ` t ) h ) <-> a e. ( d C h ) ) )
11 6 10 anbi12d 
 |-  ( t = T -> ( ( <. d , h , a >. e. ( mPreSt ` t ) /\ a e. ( d ( mCls ` t ) h ) ) <-> ( <. d , h , a >. e. P /\ a e. ( d C h ) ) ) )
12 11 oprabbidv 
 |-  ( t = T -> { <. <. d , h >. , a >. | ( <. d , h , a >. e. ( mPreSt ` t ) /\ a e. ( d ( mCls ` t ) h ) ) } = { <. <. d , h >. , a >. | ( <. d , h , a >. e. P /\ a e. ( d C h ) ) } )
13 df-mpps 
 |-  mPPSt = ( t e. _V |-> { <. <. d , h >. , a >. | ( <. d , h , a >. e. ( mPreSt ` t ) /\ a e. ( d ( mCls ` t ) h ) ) } )
14 1 fvexi 
 |-  P e. _V
15 1 2 3 mppspstlem 
 |-  { <. <. d , h >. , a >. | ( <. d , h , a >. e. P /\ a e. ( d C h ) ) } C_ P
16 14 15 ssexi 
 |-  { <. <. d , h >. , a >. | ( <. d , h , a >. e. P /\ a e. ( d C h ) ) } e. _V
17 12 13 16 fvmpt 
 |-  ( T e. _V -> ( mPPSt ` T ) = { <. <. d , h >. , a >. | ( <. d , h , a >. e. P /\ a e. ( d C h ) ) } )
18 fvprc 
 |-  ( -. T e. _V -> ( mPPSt ` T ) = (/) )
19 df-oprab 
 |-  { <. <. 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 ) ) ) }
20 abn0 
 |-  ( { x | E. d E. h E. a ( x = <. <. d , h >. , a >. /\ ( <. d , h , a >. e. P /\ a e. ( d C h ) ) ) } =/= (/) <-> E. x E. d E. h E. a ( x = <. <. d , h >. , a >. /\ ( <. d , h , a >. e. P /\ a e. ( d C h ) ) ) )
21 elfvex 
 |-  ( <. d , h , a >. e. ( mPreSt ` T ) -> T e. _V )
22 21 1 eleq2s 
 |-  ( <. d , h , a >. e. P -> T e. _V )
23 22 ad2antrl 
 |-  ( ( x = <. <. d , h >. , a >. /\ ( <. d , h , a >. e. P /\ a e. ( d C h ) ) ) -> T e. _V )
24 23 exlimivv 
 |-  ( E. h E. a ( x = <. <. d , h >. , a >. /\ ( <. d , h , a >. e. P /\ a e. ( d C h ) ) ) -> T e. _V )
25 24 exlimivv 
 |-  ( E. x E. d E. h E. a ( x = <. <. d , h >. , a >. /\ ( <. d , h , a >. e. P /\ a e. ( d C h ) ) ) -> T e. _V )
26 20 25 sylbi 
 |-  ( { x | E. d E. h E. a ( x = <. <. d , h >. , a >. /\ ( <. d , h , a >. e. P /\ a e. ( d C h ) ) ) } =/= (/) -> T e. _V )
27 26 necon1bi 
 |-  ( -. T e. _V -> { x | E. d E. h E. a ( x = <. <. d , h >. , a >. /\ ( <. d , h , a >. e. P /\ a e. ( d C h ) ) ) } = (/) )
28 19 27 syl5eq 
 |-  ( -. T e. _V -> { <. <. d , h >. , a >. | ( <. d , h , a >. e. P /\ a e. ( d C h ) ) } = (/) )
29 18 28 eqtr4d 
 |-  ( -. T e. _V -> ( mPPSt ` T ) = { <. <. d , h >. , a >. | ( <. d , h , a >. e. P /\ a e. ( d C h ) ) } )
30 17 29 pm2.61i 
 |-  ( mPPSt ` T ) = { <. <. d , h >. , a >. | ( <. d , h , a >. e. P /\ a e. ( d C h ) ) }
31 2 30 eqtri 
 |-  J = { <. <. d , h >. , a >. | ( <. d , h , a >. e. P /\ a e. ( d C h ) ) }