Theorem mvtinf

Description: Each variable typecode has infinitely many variables. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mvtinf.f	$$⊢F=\mathrm{mVT}\left(T\right)$$
	mvtinf.y	$$⊢Y=\mathrm{mType}\left(T\right)$$
Assertion	mvtinf	$$⊢\left(T\in \mathrm{mFS}\wedge X\in F\right)\to \neg Y^{-1}\left[\left\{X\right\}\right]\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		mvtinf.f	$$⊢F=\mathrm{mVT}\left(T\right)$$
2		mvtinf.y	$$⊢Y=\mathrm{mType}\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{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	3 4 2 1 5 6 7	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 Y:\mathrm{mVR}\left(T\right)⟶\mathrm{mTC}\left(T\right)\right)\wedge \left(\mathrm{mAx}\left(T\right)\subseteq \mathrm{mStat}\left(T\right)\wedge \forall v\in F\neg Y^{-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 Y:\mathrm{mVR}\left(T\right)⟶\mathrm{mTC}\left(T\right)\right)\wedge \left(\mathrm{mAx}\left(T\right)\subseteq \mathrm{mStat}\left(T\right)\wedge \forall v\in F\neg Y^{-1}\left[\left\{v\right\}\right]\in \mathrm{Fin}\right)\right)$$
10	9	simprrd	$$⊢T\in \mathrm{mFS}\to \forall v\in F\neg Y^{-1}\left[\left\{v\right\}\right]\in \mathrm{Fin}$$
11		sneq	$$⊢v=X\to \left\{v\right\}=\left\{X\right\}$$
12	11	imaeq2d	$$⊢v=X\to Y^{-1}\left[\left\{v\right\}\right]=Y^{-1}\left[\left\{X\right\}\right]$$
13	12	eleq1d	$$⊢v=X\to \left(Y^{-1}\left[\left\{v\right\}\right]\in \mathrm{Fin}\leftrightarrow Y^{-1}\left[\left\{X\right\}\right]\in \mathrm{Fin}\right)$$
14	13	notbid	$$⊢v=X\to \left(\neg Y^{-1}\left[\left\{v\right\}\right]\in \mathrm{Fin}\leftrightarrow \neg Y^{-1}\left[\left\{X\right\}\right]\in \mathrm{Fin}\right)$$
15	14	rspccva	$$⊢\left(\forall v\in F\neg Y^{-1}\left[\left\{v\right\}\right]\in \mathrm{Fin}\wedge X\in F\right)\to \neg Y^{-1}\left[\left\{X\right\}\right]\in \mathrm{Fin}$$
16	10 15	sylan	$$⊢\left(T\in \mathrm{mFS}\wedge X\in F\right)\to \neg Y^{-1}\left[\left\{X\right\}\right]\in \mathrm{Fin}$$