Metamath Proof Explorer


Theorem pmtrfb

Description: An intrinsic characterization of the transposition permutations. (Contributed by Stefan O'Rear, 22-Aug-2015)

Ref Expression
Hypotheses pmtrrn.t
|- T = ( pmTrsp ` D )
pmtrrn.r
|- R = ran T
Assertion pmtrfb
|- ( F e. R <-> ( D e. _V /\ F : D -1-1-onto-> D /\ dom ( F \ _I ) ~~ 2o ) )

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 simpl1
 |-  ( ( ( D e. _V /\ dom ( F \ _I ) C_ D /\ dom ( F \ _I ) ~~ 2o ) /\ F = ( T ` dom ( F \ _I ) ) ) -> D e. _V )
6 4 5 syl
 |-  ( F e. R -> D e. _V )
7 1 2 pmtrff1o
 |-  ( F e. R -> F : D -1-1-onto-> D )
8 simpl3
 |-  ( ( ( D e. _V /\ dom ( F \ _I ) C_ D /\ dom ( F \ _I ) ~~ 2o ) /\ F = ( T ` dom ( F \ _I ) ) ) -> dom ( F \ _I ) ~~ 2o )
9 4 8 syl
 |-  ( F e. R -> dom ( F \ _I ) ~~ 2o )
10 6 7 9 3jca
 |-  ( F e. R -> ( D e. _V /\ F : D -1-1-onto-> D /\ dom ( F \ _I ) ~~ 2o ) )
11 simp2
 |-  ( ( D e. _V /\ F : D -1-1-onto-> D /\ dom ( F \ _I ) ~~ 2o ) -> F : D -1-1-onto-> D )
12 difss
 |-  ( F \ _I ) C_ F
13 dmss
 |-  ( ( F \ _I ) C_ F -> dom ( F \ _I ) C_ dom F )
14 12 13 ax-mp
 |-  dom ( F \ _I ) C_ dom F
15 f1odm
 |-  ( F : D -1-1-onto-> D -> dom F = D )
16 14 15 sseqtrid
 |-  ( F : D -1-1-onto-> D -> dom ( F \ _I ) C_ D )
17 1 2 pmtrrn
 |-  ( ( D e. _V /\ dom ( F \ _I ) C_ D /\ dom ( F \ _I ) ~~ 2o ) -> ( T ` dom ( F \ _I ) ) e. R )
18 16 17 syl3an2
 |-  ( ( D e. _V /\ F : D -1-1-onto-> D /\ dom ( F \ _I ) ~~ 2o ) -> ( T ` dom ( F \ _I ) ) e. R )
19 1 2 pmtrff1o
 |-  ( ( T ` dom ( F \ _I ) ) e. R -> ( T ` dom ( F \ _I ) ) : D -1-1-onto-> D )
20 18 19 syl
 |-  ( ( D e. _V /\ F : D -1-1-onto-> D /\ dom ( F \ _I ) ~~ 2o ) -> ( T ` dom ( F \ _I ) ) : D -1-1-onto-> D )
21 simp3
 |-  ( ( D e. _V /\ F : D -1-1-onto-> D /\ dom ( F \ _I ) ~~ 2o ) -> dom ( F \ _I ) ~~ 2o )
22 1 pmtrmvd
 |-  ( ( D e. _V /\ dom ( F \ _I ) C_ D /\ dom ( F \ _I ) ~~ 2o ) -> dom ( ( T ` dom ( F \ _I ) ) \ _I ) = dom ( F \ _I ) )
23 16 22 syl3an2
 |-  ( ( D e. _V /\ F : D -1-1-onto-> D /\ dom ( F \ _I ) ~~ 2o ) -> dom ( ( T ` dom ( F \ _I ) ) \ _I ) = dom ( F \ _I ) )
24 f1otrspeq
 |-  ( ( ( F : D -1-1-onto-> D /\ ( T ` dom ( F \ _I ) ) : D -1-1-onto-> D ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( ( T ` dom ( F \ _I ) ) \ _I ) = dom ( F \ _I ) ) ) -> F = ( T ` dom ( F \ _I ) ) )
25 11 20 21 23 24 syl22anc
 |-  ( ( D e. _V /\ F : D -1-1-onto-> D /\ dom ( F \ _I ) ~~ 2o ) -> F = ( T ` dom ( F \ _I ) ) )
26 25 18 eqeltrd
 |-  ( ( D e. _V /\ F : D -1-1-onto-> D /\ dom ( F \ _I ) ~~ 2o ) -> F e. R )
27 10 26 impbii
 |-  ( F e. R <-> ( D e. _V /\ F : D -1-1-onto-> D /\ dom ( F \ _I ) ~~ 2o ) )