Theorem symg2hash

Description: The symmetric group on a (proper) pair has cardinality 2 . (Contributed by AV, 9-Dec-2018)

	Ref	Expression
Hypotheses	symg1bas.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
	symg1bas.2	$$⊢B={\mathrm{Base}}_G$$
	symg2bas.0	$$⊢A=\left\{I,J\right\}$$
Assertion	symg2hash	$$⊢\left(I\in V\wedge J\in W\wedge I\ne J\right)\to \left|B\right|=2$$

Proof

Step	Hyp	Ref	Expression
1		symg1bas.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
2		symg1bas.2	$$⊢B={\mathrm{Base}}_G$$
3		symg2bas.0	$$⊢A=\left\{I,J\right\}$$
4		prfi	$$⊢\left\{I,J\right\}\in \mathrm{Fin}$$
5	3 4	eqeltri	$$⊢A\in \mathrm{Fin}$$
6	1 2	symghash	$$⊢A\in \mathrm{Fin}\to \left|B\right|=\left|A\right|!$$
7	5 6	ax-mp	$$⊢\left|B\right|=\left|A\right|!$$
8	3	fveq2i	$$⊢\left|A\right|=\left|\left\{I,J\right\}\right|$$
9		elex	$$⊢I\in V\to I\in \mathrm{V}$$
10		elex	$$⊢J\in W\to J\in \mathrm{V}$$
11		id	$$⊢I\ne J\to I\ne J$$
12	9 10 11	3anim123i	$$⊢\left(I\in V\wedge J\in W\wedge I\ne J\right)\to \left(I\in \mathrm{V}\wedge J\in \mathrm{V}\wedge I\ne J\right)$$
13		hashprb	$$⊢\left(I\in \mathrm{V}\wedge J\in \mathrm{V}\wedge I\ne J\right)\leftrightarrow \left|\left\{I,J\right\}\right|=2$$
14	12 13	sylib	$$⊢\left(I\in V\wedge J\in W\wedge I\ne J\right)\to \left|\left\{I,J\right\}\right|=2$$
15	8 14	syl5eq	$$⊢\left(I\in V\wedge J\in W\wedge I\ne J\right)\to \left|A\right|=2$$
16	15	fveq2d	$$⊢\left(I\in V\wedge J\in W\wedge I\ne J\right)\to \left|A\right|!=2!$$
17		fac2	$$⊢2!=2$$
18	16 17	eqtrdi	$$⊢\left(I\in V\wedge J\in W\wedge I\ne J\right)\to \left|A\right|!=2$$
19	7 18	syl5eq	$$⊢\left(I\in V\wedge J\in W\wedge I\ne J\right)\to \left|B\right|=2$$