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 → 𝐴 ⊆ 𝑆 )