Metamath Proof Explorer

Theorem pmtrrn2

Description: For any transposition there are two points it is transposing. (Contributed by SO, 15-Jul-2018)

Ref Expression
Hypotheses pmtrrn.t 
|- T = ( pmTrsp ` D )
pmtrrn.r 
|- R = ran T
Assertion pmtrrn2 
|- ( F e. R -> E. x e. D E. y e. D ( x =/= y /\ F = ( T ` { x , y } ) ) )

Proof

Step Hyp Ref Expression
1 pmtrrn.t 
 |-  T = ( pmTrsp ` D )
2 pmtrrn.r 
 |-  R = ran T
3 eqid 
 |-  dom ( F \ _I ) = dom ( F \ _I )
4 1 2 3 pmtrfrn 
 |-  ( F e. R -> ( ( D e. _V /\ dom ( F \ _I ) C_ D /\ dom ( F \ _I ) ~~ 2o ) /\ F = ( T ` dom ( F \ _I ) ) ) )
5 4 simpld 
 |-  ( F e. R -> ( D e. _V /\ dom ( F \ _I ) C_ D /\ dom ( F \ _I ) ~~ 2o ) )
6 5 simp3d 
 |-  ( F e. R -> dom ( F \ _I ) ~~ 2o )
7 en2 
 |-  ( dom ( F \ _I ) ~~ 2o -> E. x E. y dom ( F \ _I ) = { x , y } )
8 6 7 syl 
 |-  ( F e. R -> E. x E. y dom ( F \ _I ) = { x , y } )
9 5 simp2d 
 |-  ( F e. R -> dom ( F \ _I ) C_ D )
10 4 simprd 
 |-  ( F e. R -> F = ( T ` dom ( F \ _I ) ) )
11 9 6 10 jca32 
 |-  ( F e. R -> ( dom ( F \ _I ) C_ D /\ ( dom ( F \ _I ) ~~ 2o /\ F = ( T ` dom ( F \ _I ) ) ) ) )
12 sseq1 
 |-  ( dom ( F \ _I ) = { x , y } -> ( dom ( F \ _I ) C_ D <-> { x , y } C_ D ) )
13 breq1 
 |-  ( dom ( F \ _I ) = { x , y } -> ( dom ( F \ _I ) ~~ 2o <-> { x , y } ~~ 2o ) )
14 fveq2 
 |-  ( dom ( F \ _I ) = { x , y } -> ( T ` dom ( F \ _I ) ) = ( T ` { x , y } ) )
15 14 eqeq2d 
 |-  ( dom ( F \ _I ) = { x , y } -> ( F = ( T ` dom ( F \ _I ) ) <-> F = ( T ` { x , y } ) ) )
16 13 15 anbi12d 
 |-  ( dom ( F \ _I ) = { x , y } -> ( ( dom ( F \ _I ) ~~ 2o /\ F = ( T ` dom ( F \ _I ) ) ) <-> ( { x , y } ~~ 2o /\ F = ( T ` { x , y } ) ) ) )
17 12 16 anbi12d 
 |-  ( dom ( F \ _I ) = { x , y } -> ( ( dom ( F \ _I ) C_ D /\ ( dom ( F \ _I ) ~~ 2o /\ F = ( T ` dom ( F \ _I ) ) ) ) <-> ( { x , y } C_ D /\ ( { x , y } ~~ 2o /\ F = ( T ` { x , y } ) ) ) ) )
18 11 17 syl5ibcom 
 |-  ( F e. R -> ( dom ( F \ _I ) = { x , y } -> ( { x , y } C_ D /\ ( { x , y } ~~ 2o /\ F = ( T ` { x , y } ) ) ) ) )
19 vex 
 |-  x e. _V
20 vex 
 |-  y e. _V
21 19 20 prss 
 |-  ( ( x e. D /\ y e. D ) <-> { x , y } C_ D )
22 21 bicomi 
 |-  ( { x , y } C_ D <-> ( x e. D /\ y e. D ) )
23 pr2ne 
 |-  ( ( x e. _V /\ y e. _V ) -> ( { x , y } ~~ 2o <-> x =/= y ) )
24 23 el2v 
 |-  ( { x , y } ~~ 2o <-> x =/= y )
25 24 anbi1i 
 |-  ( ( { x , y } ~~ 2o /\ F = ( T ` { x , y } ) ) <-> ( x =/= y /\ F = ( T ` { x , y } ) ) )
26 22 25 anbi12i 
 |-  ( ( { x , y } C_ D /\ ( { x , y } ~~ 2o /\ F = ( T ` { x , y } ) ) ) <-> ( ( x e. D /\ y e. D ) /\ ( x =/= y /\ F = ( T ` { x , y } ) ) ) )
27 18 26 syl6ib 
 |-  ( F e. R -> ( dom ( F \ _I ) = { x , y } -> ( ( x e. D /\ y e. D ) /\ ( x =/= y /\ F = ( T ` { x , y } ) ) ) ) )
28 27 2eximdv 
 |-  ( F e. R -> ( E. x E. y dom ( F \ _I ) = { x , y } -> E. x E. y ( ( x e. D /\ y e. D ) /\ ( x =/= y /\ F = ( T ` { x , y } ) ) ) ) )
29 8 28 mpd 
 |-  ( F e. R -> E. x E. y ( ( x e. D /\ y e. D ) /\ ( x =/= y /\ F = ( T ` { x , y } ) ) ) )
30 r2ex 
 |-  ( E. x e. D E. y e. D ( x =/= y /\ F = ( T ` { x , y } ) ) <-> E. x E. y ( ( x e. D /\ y e. D ) /\ ( x =/= y /\ F = ( T ` { x , y } ) ) ) )
31 29 30 sylibr 
 |-  ( F e. R -> E. x e. D E. y e. D ( x =/= y /\ F = ( T ` { x , y } ) ) )