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 e. R -> dom ( F \ _I ) =/= (/) )

Proof

Step Hyp Ref Expression
1 pmtrrn.t
 |-  T = ( pmTrsp ` D )
2 pmtrrn.r
 |-  R = ran T
3 2on0
 |-  2o =/= (/)
4 eqid
 |-  dom ( F \ _I ) = dom ( F \ _I )
5 1 2 4 pmtrfrn
 |-  ( F e. R -> ( ( D e. _V /\ dom ( F \ _I ) C_ D /\ dom ( F \ _I ) ~~ 2o ) /\ F = ( T ` dom ( F \ _I ) ) ) )
6 5 simpld
 |-  ( F e. R -> ( D e. _V /\ dom ( F \ _I ) C_ D /\ dom ( F \ _I ) ~~ 2o ) )
7 6 simp3d
 |-  ( F e. R -> dom ( F \ _I ) ~~ 2o )
8 enen1
 |-  ( dom ( F \ _I ) ~~ 2o -> ( dom ( F \ _I ) ~~ (/) <-> 2o ~~ (/) ) )
9 7 8 syl
 |-  ( F e. R -> ( dom ( F \ _I ) ~~ (/) <-> 2o ~~ (/) ) )
10 en0
 |-  ( dom ( F \ _I ) ~~ (/) <-> dom ( F \ _I ) = (/) )
11 en0
 |-  ( 2o ~~ (/) <-> 2o = (/) )
12 9 10 11 3bitr3g
 |-  ( F e. R -> ( dom ( F \ _I ) = (/) <-> 2o = (/) ) )
13 12 necon3bid
 |-  ( F e. R -> ( dom ( F \ _I ) =/= (/) <-> 2o =/= (/) ) )
14 3 13 mpbiri
 |-  ( F e. R -> dom ( F \ _I ) =/= (/) )