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 ⊢ 𝑇 = ( 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 ) ≠ ∅ )