Metamath Proof Explorer


Theorem maxsta

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

Ref Expression
Hypotheses maxsta.a 𝐴 = ( mAx ‘ 𝑇 )
maxsta.s 𝑆 = ( mStat ‘ 𝑇 )
Assertion maxsta ( 𝑇 ∈ mFS → 𝐴𝑆 )

Proof

Step Hyp Ref Expression
1 maxsta.a 𝐴 = ( mAx ‘ 𝑇 )
2 maxsta.s 𝑆 = ( mStat ‘ 𝑇 )
3 eqid ( mCN ‘ 𝑇 ) = ( mCN ‘ 𝑇 )
4 eqid ( mVR ‘ 𝑇 ) = ( mVR ‘ 𝑇 )
5 eqid ( mType ‘ 𝑇 ) = ( mType ‘ 𝑇 )
6 eqid ( mVT ‘ 𝑇 ) = ( mVT ‘ 𝑇 )
7 eqid ( mTC ‘ 𝑇 ) = ( mTC ‘ 𝑇 )
8 3 4 5 6 7 1 2 ismfs ( 𝑇 ∈ mFS → ( 𝑇 ∈ mFS ↔ ( ( ( ( mCN ‘ 𝑇 ) ∩ ( mVR ‘ 𝑇 ) ) = ∅ ∧ ( mType ‘ 𝑇 ) : ( mVR ‘ 𝑇 ) ⟶ ( mTC ‘ 𝑇 ) ) ∧ ( 𝐴𝑆 ∧ ∀ 𝑣 ∈ ( mVT ‘ 𝑇 ) ¬ ( ( mType ‘ 𝑇 ) “ { 𝑣 } ) ∈ Fin ) ) ) )
9 8 ibi ( 𝑇 ∈ mFS → ( ( ( ( mCN ‘ 𝑇 ) ∩ ( mVR ‘ 𝑇 ) ) = ∅ ∧ ( mType ‘ 𝑇 ) : ( mVR ‘ 𝑇 ) ⟶ ( mTC ‘ 𝑇 ) ) ∧ ( 𝐴𝑆 ∧ ∀ 𝑣 ∈ ( mVT ‘ 𝑇 ) ¬ ( ( mType ‘ 𝑇 ) “ { 𝑣 } ) ∈ Fin ) ) )
10 9 simprld ( 𝑇 ∈ mFS → 𝐴𝑆 )