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=\mathrm{SymGrp}\left(A\right)$$
Assertion	pgrple2abl	$$⊢\left(A\in V\wedge \left|A\right|\le 2\right)\to G\in \mathrm{Abel}$$

Proof

Step	Hyp	Ref	Expression
1		pgrple2abl.g	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
2	1	symggrp	$$⊢A\in V\to G\in \mathrm{Grp}$$
3	2	adantr	$$⊢\left(A\in V\wedge \left|A\right|\le 2\right)\to G\in \mathrm{Grp}$$
4		2nn0	$$⊢2\in {\mathbb{N}}_0$$
5		hashbnd	$$⊢\left(A\in V\wedge 2\in {\mathbb{N}}_0\wedge \left|A\right|\le 2\right)\to A\in \mathrm{Fin}$$
6	4 5	mp3an2	$$⊢\left(A\in V\wedge \left|A\right|\le 2\right)\to A\in \mathrm{Fin}$$
7		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
8	1 7	symghash	$$⊢A\in \mathrm{Fin}\to \left|{\mathrm{Base}}_G\right|=\left|A\right|!$$
9	6 8	syl	$$⊢\left(A\in V\wedge \left|A\right|\le 2\right)\to \left|{\mathrm{Base}}_G\right|=\left|A\right|!$$
10		hashcl	$$⊢A\in \mathrm{Fin}\to \left|A\right|\in {\mathbb{N}}_0$$
11	6 10	syl	$$⊢\left(A\in V\wedge \left|A\right|\le 2\right)\to \left|A\right|\in {\mathbb{N}}_0$$
12		faccl	$$⊢\left|A\right|\in {\mathbb{N}}_0\to \left|A\right|!\in \mathbb{N}$$
13	11 12	syl	$$⊢\left(A\in V\wedge \left|A\right|\le 2\right)\to \left|A\right|!\in \mathbb{N}$$
14	13	nnred	$$⊢\left(A\in V\wedge \left|A\right|\le 2\right)\to \left|A\right|!\in ℝ$$
15	11 11	nn0expcld	$$⊢\left(A\in V\wedge \left|A\right|\le 2\right)\to {\left|A\right|}^{\left|A\right|}\in {\mathbb{N}}_0$$
16	15	nn0red	$$⊢\left(A\in V\wedge \left|A\right|\le 2\right)\to {\left|A\right|}^{\left|A\right|}\in ℝ$$
17		6re	$$⊢6\in ℝ$$
18	17	a1i	$$⊢\left(A\in V\wedge \left|A\right|\le 2\right)\to 6\in ℝ$$
19		facubnd	$$⊢\left|A\right|\in {\mathbb{N}}_0\to \left|A\right|!\le {\left|A\right|}^{\left|A\right|}$$
20	11 19	syl	$$⊢\left(A\in V\wedge \left|A\right|\le 2\right)\to \left|A\right|!\le {\left|A\right|}^{\left|A\right|}$$
21		exple2lt6	$$⊢\left(\left|A\right|\in {\mathbb{N}}_0\wedge \left|A\right|\le 2\right)\to {\left|A\right|}^{\left|A\right|}<6$$
22	11 21	sylancom	$$⊢\left(A\in V\wedge \left|A\right|\le 2\right)\to {\left|A\right|}^{\left|A\right|}<6$$
23	14 16 18 20 22	lelttrd	$$⊢\left(A\in V\wedge \left|A\right|\le 2\right)\to \left|A\right|!<6$$
24	9 23	eqbrtrd	$$⊢\left(A\in V\wedge \left|A\right|\le 2\right)\to \left|{\mathrm{Base}}_G\right|<6$$
25	7	lt6abl	$$⊢\left(G\in \mathrm{Grp}\wedge \left|{\mathrm{Base}}_G\right|<6\right)\to G\in \mathrm{Abel}$$
26	3 24 25	syl2anc	$$⊢\left(A\in V\wedge \left|A\right|\le 2\right)\to G\in \mathrm{Abel}$$