Description: An intrinsic characterization of the transposition permutations. (Contributed by Stefan O'Rear, 22-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | pmtrrn.t | |
|
pmtrrn.r | |
||
Assertion | pmtrfb | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pmtrrn.t | |
|
2 | pmtrrn.r | |
|
3 | eqid | |
|
4 | 1 2 3 | pmtrfrn | |
5 | simpl1 | |
|
6 | 4 5 | syl | |
7 | 1 2 | pmtrff1o | |
8 | simpl3 | |
|
9 | 4 8 | syl | |
10 | 6 7 9 | 3jca | |
11 | simp2 | |
|
12 | difss | |
|
13 | dmss | |
|
14 | 12 13 | ax-mp | |
15 | f1odm | |
|
16 | 14 15 | sseqtrid | |
17 | 1 2 | pmtrrn | |
18 | 16 17 | syl3an2 | |
19 | 1 2 | pmtrff1o | |
20 | 18 19 | syl | |
21 | simp3 | |
|
22 | 1 | pmtrmvd | |
23 | 16 22 | syl3an2 | |
24 | f1otrspeq | |
|
25 | 11 20 21 23 24 | syl22anc | |
26 | 25 18 | eqeltrd | |
27 | 10 26 | impbii | |