Theorem mfsdisj

Description: The constants and variables of a formal system are disjoint. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mfsdisj.c	$$⊢C=\mathrm{mCN}\left(T\right)$$
	mfsdisj.v	$$⊢V=\mathrm{mVR}\left(T\right)$$
Assertion	mfsdisj	$$⊢T\in \mathrm{mFS}\to C\cap V=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		mfsdisj.c	$$⊢C=\mathrm{mCN}\left(T\right)$$
2		mfsdisj.v	$$⊢V=\mathrm{mVR}\left(T\right)$$
3		eqid	$$⊢\mathrm{mType}\left(T\right)=\mathrm{mType}\left(T\right)$$
4		eqid	$$⊢\mathrm{mVT}\left(T\right)=\mathrm{mVT}\left(T\right)$$
5		eqid	$$⊢\mathrm{mTC}\left(T\right)=\mathrm{mTC}\left(T\right)$$
6		eqid	$$⊢\mathrm{mAx}\left(T\right)=\mathrm{mAx}\left(T\right)$$
7		eqid	$$⊢\mathrm{mStat}\left(T\right)=\mathrm{mStat}\left(T\right)$$
8	1 2 3 4 5 6 7	ismfs	$$⊢T\in \mathrm{mFS}\to \left(T\in \mathrm{mFS}\leftrightarrow \left(\left(C\cap V=\varnothing \wedge \mathrm{mType}\left(T\right):V⟶\mathrm{mTC}\left(T\right)\right)\wedge \left(\mathrm{mAx}\left(T\right)\subseteq \mathrm{mStat}\left(T\right)\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(C\cap V=\varnothing \wedge \mathrm{mType}\left(T\right):V⟶\mathrm{mTC}\left(T\right)\right)\wedge \left(\mathrm{mAx}\left(T\right)\subseteq \mathrm{mStat}\left(T\right)\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	simplld	$$⊢T\in \mathrm{mFS}\to C\cap V=\varnothing$$