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 = SymGrp (A)$
	symg1bas.2	$⊢ B = {Base}_{G}$
	symg2bas.0	$⊢ A = \{I, J\}$
Assertion	symg2bas	$⊢ (I \in V \land J \in W) \to B = \{\{⟨I, I⟩, ⟨J, J⟩\}, \{⟨I, J⟩, ⟨J, I⟩\}\}$

Proof

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

Metamath Proof Explorer

Theorem symg2bas

Proof