Theorem symg2bas

Description: The symmetric group on a pair is the symmetric group S_2 consisting of the identity and the transposition. Notice that this statement is valid for proper pairs only. In the case that both elements are identical, i.e., the pairs are actually singletons, this theorem would be about S_1, see Theorem symg1bas . (Contributed by AV, 9-Dec-2018) (Proof shortened by AV, 16-Jun-2022)

	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	symg2bas	$$⊢\left(I\in V\wedge J\in W\right)\to B=\left\{\left\{⟨I,I⟩,⟨J,J⟩\right\},\left\{⟨I,J⟩,⟨J,I⟩\right\}\right\}$$

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		eqid	$$⊢\mathrm{SymGrp}\left(\left\{J\right\}\right)=\mathrm{SymGrp}\left(\left\{J\right\}\right)$$
5		eqid	$$⊢{\mathrm{Base}}_{\mathrm{SymGrp}\left(\left\{J\right\}\right)}={\mathrm{Base}}_{\mathrm{SymGrp}\left(\left\{J\right\}\right)}$$
6		eqid	$$⊢\left\{J\right\}=\left\{J\right\}$$
7	4 5 6	symg1bas	$$⊢J\in W\to {\mathrm{Base}}_{\mathrm{SymGrp}\left(\left\{J\right\}\right)}=\left\{\left\{⟨J,J⟩\right\}\right\}$$
8	7	ad2antll	$$⊢\left(I=J\wedge \left(I\in V\wedge J\in W\right)\right)\to {\mathrm{Base}}_{\mathrm{SymGrp}\left(\left\{J\right\}\right)}=\left\{\left\{⟨J,J⟩\right\}\right\}$$
9		df-pr	$$⊢\left\{I,J\right\}=\left\{I\right\}\cup \left\{J\right\}$$
10		sneq	$$⊢I=J\to \left\{I\right\}=\left\{J\right\}$$
11	10	uneq1d	$$⊢I=J\to \left\{I\right\}\cup \left\{J\right\}=\left\{J\right\}\cup \left\{J\right\}$$
12	11	adantr	$$⊢\left(I=J\wedge \left(I\in V\wedge J\in W\right)\right)\to \left\{I\right\}\cup \left\{J\right\}=\left\{J\right\}\cup \left\{J\right\}$$
13		unidm	$$⊢\left\{J\right\}\cup \left\{J\right\}=\left\{J\right\}$$
14	12 13	eqtrdi	$$⊢\left(I=J\wedge \left(I\in V\wedge J\in W\right)\right)\to \left\{I\right\}\cup \left\{J\right\}=\left\{J\right\}$$
15	9 14	eqtrid	$$⊢\left(I=J\wedge \left(I\in V\wedge J\in W\right)\right)\to \left\{I,J\right\}=\left\{J\right\}$$
16	3 15	eqtrid	$$⊢\left(I=J\wedge \left(I\in V\wedge J\in W\right)\right)\to A=\left\{J\right\}$$
17	16	fveq2d	$$⊢\left(I=J\wedge \left(I\in V\wedge J\in W\right)\right)\to \mathrm{SymGrp}\left(A\right)=\mathrm{SymGrp}\left(\left\{J\right\}\right)$$
18	1 17	eqtrid	$$⊢\left(I=J\wedge \left(I\in V\wedge J\in W\right)\right)\to G=\mathrm{SymGrp}\left(\left\{J\right\}\right)$$
19	18	fveq2d	$$⊢\left(I=J\wedge \left(I\in V\wedge J\in W\right)\right)\to {\mathrm{Base}}_G={\mathrm{Base}}_{\mathrm{SymGrp}\left(\left\{J\right\}\right)}$$
20	2 19	eqtrid	$$⊢\left(I=J\wedge \left(I\in V\wedge J\in W\right)\right)\to B={\mathrm{Base}}_{\mathrm{SymGrp}\left(\left\{J\right\}\right)}$$
21		id	$$⊢I=J\to I=J$$
22	21 21	opeq12d	$$⊢I=J\to ⟨I,I⟩=⟨J,J⟩$$
23	22	adantr	$$⊢\left(I=J\wedge \left(I\in V\wedge J\in W\right)\right)\to ⟨I,I⟩=⟨J,J⟩$$
24	23	preq1d	$$⊢\left(I=J\wedge \left(I\in V\wedge J\in W\right)\right)\to \left\{⟨I,I⟩,⟨J,J⟩\right\}=\left\{⟨J,J⟩,⟨J,J⟩\right\}$$
25		eqid	$$⊢⟨J,J⟩=⟨J,J⟩$$
26		opex	$$⊢⟨J,J⟩\in \mathrm{V}$$
27	26 26	preqsn	$$⊢\left\{⟨J,J⟩,⟨J,J⟩\right\}=\left\{⟨J,J⟩\right\}\leftrightarrow \left(⟨J,J⟩=⟨J,J⟩\wedge ⟨J,J⟩=⟨J,J⟩\right)$$
28	25 25 27	mpbir2an	$$⊢\left\{⟨J,J⟩,⟨J,J⟩\right\}=\left\{⟨J,J⟩\right\}$$
29	24 28	eqtrdi	$$⊢\left(I=J\wedge \left(I\in V\wedge J\in W\right)\right)\to \left\{⟨I,I⟩,⟨J,J⟩\right\}=\left\{⟨J,J⟩\right\}$$
30		opeq1	$$⊢I=J\to ⟨I,J⟩=⟨J,J⟩$$
31		opeq2	$$⊢I=J\to ⟨J,I⟩=⟨J,J⟩$$
32	30 31	preq12d	$$⊢I=J\to \left\{⟨I,J⟩,⟨J,I⟩\right\}=\left\{⟨J,J⟩,⟨J,J⟩\right\}$$
33	32 28	eqtrdi	$$⊢I=J\to \left\{⟨I,J⟩,⟨J,I⟩\right\}=\left\{⟨J,J⟩\right\}$$
34	33	adantr	$$⊢\left(I=J\wedge \left(I\in V\wedge J\in W\right)\right)\to \left\{⟨I,J⟩,⟨J,I⟩\right\}=\left\{⟨J,J⟩\right\}$$
35	29 34	preq12d	$$⊢\left(I=J\wedge \left(I\in V\wedge J\in W\right)\right)\to \left\{\left\{⟨I,I⟩,⟨J,J⟩\right\},\left\{⟨I,J⟩,⟨J,I⟩\right\}\right\}=\left\{\left\{⟨J,J⟩\right\},\left\{⟨J,J⟩\right\}\right\}$$
36		eqid	$$⊢\left\{⟨J,J⟩\right\}=\left\{⟨J,J⟩\right\}$$
37		snex	$$⊢\left\{⟨J,J⟩\right\}\in \mathrm{V}$$
38	37 37	preqsn	$$⊢\left\{\left\{⟨J,J⟩\right\},\left\{⟨J,J⟩\right\}\right\}=\left\{\left\{⟨J,J⟩\right\}\right\}\leftrightarrow \left(\left\{⟨J,J⟩\right\}=\left\{⟨J,J⟩\right\}\wedge \left\{⟨J,J⟩\right\}=\left\{⟨J,J⟩\right\}\right)$$
39	36 36 38	mpbir2an	$$⊢\left\{\left\{⟨J,J⟩\right\},\left\{⟨J,J⟩\right\}\right\}=\left\{\left\{⟨J,J⟩\right\}\right\}$$
40	35 39	eqtrdi	$$⊢\left(I=J\wedge \left(I\in V\wedge J\in W\right)\right)\to \left\{\left\{⟨I,I⟩,⟨J,J⟩\right\},\left\{⟨I,J⟩,⟨J,I⟩\right\}\right\}=\left\{\left\{⟨J,J⟩\right\}\right\}$$
41	8 20 40	3eqtr4d	$$⊢\left(I=J\wedge \left(I\in V\wedge J\in W\right)\right)\to B=\left\{\left\{⟨I,I⟩,⟨J,J⟩\right\},\left\{⟨I,J⟩,⟨J,I⟩\right\}\right\}$$
42	2	fvexi	$$⊢B\in \mathrm{V}$$
43	42	a1i	$$⊢\left(\neg I=J\wedge \left(I\in V\wedge J\in W\right)\right)\to B\in \mathrm{V}$$
44		neqne	$$⊢\neg I=J\to I\ne J$$
45	44	anim2i	$$⊢\left(\left(I\in V\wedge J\in W\right)\wedge \neg I=J\right)\to \left(\left(I\in V\wedge J\in W\right)\wedge I\ne J\right)$$
46		df-3an	$$⊢\left(I\in V\wedge J\in W\wedge I\ne J\right)\leftrightarrow \left(\left(I\in V\wedge J\in W\right)\wedge I\ne J\right)$$
47	45 46	sylibr	$$⊢\left(\left(I\in V\wedge J\in W\right)\wedge \neg I=J\right)\to \left(I\in V\wedge J\in W\wedge I\ne J\right)$$
48	47	ancoms	$$⊢\left(\neg I=J\wedge \left(I\in V\wedge J\in W\right)\right)\to \left(I\in V\wedge J\in W\wedge I\ne J\right)$$
49	1 2 3	symg2hash	$$⊢\left(I\in V\wedge J\in W\wedge I\ne J\right)\to \left|B\right|=2$$
50	48 49	syl	$$⊢\left(\neg I=J\wedge \left(I\in V\wedge J\in W\right)\right)\to \left|B\right|=2$$
51		id	$$⊢I\in V\to I\in V$$
52	51	ancri	$$⊢I\in V\to \left(I\in V\wedge I\in V\right)$$
53		id	$$⊢J\in W\to J\in W$$
54	53	ancri	$$⊢J\in W\to \left(J\in W\wedge J\in W\right)$$
55	52 54	anim12i	$$⊢\left(I\in V\wedge J\in W\right)\to \left(\left(I\in V\wedge I\in V\right)\wedge \left(J\in W\wedge J\in W\right)\right)$$
56		df-ne	$$⊢I\ne J\leftrightarrow \neg I=J$$
57		id	$$⊢I\ne J\to I\ne J$$
58	57	ancri	$$⊢I\ne J\to \left(I\ne J\wedge I\ne J\right)$$
59	56 58	sylbir	$$⊢\neg I=J\to \left(I\ne J\wedge I\ne J\right)$$
60		f1oprg	$$⊢\left(\left(I\in V\wedge I\in V\right)\wedge \left(J\in W\wedge J\in W\right)\right)\to \left(\left(I\ne J\wedge I\ne J\right)\to \left\{⟨I,I⟩,⟨J,J⟩\right\}:\left\{I,J\right\}\underset{1-1\; onto}{⟶}\left\{I,J\right\}\right)$$
61	60	imp	$$⊢\left(\left(\left(I\in V\wedge I\in V\right)\wedge \left(J\in W\wedge J\in W\right)\right)\wedge \left(I\ne J\wedge I\ne J\right)\right)\to \left\{⟨I,I⟩,⟨J,J⟩\right\}:\left\{I,J\right\}\underset{1-1\; onto}{⟶}\left\{I,J\right\}$$
62	55 59 61	syl2anr	$$⊢\left(\neg I=J\wedge \left(I\in V\wedge J\in W\right)\right)\to \left\{⟨I,I⟩,⟨J,J⟩\right\}:\left\{I,J\right\}\underset{1-1\; onto}{⟶}\left\{I,J\right\}$$
63		eqidd	$$⊢A=\left\{I,J\right\}\to \left\{⟨I,I⟩,⟨J,J⟩\right\}=\left\{⟨I,I⟩,⟨J,J⟩\right\}$$
64		id	$$⊢A=\left\{I,J\right\}\to A=\left\{I,J\right\}$$
65	63 64 64	f1oeq123d	$$⊢A=\left\{I,J\right\}\to \left(\left\{⟨I,I⟩,⟨J,J⟩\right\}:A\underset{1-1\; onto}{⟶}A\leftrightarrow \left\{⟨I,I⟩,⟨J,J⟩\right\}:\left\{I,J\right\}\underset{1-1\; onto}{⟶}\left\{I,J\right\}\right)$$
66	3 65	ax-mp	$$⊢\left\{⟨I,I⟩,⟨J,J⟩\right\}:A\underset{1-1\; onto}{⟶}A\leftrightarrow \left\{⟨I,I⟩,⟨J,J⟩\right\}:\left\{I,J\right\}\underset{1-1\; onto}{⟶}\left\{I,J\right\}$$
67	62 66	sylibr	$$⊢\left(\neg I=J\wedge \left(I\in V\wedge J\in W\right)\right)\to \left\{⟨I,I⟩,⟨J,J⟩\right\}:A\underset{1-1\; onto}{⟶}A$$
68		prex	$$⊢\left\{⟨I,I⟩,⟨J,J⟩\right\}\in \mathrm{V}$$
69	1 2	elsymgbas2	$$⊢\left\{⟨I,I⟩,⟨J,J⟩\right\}\in \mathrm{V}\to \left(\left\{⟨I,I⟩,⟨J,J⟩\right\}\in B\leftrightarrow \left\{⟨I,I⟩,⟨J,J⟩\right\}:A\underset{1-1\; onto}{⟶}A\right)$$
70	68 69	ax-mp	$$⊢\left\{⟨I,I⟩,⟨J,J⟩\right\}\in B\leftrightarrow \left\{⟨I,I⟩,⟨J,J⟩\right\}:A\underset{1-1\; onto}{⟶}A$$
71	67 70	sylibr	$$⊢\left(\neg I=J\wedge \left(I\in V\wedge J\in W\right)\right)\to \left\{⟨I,I⟩,⟨J,J⟩\right\}\in B$$
72		f1oprswap	$$⊢\left(I\in V\wedge J\in W\right)\to \left\{⟨I,J⟩,⟨J,I⟩\right\}:\left\{I,J\right\}\underset{1-1\; onto}{⟶}\left\{I,J\right\}$$
73		eqidd	$$⊢A=\left\{I,J\right\}\to \left\{⟨I,J⟩,⟨J,I⟩\right\}=\left\{⟨I,J⟩,⟨J,I⟩\right\}$$
74	73 64 64	f1oeq123d	$$⊢A=\left\{I,J\right\}\to \left(\left\{⟨I,J⟩,⟨J,I⟩\right\}:A\underset{1-1\; onto}{⟶}A\leftrightarrow \left\{⟨I,J⟩,⟨J,I⟩\right\}:\left\{I,J\right\}\underset{1-1\; onto}{⟶}\left\{I,J\right\}\right)$$
75	3 74	ax-mp	$$⊢\left\{⟨I,J⟩,⟨J,I⟩\right\}:A\underset{1-1\; onto}{⟶}A\leftrightarrow \left\{⟨I,J⟩,⟨J,I⟩\right\}:\left\{I,J\right\}\underset{1-1\; onto}{⟶}\left\{I,J\right\}$$
76	72 75	sylibr	$$⊢\left(I\in V\wedge J\in W\right)\to \left\{⟨I,J⟩,⟨J,I⟩\right\}:A\underset{1-1\; onto}{⟶}A$$
77	76	adantl	$$⊢\left(\neg I=J\wedge \left(I\in V\wedge J\in W\right)\right)\to \left\{⟨I,J⟩,⟨J,I⟩\right\}:A\underset{1-1\; onto}{⟶}A$$
78		prex	$$⊢\left\{⟨I,J⟩,⟨J,I⟩\right\}\in \mathrm{V}$$
79	1 2	elsymgbas2	$$⊢\left\{⟨I,J⟩,⟨J,I⟩\right\}\in \mathrm{V}\to \left(\left\{⟨I,J⟩,⟨J,I⟩\right\}\in B\leftrightarrow \left\{⟨I,J⟩,⟨J,I⟩\right\}:A\underset{1-1\; onto}{⟶}A\right)$$
80	78 79	ax-mp	$$⊢\left\{⟨I,J⟩,⟨J,I⟩\right\}\in B\leftrightarrow \left\{⟨I,J⟩,⟨J,I⟩\right\}:A\underset{1-1\; onto}{⟶}A$$
81	77 80	sylibr	$$⊢\left(\neg I=J\wedge \left(I\in V\wedge J\in W\right)\right)\to \left\{⟨I,J⟩,⟨J,I⟩\right\}\in B$$
82		opex	$$⊢⟨I,I⟩\in \mathrm{V}$$
83	82 26	pm3.2i	$$⊢\left(⟨I,I⟩\in \mathrm{V}\wedge ⟨J,J⟩\in \mathrm{V}\right)$$
84		opex	$$⊢⟨I,J⟩\in \mathrm{V}$$
85		opex	$$⊢⟨J,I⟩\in \mathrm{V}$$
86	84 85	pm3.2i	$$⊢\left(⟨I,J⟩\in \mathrm{V}\wedge ⟨J,I⟩\in \mathrm{V}\right)$$
87	83 86	pm3.2i	$$⊢\left(\left(⟨I,I⟩\in \mathrm{V}\wedge ⟨J,J⟩\in \mathrm{V}\right)\wedge \left(⟨I,J⟩\in \mathrm{V}\wedge ⟨J,I⟩\in \mathrm{V}\right)\right)$$
88		opthg2	$$⊢\left(I\in V\wedge J\in W\right)\to \left(⟨I,I⟩=⟨I,J⟩\leftrightarrow \left(I=I\wedge I=J\right)\right)$$
89		eqtr	$$⊢\left(I=I\wedge I=J\right)\to I=J$$
90	88 89	syl6bi	$$⊢\left(I\in V\wedge J\in W\right)\to \left(⟨I,I⟩=⟨I,J⟩\to I=J\right)$$
91	90	necon3d	$$⊢\left(I\in V\wedge J\in W\right)\to \left(I\ne J\to ⟨I,I⟩\ne ⟨I,J⟩\right)$$
92	91	com12	$$⊢I\ne J\to \left(\left(I\in V\wedge J\in W\right)\to ⟨I,I⟩\ne ⟨I,J⟩\right)$$
93	56 92	sylbir	$$⊢\neg I=J\to \left(\left(I\in V\wedge J\in W\right)\to ⟨I,I⟩\ne ⟨I,J⟩\right)$$
94	93	imp	$$⊢\left(\neg I=J\wedge \left(I\in V\wedge J\in W\right)\right)\to ⟨I,I⟩\ne ⟨I,J⟩$$
95	52	adantr	$$⊢\left(I\in V\wedge J\in W\right)\to \left(I\in V\wedge I\in V\right)$$
96		opthg	$$⊢\left(I\in V\wedge I\in V\right)\to \left(⟨I,I⟩=⟨J,I⟩\leftrightarrow \left(I=J\wedge I=I\right)\right)$$
97	95 96	syl	$$⊢\left(I\in V\wedge J\in W\right)\to \left(⟨I,I⟩=⟨J,I⟩\leftrightarrow \left(I=J\wedge I=I\right)\right)$$
98		simpl	$$⊢\left(I=J\wedge I=I\right)\to I=J$$
99	97 98	syl6bi	$$⊢\left(I\in V\wedge J\in W\right)\to \left(⟨I,I⟩=⟨J,I⟩\to I=J\right)$$
100	99	necon3d	$$⊢\left(I\in V\wedge J\in W\right)\to \left(I\ne J\to ⟨I,I⟩\ne ⟨J,I⟩\right)$$
101	100	com12	$$⊢I\ne J\to \left(\left(I\in V\wedge J\in W\right)\to ⟨I,I⟩\ne ⟨J,I⟩\right)$$
102	56 101	sylbir	$$⊢\neg I=J\to \left(\left(I\in V\wedge J\in W\right)\to ⟨I,I⟩\ne ⟨J,I⟩\right)$$
103	102	imp	$$⊢\left(\neg I=J\wedge \left(I\in V\wedge J\in W\right)\right)\to ⟨I,I⟩\ne ⟨J,I⟩$$
104	94 103	jca	$$⊢\left(\neg I=J\wedge \left(I\in V\wedge J\in W\right)\right)\to \left(⟨I,I⟩\ne ⟨I,J⟩\wedge ⟨I,I⟩\ne ⟨J,I⟩\right)$$
105	104	orcd	$$⊢\left(\neg I=J\wedge \left(I\in V\wedge J\in W\right)\right)\to \left(\left(⟨I,I⟩\ne ⟨I,J⟩\wedge ⟨I,I⟩\ne ⟨J,I⟩\right)\vee \left(⟨J,J⟩\ne ⟨I,J⟩\wedge ⟨J,J⟩\ne ⟨J,I⟩\right)\right)$$
106		prneimg	$$⊢\left(\left(⟨I,I⟩\in \mathrm{V}\wedge ⟨J,J⟩\in \mathrm{V}\right)\wedge \left(⟨I,J⟩\in \mathrm{V}\wedge ⟨J,I⟩\in \mathrm{V}\right)\right)\to \left(\left(\left(⟨I,I⟩\ne ⟨I,J⟩\wedge ⟨I,I⟩\ne ⟨J,I⟩\right)\vee \left(⟨J,J⟩\ne ⟨I,J⟩\wedge ⟨J,J⟩\ne ⟨J,I⟩\right)\right)\to \left\{⟨I,I⟩,⟨J,J⟩\right\}\ne \left\{⟨I,J⟩,⟨J,I⟩\right\}\right)$$
107	87 105 106	mpsyl	$$⊢\left(\neg I=J\wedge \left(I\in V\wedge J\in W\right)\right)\to \left\{⟨I,I⟩,⟨J,J⟩\right\}\ne \left\{⟨I,J⟩,⟨J,I⟩\right\}$$
108		hash2prd	$$⊢\left(B\in \mathrm{V}\wedge \left|B\right|=2\right)\to \left(\left(\left\{⟨I,I⟩,⟨J,J⟩\right\}\in B\wedge \left\{⟨I,J⟩,⟨J,I⟩\right\}\in B\wedge \left\{⟨I,I⟩,⟨J,J⟩\right\}\ne \left\{⟨I,J⟩,⟨J,I⟩\right\}\right)\to B=\left\{\left\{⟨I,I⟩,⟨J,J⟩\right\},\left\{⟨I,J⟩,⟨J,I⟩\right\}\right\}\right)$$
109	108	imp	$$⊢\left(\left(B\in \mathrm{V}\wedge \left|B\right|=2\right)\wedge \left(\left\{⟨I,I⟩,⟨J,J⟩\right\}\in B\wedge \left\{⟨I,J⟩,⟨J,I⟩\right\}\in B\wedge \left\{⟨I,I⟩,⟨J,J⟩\right\}\ne \left\{⟨I,J⟩,⟨J,I⟩\right\}\right)\right)\to B=\left\{\left\{⟨I,I⟩,⟨J,J⟩\right\},\left\{⟨I,J⟩,⟨J,I⟩\right\}\right\}$$
110	43 50 71 81 107 109	syl23anc	$$⊢\left(\neg I=J\wedge \left(I\in V\wedge J\in W\right)\right)\to B=\left\{\left\{⟨I,I⟩,⟨J,J⟩\right\},\left\{⟨I,J⟩,⟨J,I⟩\right\}\right\}$$
111	41 110	pm2.61ian	$$⊢\left(I\in V\wedge J\in W\right)\to B=\left\{\left\{⟨I,I⟩,⟨J,J⟩\right\},\left\{⟨I,J⟩,⟨J,I⟩\right\}\right\}$$