Theorem maxsta

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

	Ref	Expression
Hypotheses	maxsta.a	$$⊢A=\mathrm{mAx}\left(T\right)$$
	maxsta.s	$$⊢S=\mathrm{mStat}\left(T\right)$$
Assertion	maxsta	$$⊢T\in \mathrm{mFS}\to A\subseteq S$$

Proof

Step	Hyp	Ref	Expression
1		maxsta.a	$$⊢A=\mathrm{mAx}\left(T\right)$$
2		maxsta.s	$$⊢S=\mathrm{mStat}\left(T\right)$$
3		eqid	$$⊢\mathrm{mCN}\left(T\right)=\mathrm{mCN}\left(T\right)$$
4		eqid	$$⊢\mathrm{mVR}\left(T\right)=\mathrm{mVR}\left(T\right)$$
5		eqid	$$⊢\mathrm{mType}\left(T\right)=\mathrm{mType}\left(T\right)$$
6		eqid	$$⊢\mathrm{mVT}\left(T\right)=\mathrm{mVT}\left(T\right)$$
7		eqid	$$⊢\mathrm{mTC}\left(T\right)=\mathrm{mTC}\left(T\right)$$
8	3 4 5 6 7 1 2	ismfs	$$⊢T\in \mathrm{mFS}\to \left(T\in \mathrm{mFS}\leftrightarrow \left(\left(\mathrm{mCN}\left(T\right)\cap \mathrm{mVR}\left(T\right)=\varnothing \wedge \mathrm{mType}\left(T\right):\mathrm{mVR}\left(T\right)⟶\mathrm{mTC}\left(T\right)\right)\wedge \left(A\subseteq S\wedge \forall v\in \mathrm{mVT}\left(T\right)\neg {\mathrm{mType}\left(T\right)}^{-1}\left[\left\{v\right\}\right]\in \mathrm{Fin}\right)\right)\right)$$
9	8	ibi	$$⊢T\in \mathrm{mFS}\to \left(\left(\mathrm{mCN}\left(T\right)\cap \mathrm{mVR}\left(T\right)=\varnothing \wedge \mathrm{mType}\left(T\right):\mathrm{mVR}\left(T\right)⟶\mathrm{mTC}\left(T\right)\right)\wedge \left(A\subseteq S\wedge \forall v\in \mathrm{mVT}\left(T\right)\neg {\mathrm{mType}\left(T\right)}^{-1}\left[\left\{v\right\}\right]\in \mathrm{Fin}\right)\right)$$
10	9	simprld	$$⊢T\in \mathrm{mFS}\to A\subseteq S$$