Metamath Proof Explorer

Theorem pgrple2abl

Description: Every symmetric group on a set with at most 2 elements is abelian. (Contributed by AV, 16-Mar-2019)

Ref Expression
Hypothesis pgrple2abl.g ⊢ G = SymGrp ⁡ A
Assertion pgrple2abl ⊢ A ∈ V ∧ A ≤ 2 → G ∈ Abel

Proof

Step Hyp Ref Expression
1 pgrple2abl.g ⊢ G = SymGrp ⁡ A
2 1 symggrp ⊢ A ∈ V → G ∈ Grp
3 2 adantr ⊢ A ∈ V ∧ A ≤ 2 → G ∈ Grp
4 2nn0 ⊢ 2 ∈ ℕ 0
5 hashbnd ⊢ A ∈ V ∧ 2 ∈ ℕ 0 ∧ A ≤ 2 → A ∈ Fin
6 4 5 mp3an2 ⊢ A ∈ V ∧ A ≤ 2 → A ∈ Fin
7 eqid ⊢ Base G = Base G
8 1 7 symghash ⊢ A ∈ Fin → Base G = A !
9 6 8 syl ⊢ A ∈ V ∧ A ≤ 2 → Base G = A !
10 hashcl ⊢ A ∈ Fin → A ∈ ℕ 0
11 6 10 syl ⊢ A ∈ V ∧ A ≤ 2 → A ∈ ℕ 0
12 faccl ⊢ A ∈ ℕ 0 → A ! ∈ ℕ
13 11 12 syl ⊢ A ∈ V ∧ A ≤ 2 → A ! ∈ ℕ
14 13 nnred ⊢ A ∈ V ∧ A ≤ 2 → A ! ∈ ℝ
15 11 11 nn0expcld ⊢ A ∈ V ∧ A ≤ 2 → A A ∈ ℕ 0
16 15 nn0red ⊢ A ∈ V ∧ A ≤ 2 → A A ∈ ℝ
17 6re ⊢ 6 ∈ ℝ
18 17 a1i ⊢ A ∈ V ∧ A ≤ 2 → 6 ∈ ℝ
19 facubnd ⊢ A ∈ ℕ 0 → A ! ≤ A A
20 11 19 syl ⊢ A ∈ V ∧ A ≤ 2 → A ! ≤ A A
21 exple2lt6 ⊢ A ∈ ℕ 0 ∧ A ≤ 2 → A A < 6
22 11 21 sylancom ⊢ A ∈ V ∧ A ≤ 2 → A A < 6
23 14 16 18 20 22 lelttrd ⊢ A ∈ V ∧ A ≤ 2 → A ! < 6
24 9 23 eqbrtrd ⊢ A ∈ V ∧ A ≤ 2 → Base G < 6
25 7 lt6abl ⊢ G ∈ Grp ∧ Base G < 6 → G ∈ Abel
26 3 24 25 syl2anc ⊢ A ∈ V ∧ A ≤ 2 → G ∈ Abel