This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pmtrfmvdn0

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

Ref Expression
Hypotheses pmtrrn.t ⊢ T = pmTrsp ⁡ D
pmtrrn.r ⊢ R = ran ⁡ T
Assertion pmtrfmvdn0 ⊢ F ∈ R → dom ⁡ F ∖ I ≠ ∅

Proof

Step Hyp Ref Expression
1 pmtrrn.t ⊢ T = pmTrsp ⁡ D
2 pmtrrn.r ⊢ R = ran ⁡ T
3 2on0 ⊢ 2 𝑜 ≠ ∅
4 eqid ⊢ dom ⁡ F ∖ I = dom ⁡ F ∖ I
5 1 2 4 pmtrfrn ⊢ F ∈ R → D ∈ V ∧ dom ⁡ F ∖ I ⊆ D ∧ dom ⁡ F ∖ I ≈ 2 𝑜 ∧ F = T ⁡ dom ⁡ F ∖ I
6 5 simpld ⊢ F ∈ R → D ∈ V ∧ dom ⁡ F ∖ I ⊆ D ∧ dom ⁡ F ∖ I ≈ 2 𝑜
7 6 simp3d ⊢ F ∈ R → dom ⁡ F ∖ I ≈ 2 𝑜
8 enen1 ⊢ dom ⁡ F ∖ I ≈ 2 𝑜 → dom ⁡ F ∖ I ≈ ∅ ↔ 2 𝑜 ≈ ∅
9 7 8 syl ⊢ F ∈ R → dom ⁡ F ∖ I ≈ ∅ ↔ 2 𝑜 ≈ ∅
10 en0 ⊢ dom ⁡ F ∖ I ≈ ∅ ↔ dom ⁡ F ∖ I = ∅
11 en0 ⊢ 2 𝑜 ≈ ∅ ↔ 2 𝑜 = ∅
12 9 10 11 3bitr3g ⊢ F ∈ R → dom ⁡ F ∖ I = ∅ ↔ 2 𝑜 = ∅
13 12 necon3bid ⊢ F ∈ R → dom ⁡ F ∖ I ≠ ∅ ↔ 2 𝑜 ≠ ∅
14 3 13 mpbiri ⊢ F ∈ R → dom ⁡ F ∖ I ≠ ∅