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=pmTrspD
pmtrrn.r R=ranT
Assertion pmtrfb FRDVF:D1-1 ontoDdomFI2𝑜

Proof

Step Hyp Ref Expression
1 pmtrrn.t T=pmTrspD
2 pmtrrn.r R=ranT
3 eqid domFI=domFI
4 1 2 3 pmtrfrn FRDVdomFIDdomFI2𝑜F=TdomFI
5 simpl1 DVdomFIDdomFI2𝑜F=TdomFIDV
6 4 5 syl FRDV
7 1 2 pmtrff1o FRF:D1-1 ontoD
8 simpl3 DVdomFIDdomFI2𝑜F=TdomFIdomFI2𝑜
9 4 8 syl FRdomFI2𝑜
10 6 7 9 3jca FRDVF:D1-1 ontoDdomFI2𝑜
11 simp2 DVF:D1-1 ontoDdomFI2𝑜F:D1-1 ontoD
12 difss FIF
13 dmss FIFdomFIdomF
14 12 13 ax-mp domFIdomF
15 f1odm F:D1-1 ontoDdomF=D
16 14 15 sseqtrid F:D1-1 ontoDdomFID
17 1 2 pmtrrn DVdomFIDdomFI2𝑜TdomFIR
18 16 17 syl3an2 DVF:D1-1 ontoDdomFI2𝑜TdomFIR
19 1 2 pmtrff1o TdomFIRTdomFI:D1-1 ontoD
20 18 19 syl DVF:D1-1 ontoDdomFI2𝑜TdomFI:D1-1 ontoD
21 simp3 DVF:D1-1 ontoDdomFI2𝑜domFI2𝑜
22 1 pmtrmvd DVdomFIDdomFI2𝑜domTdomFII=domFI
23 16 22 syl3an2 DVF:D1-1 ontoDdomFI2𝑜domTdomFII=domFI
24 f1otrspeq F:D1-1 ontoDTdomFI:D1-1 ontoDdomFI2𝑜domTdomFII=domFIF=TdomFI
25 11 20 21 23 24 syl22anc DVF:D1-1 ontoDdomFI2𝑜F=TdomFI
26 25 18 eqeltrd DVF:D1-1 ontoDdomFI2𝑜FR
27 10 26 impbii FRDVF:D1-1 ontoDdomFI2𝑜