Theorem elmsta

Description: Property of being a statement. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mstapst.p	|- P = ( mPreSt ` T )
	mstapst.s	|- S = ( mStat ` T )
	elmsta.v	|- V = ( mVars ` T )
	elmsta.z	|- Z = U. ( V " ( H u. { A } ) )
Assertion	elmsta	|- ( <. D , H , A >. e. S <-> ( <. D , H , A >. e. P /\ D C_ ( Z X. Z ) ) )

Proof

Step	Hyp	Ref	Expression
1		mstapst.p	|- P = ( mPreSt ` T )
2		mstapst.s	|- S = ( mStat ` T )
3		elmsta.v	|- V = ( mVars ` T )
4		elmsta.z	|- Z = U. ( V " ( H u. { A } ) )
5	1 2	mstapst	|- S C_ P
6	5	sseli	|- ( <. D , H , A >. e. S -> <. D , H , A >. e. P )
7		eqid	|- ( mStRed ` T ) = ( mStRed ` T )
8	3 1 7 4	msrval	|- ( <. D , H , A >. e. P -> ( ( mStRed ` T ) ` <. D , H , A >. ) = <. ( D i^i ( Z X. Z ) ) , H , A >. )
9	6 8	syl	|- ( <. D , H , A >. e. S -> ( ( mStRed ` T ) ` <. D , H , A >. ) = <. ( D i^i ( Z X. Z ) ) , H , A >. )
10	7 2	msrid	|- ( <. D , H , A >. e. S -> ( ( mStRed ` T ) ` <. D , H , A >. ) = <. D , H , A >. )
11	9 10	eqtr3d	|- ( <. D , H , A >. e. S -> <. ( D i^i ( Z X. Z ) ) , H , A >. = <. D , H , A >. )
12	11	fveq2d	|- ( <. D , H , A >. e. S -> ( 1st ` <. ( D i^i ( Z X. Z ) ) , H , A >. ) = ( 1st ` <. D , H , A >. ) )
13	12	fveq2d	|- ( <. D , H , A >. e. S -> ( 1st ` ( 1st ` <. ( D i^i ( Z X. Z ) ) , H , A >. ) ) = ( 1st ` ( 1st ` <. D , H , A >. ) ) )
14		inss1	|- ( D i^i ( Z X. Z ) ) C_ D
15	1	mpstrcl	|- ( <. D , H , A >. e. P -> ( D e. _V /\ H e. _V /\ A e. _V ) )
16	6 15	syl	|- ( <. D , H , A >. e. S -> ( D e. _V /\ H e. _V /\ A e. _V ) )
17	16	simp1d	|- ( <. D , H , A >. e. S -> D e. _V )
18		ssexg	|- ( ( ( D i^i ( Z X. Z ) ) C_ D /\ D e. _V ) -> ( D i^i ( Z X. Z ) ) e. _V )
19	14 17 18	sylancr	|- ( <. D , H , A >. e. S -> ( D i^i ( Z X. Z ) ) e. _V )
20	16	simp2d	|- ( <. D , H , A >. e. S -> H e. _V )
21	16	simp3d	|- ( <. D , H , A >. e. S -> A e. _V )
22		ot1stg	|- ( ( ( D i^i ( Z X. Z ) ) e. _V /\ H e. _V /\ A e. _V ) -> ( 1st ` ( 1st ` <. ( D i^i ( Z X. Z ) ) , H , A >. ) ) = ( D i^i ( Z X. Z ) ) )
23	19 20 21 22	syl3anc	|- ( <. D , H , A >. e. S -> ( 1st ` ( 1st ` <. ( D i^i ( Z X. Z ) ) , H , A >. ) ) = ( D i^i ( Z X. Z ) ) )
24		ot1stg	|- ( ( D e. _V /\ H e. _V /\ A e. _V ) -> ( 1st ` ( 1st ` <. D , H , A >. ) ) = D )
25	16 24	syl	|- ( <. D , H , A >. e. S -> ( 1st ` ( 1st ` <. D , H , A >. ) ) = D )
26	13 23 25	3eqtr3d	|- ( <. D , H , A >. e. S -> ( D i^i ( Z X. Z ) ) = D )
27		inss2	|- ( D i^i ( Z X. Z ) ) C_ ( Z X. Z )
28	26 27	eqsstrrdi	|- ( <. D , H , A >. e. S -> D C_ ( Z X. Z ) )
29	6 28	jca	|- ( <. D , H , A >. e. S -> ( <. D , H , A >. e. P /\ D C_ ( Z X. Z ) ) )
30	8	adantr	|- ( ( <. D , H , A >. e. P /\ D C_ ( Z X. Z ) ) -> ( ( mStRed ` T ) ` <. D , H , A >. ) = <. ( D i^i ( Z X. Z ) ) , H , A >. )
31		simpr	|- ( ( <. D , H , A >. e. P /\ D C_ ( Z X. Z ) ) -> D C_ ( Z X. Z ) )
32		df-ss	|- ( D C_ ( Z X. Z ) <-> ( D i^i ( Z X. Z ) ) = D )
33	31 32	sylib	|- ( ( <. D , H , A >. e. P /\ D C_ ( Z X. Z ) ) -> ( D i^i ( Z X. Z ) ) = D )
34	33	oteq1d	|- ( ( <. D , H , A >. e. P /\ D C_ ( Z X. Z ) ) -> <. ( D i^i ( Z X. Z ) ) , H , A >. = <. D , H , A >. )
35	30 34	eqtrd	|- ( ( <. D , H , A >. e. P /\ D C_ ( Z X. Z ) ) -> ( ( mStRed ` T ) ` <. D , H , A >. ) = <. D , H , A >. )
36	1 7	msrf	|- ( mStRed ` T ) : P --> P
37		ffn	|- ( ( mStRed ` T ) : P --> P -> ( mStRed ` T ) Fn P )
38	36 37	ax-mp	|- ( mStRed ` T ) Fn P
39		simpl	|- ( ( <. D , H , A >. e. P /\ D C_ ( Z X. Z ) ) -> <. D , H , A >. e. P )
40		fnfvelrn	|- ( ( ( mStRed ` T ) Fn P /\ <. D , H , A >. e. P ) -> ( ( mStRed ` T ) ` <. D , H , A >. ) e. ran ( mStRed ` T ) )
41	38 39 40	sylancr	|- ( ( <. D , H , A >. e. P /\ D C_ ( Z X. Z ) ) -> ( ( mStRed ` T ) ` <. D , H , A >. ) e. ran ( mStRed ` T ) )
42	35 41	eqeltrrd	|- ( ( <. D , H , A >. e. P /\ D C_ ( Z X. Z ) ) -> <. D , H , A >. e. ran ( mStRed ` T ) )
43	7 2	mstaval	|- S = ran ( mStRed ` T )
44	42 43	eleqtrrdi	|- ( ( <. D , H , A >. e. P /\ D C_ ( Z X. Z ) ) -> <. D , H , A >. e. S )
45	29 44	impbii	|- ( <. D , H , A >. e. S <-> ( <. D , H , A >. e. P /\ D C_ ( Z X. Z ) ) )