Theorem mpstrcl

Description: The elements of a pre-statement are sets. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypothesis	mpstssv.p	|- P = ( mPreSt ` T )
Assertion	mpstrcl	|- ( <. D , H , A >. e. P -> ( D e. _V /\ H e. _V /\ A e. _V ) )

Proof

Step	Hyp	Ref	Expression
1		mpstssv.p	|- P = ( mPreSt ` T )
2		df-ot	|- <. D , H , A >. = <. <. D , H >. , A >.
3	1	mpstssv	|- P C_ ( ( _V X. _V ) X. _V )
4	3	sseli	|- ( <. D , H , A >. e. P -> <. D , H , A >. e. ( ( _V X. _V ) X. _V ) )
5	2 4	eqeltrrid	|- ( <. D , H , A >. e. P -> <. <. D , H >. , A >. e. ( ( _V X. _V ) X. _V ) )
6		opelxp	|- ( <. D , H >. e. ( _V X. _V ) <-> ( D e. _V /\ H e. _V ) )
7	6	anbi1i	|- ( ( <. D , H >. e. ( _V X. _V ) /\ A e. _V ) <-> ( ( D e. _V /\ H e. _V ) /\ A e. _V ) )
8		opelxp	|- ( <. <. D , H >. , A >. e. ( ( _V X. _V ) X. _V ) <-> ( <. D , H >. e. ( _V X. _V ) /\ A e. _V ) )
9		df-3an	|- ( ( D e. _V /\ H e. _V /\ A e. _V ) <-> ( ( D e. _V /\ H e. _V ) /\ A e. _V ) )
10	7 8 9	3bitr4i	|- ( <. <. D , H >. , A >. e. ( ( _V X. _V ) X. _V ) <-> ( D e. _V /\ H e. _V /\ A e. _V ) )
11	5 10	sylib	|- ( <. D , H , A >. e. P -> ( D e. _V /\ H e. _V /\ A e. _V ) )