Theorem pmtrfmvdn0

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

	Ref	Expression
Hypotheses	pmtrrn.t	⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
	pmtrrn.r	⊢ 𝑅 = ran 𝑇
Assertion	pmtrfmvdn0	⊢ ( 𝐹 ∈ 𝑅 → dom ( 𝐹 ∖ I ) ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		pmtrrn.t	⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
2		pmtrrn.r	⊢ 𝑅 = ran 𝑇
3		2on0	⊢ 2o ≠ ∅
4		eqid	⊢ dom ( 𝐹 ∖ I ) = dom ( 𝐹 ∖ I )
5	1 2 4	pmtrfrn	⊢ ( 𝐹 ∈ 𝑅 → ( ( 𝐷 ∈ V ∧ dom ( 𝐹 ∖ I ) ⊆ 𝐷 ∧ dom ( 𝐹 ∖ I ) ≈ 2o ) ∧ 𝐹 = ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) ) )
6	5	simpld	⊢ ( 𝐹 ∈ 𝑅 → ( 𝐷 ∈ V ∧ dom ( 𝐹 ∖ I ) ⊆ 𝐷 ∧ dom ( 𝐹 ∖ I ) ≈ 2o ) )
7	6	simp3d	⊢ ( 𝐹 ∈ 𝑅 → dom ( 𝐹 ∖ I ) ≈ 2o )
8		enen1	⊢ ( dom ( 𝐹 ∖ I ) ≈ 2o → ( dom ( 𝐹 ∖ I ) ≈ ∅ ↔ 2o ≈ ∅ ) )
9	7 8	syl	⊢ ( 𝐹 ∈ 𝑅 → ( dom ( 𝐹 ∖ I ) ≈ ∅ ↔ 2o ≈ ∅ ) )
10		en0	⊢ ( dom ( 𝐹 ∖ I ) ≈ ∅ ↔ dom ( 𝐹 ∖ I ) = ∅ )
11		en0	⊢ ( 2o ≈ ∅ ↔ 2o = ∅ )
12	9 10 11	3bitr3g	⊢ ( 𝐹 ∈ 𝑅 → ( dom ( 𝐹 ∖ I ) = ∅ ↔ 2o = ∅ ) )
13	12	necon3bid	⊢ ( 𝐹 ∈ 𝑅 → ( dom ( 𝐹 ∖ I ) ≠ ∅ ↔ 2o ≠ ∅ ) )
14	3 13	mpbiri	⊢ ( 𝐹 ∈ 𝑅 → dom ( 𝐹 ∖ I ) ≠ ∅ )