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 ) =/= (/) )