Metamath Proof Explorer

Theorem maxsta

Description: An axiom is a statement. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses maxsta.a 
|- A = ( mAx ` T )
maxsta.s 
|- S = ( mStat ` T )
Assertion maxsta 
|- ( T e. mFS -> A C_ S )

Proof

Step Hyp Ref Expression
1 maxsta.a 
 |-  A = ( mAx ` T )
2 maxsta.s 
 |-  S = ( mStat ` T )
3 eqid 
 |-  ( mCN ` T ) = ( mCN ` T )
4 eqid 
 |-  ( mVR ` T ) = ( mVR ` T )
5 eqid 
 |-  ( mType ` T ) = ( mType ` T )
6 eqid 
 |-  ( mVT ` T ) = ( mVT ` T )
7 eqid 
 |-  ( mTC ` T ) = ( mTC ` T )
8 3 4 5 6 7 1 2 ismfs 
 |-  ( T e. mFS -> ( T e. mFS <-> ( ( ( ( mCN ` T ) i^i ( mVR ` T ) ) = (/) /\ ( mType ` T ) : ( mVR ` T ) --> ( mTC ` T ) ) /\ ( A C_ S /\ A. v e. ( mVT ` T ) -. ( `' ( mType ` T ) " { v } ) e. Fin ) ) ) )
9 8 ibi 
 |-  ( T e. mFS -> ( ( ( ( mCN ` T ) i^i ( mVR ` T ) ) = (/) /\ ( mType ` T ) : ( mVR ` T ) --> ( mTC ` T ) ) /\ ( A C_ S /\ A. v e. ( mVT ` T ) -. ( `' ( mType ` T ) " { v } ) e. Fin ) ) )
10 9 simprld 
 |-  ( T e. mFS -> A C_ S )