Metamath Proof Explorer

Theorem elmpps

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 elmpps 
|- ( <. D , H , A >. e. J <-> ( <. 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 df-ot 
 |-  <. D , H , A >. = <. <. D , H >. , A >.
5 1 2 3 mppsval 
 |-  J = { <. <. d , h >. , a >. | ( <. d , h , a >. e. P /\ a e. ( d C h ) ) }
6 4 5 eleq12i 
 |-  ( <. D , H , A >. e. J <-> <. <. D , H >. , A >. e. { <. <. d , h >. , a >. | ( <. d , h , a >. e. P /\ a e. ( d C h ) ) } )
7 oprabss 
 |-  { <. <. d , h >. , a >. | ( <. d , h , a >. e. P /\ a e. ( d C h ) ) } C_ ( ( _V X. _V ) X. _V )
8 7 sseli 
 |-  ( <. <. D , H >. , A >. e. { <. <. d , h >. , a >. | ( <. d , h , a >. e. P /\ a e. ( d C h ) ) } -> <. <. D , H >. , A >. e. ( ( _V X. _V ) X. _V ) )
9 1 mpstssv 
 |-  P C_ ( ( _V X. _V ) X. _V )
10 9 sseli 
 |-  ( <. D , H , A >. e. P -> <. D , H , A >. e. ( ( _V X. _V ) X. _V ) )
11 4 10 eqeltrrid 
 |-  ( <. D , H , A >. e. P -> <. <. D , H >. , A >. e. ( ( _V X. _V ) X. _V ) )
12 11 adantr 
 |-  ( ( <. D , H , A >. e. P /\ A e. ( D C H ) ) -> <. <. D , H >. , A >. e. ( ( _V X. _V ) X. _V ) )
13 opelxp 
 |-  ( <. <. D , H >. , A >. e. ( ( _V X. _V ) X. _V ) <-> ( <. D , H >. e. ( _V X. _V ) /\ A e. _V ) )
14 opelxp 
 |-  ( <. D , H >. e. ( _V X. _V ) <-> ( D e. _V /\ H e. _V ) )
15 simp1 
 |-  ( ( d = D /\ h = H /\ a = A ) -> d = D )
16 simp2 
 |-  ( ( d = D /\ h = H /\ a = A ) -> h = H )
17 simp3 
 |-  ( ( d = D /\ h = H /\ a = A ) -> a = A )
18 15 16 17 oteq123d 
 |-  ( ( d = D /\ h = H /\ a = A ) -> <. d , h , a >. = <. D , H , A >. )
19 18 eleq1d 
 |-  ( ( d = D /\ h = H /\ a = A ) -> ( <. d , h , a >. e. P <-> <. D , H , A >. e. P ) )
20 15 16 oveq12d 
 |-  ( ( d = D /\ h = H /\ a = A ) -> ( d C h ) = ( D C H ) )
21 17 20 eleq12d 
 |-  ( ( d = D /\ h = H /\ a = A ) -> ( a e. ( d C h ) <-> A e. ( D C H ) ) )
22 19 21 anbi12d 
 |-  ( ( d = D /\ h = H /\ a = A ) -> ( ( <. d , h , a >. e. P /\ a e. ( d C h ) ) <-> ( <. D , H , A >. e. P /\ A e. ( D C H ) ) ) )
23 22 eloprabga 
 |-  ( ( D e. _V /\ H e. _V /\ A e. _V ) -> ( <. <. D , H >. , A >. e. { <. <. d , h >. , a >. | ( <. d , h , a >. e. P /\ a e. ( d C h ) ) } <-> ( <. D , H , A >. e. P /\ A e. ( D C H ) ) ) )
24 23 3expa 
 |-  ( ( ( D e. _V /\ H e. _V ) /\ A e. _V ) -> ( <. <. D , H >. , A >. e. { <. <. d , h >. , a >. | ( <. d , h , a >. e. P /\ a e. ( d C h ) ) } <-> ( <. D , H , A >. e. P /\ A e. ( D C H ) ) ) )
25 14 24 sylanb 
 |-  ( ( <. D , H >. e. ( _V X. _V ) /\ A e. _V ) -> ( <. <. D , H >. , A >. e. { <. <. d , h >. , a >. | ( <. d , h , a >. e. P /\ a e. ( d C h ) ) } <-> ( <. D , H , A >. e. P /\ A e. ( D C H ) ) ) )
26 13 25 sylbi 
 |-  ( <. <. D , H >. , A >. e. ( ( _V X. _V ) X. _V ) -> ( <. <. D , H >. , A >. e. { <. <. d , h >. , a >. | ( <. d , h , a >. e. P /\ a e. ( d C h ) ) } <-> ( <. D , H , A >. e. P /\ A e. ( D C H ) ) ) )
27 8 12 26 pm5.21nii 
 |-  ( <. <. D , H >. , A >. e. { <. <. d , h >. , a >. | ( <. d , h , a >. e. P /\ a e. ( d C h ) ) } <-> ( <. D , H , A >. e. P /\ A e. ( D C H ) ) )
28 6 27 bitri 
 |-  ( <. D , H , A >. e. J <-> ( <. D , H , A >. e. P /\ A e. ( D C H ) ) )