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