Description: Every symmetric group on a set with more than 2 elements is not abelian, see also the remark in Rotman p. 28. (Contributed by AV, 21-Mar-2019)
Ref | Expression | ||
---|---|---|---|
Hypothesis | pgrple2abl.g | |
|
Assertion | pgrpgt2nabl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pgrple2abl.g | |
|
2 | eqid | |
|
3 | eqid | |
|
4 | 2 1 3 | symgtrf | |
5 | hashcl | |
|
6 | 2nn0 | |
|
7 | nn0ltp1le | |
|
8 | 6 7 | mpan | |
9 | 2p1e3 | |
|
10 | 9 | a1i | |
11 | 10 | breq1d | |
12 | 8 11 | bitrd | |
13 | 12 | biimpd | |
14 | 13 | adantld | |
15 | 5 14 | syl | |
16 | 3re | |
|
17 | 16 | rexri | |
18 | pnfge | |
|
19 | 17 18 | ax-mp | |
20 | hashinf | |
|
21 | 19 20 | breqtrrid | |
22 | 21 | ex | |
23 | 22 | adantr | |
24 | 23 | com12 | |
25 | 15 24 | pm2.61i | |
26 | eqid | |
|
27 | 26 | pmtr3ncom | |
28 | rexcom | |
|
29 | 27 28 | sylibr | |
30 | 25 29 | syldan | |
31 | ssrexv | |
|
32 | 31 | reximdv | |
33 | 4 30 32 | mpsyl | |
34 | ssrexv | |
|
35 | 4 33 34 | mpsyl | |
36 | eqid | |
|
37 | 1 3 36 | symgov | |
38 | 37 | adantl | |
39 | pm3.22 | |
|
40 | 39 | adantl | |
41 | 1 3 36 | symgov | |
42 | 40 41 | syl | |
43 | 38 42 | neeq12d | |
44 | 43 | 2rexbidva | |
45 | 35 44 | mpbird | |
46 | rexnal | |
|
47 | rexnal | |
|
48 | df-ne | |
|
49 | 48 | bicomi | |
50 | 49 | rexbii | |
51 | 47 50 | bitr3i | |
52 | 51 | rexbii | |
53 | 46 52 | bitr3i | |
54 | 45 53 | sylibr | |
55 | 54 | intnand | |
56 | 55 | intnand | |
57 | df-nel | |
|
58 | isabl | |
|
59 | 3 36 | iscmn | |
60 | 59 | anbi2i | |
61 | 58 60 | bitri | |
62 | 57 61 | xchbinx | |
63 | 56 62 | sylibr | |