Theorem pmtrfmvdn0

Description: A transposition moves at least one point. (Contributed by Stefan O'Rear, 23-Aug-2015)

	Ref	Expression
Hypotheses	pmtrrn.t	$$⊢T=\mathrm{pmTrsp}\left(D\right)$$
	pmtrrn.r	$$⊢R=\mathrm{ran}T$$
Assertion	pmtrfmvdn0	$$⊢F\in R\to \mathrm{dom}\left(F\setminus \mathrm{I}\right)\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		pmtrrn.t	$$⊢T=\mathrm{pmTrsp}\left(D\right)$$
2		pmtrrn.r	$$⊢R=\mathrm{ran}T$$
3		2on0	$$⊢2_{𝑜}\ne \varnothing$$
4		eqid	$$⊢\mathrm{dom}\left(F\setminus \mathrm{I}\right)=\mathrm{dom}\left(F\setminus \mathrm{I}\right)$$
5	1 2 4	pmtrfrn	$$⊢F\in R\to \left(\left(D\in \mathrm{V}\wedge \mathrm{dom}\left(F\setminus \mathrm{I}\right)\subseteq D\wedge \mathrm{dom}\left(F\setminus \mathrm{I}\right)\approx 2_{𝑜}\right)\wedge F=T\left(\mathrm{dom}\left(F\setminus \mathrm{I}\right)\right)\right)$$
6	5	simpld	$$⊢F\in R\to \left(D\in \mathrm{V}\wedge \mathrm{dom}\left(F\setminus \mathrm{I}\right)\subseteq D\wedge \mathrm{dom}\left(F\setminus \mathrm{I}\right)\approx 2_{𝑜}\right)$$
7	6	simp3d	$$⊢F\in R\to \mathrm{dom}\left(F\setminus \mathrm{I}\right)\approx 2_{𝑜}$$
8		enen1	$$⊢\mathrm{dom}\left(F\setminus \mathrm{I}\right)\approx 2_{𝑜}\to \left(\mathrm{dom}\left(F\setminus \mathrm{I}\right)\approx \varnothing \leftrightarrow 2_{𝑜}\approx \varnothing \right)$$
9	7 8	syl	$$⊢F\in R\to \left(\mathrm{dom}\left(F\setminus \mathrm{I}\right)\approx \varnothing \leftrightarrow 2_{𝑜}\approx \varnothing \right)$$
10		en0	$$⊢\mathrm{dom}\left(F\setminus \mathrm{I}\right)\approx \varnothing \leftrightarrow \mathrm{dom}\left(F\setminus \mathrm{I}\right)=\varnothing$$
11		en0	$$⊢2_{𝑜}\approx \varnothing \leftrightarrow 2_{𝑜}=\varnothing$$
12	9 10 11	3bitr3g	$$⊢F\in R\to \left(\mathrm{dom}\left(F\setminus \mathrm{I}\right)=\varnothing \leftrightarrow 2_{𝑜}=\varnothing \right)$$
13	12	necon3bid	$$⊢F\in R\to \left(\mathrm{dom}\left(F\setminus \mathrm{I}\right)\ne \varnothing \leftrightarrow 2_{𝑜}\ne \varnothing \right)$$
14	3 13	mpbiri	$$⊢F\in R\to \mathrm{dom}\left(F\setminus \mathrm{I}\right)\ne \varnothing$$