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 ⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
Assertion pgrple2abl ( ( 𝐴 ∈ 𝑉 ∧ ( ♯ ‘ 𝐴 ) ≤ 2 ) → 𝐺 ∈ Abel )

Proof

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