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 } ) ) )