Theorem grposnOLD

Description: The group operation for the singleton group. Obsolete, use grp1 . instead. (Contributed by NM, 4-Nov-2006) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	grposnOLD.1	$$⊢A\in \mathrm{V}$$
Assertion	grposnOLD	$$⊢\left\{⟨⟨A,A⟩,A⟩\right\}\in \mathrm{GrpOp}$$

Proof

Step	Hyp	Ref	Expression
1		grposnOLD.1	$$⊢A\in \mathrm{V}$$
2		snex	$$⊢\left\{A\right\}\in \mathrm{V}$$
3		opex	$$⊢⟨A,A⟩\in \mathrm{V}$$
4	3 1	f1osn	$$⊢\left\{⟨⟨A,A⟩,A⟩\right\}:\left\{⟨A,A⟩\right\}\underset{1-1\; onto}{⟶}\left\{A\right\}$$
5		f1of	$$⊢\left\{⟨⟨A,A⟩,A⟩\right\}:\left\{⟨A,A⟩\right\}\underset{1-1\; onto}{⟶}\left\{A\right\}\to \left\{⟨⟨A,A⟩,A⟩\right\}:\left\{⟨A,A⟩\right\}⟶\left\{A\right\}$$
6	4 5	ax-mp	$$⊢\left\{⟨⟨A,A⟩,A⟩\right\}:\left\{⟨A,A⟩\right\}⟶\left\{A\right\}$$
7	1 1	xpsn	$$⊢\left\{A\right\}\times \left\{A\right\}=\left\{⟨A,A⟩\right\}$$
8	7	feq2i	$$⊢\left\{⟨⟨A,A⟩,A⟩\right\}:\left\{A\right\}\times \left\{A\right\}⟶\left\{A\right\}\leftrightarrow \left\{⟨⟨A,A⟩,A⟩\right\}:\left\{⟨A,A⟩\right\}⟶\left\{A\right\}$$
9	6 8	mpbir	$$⊢\left\{⟨⟨A,A⟩,A⟩\right\}:\left\{A\right\}\times \left\{A\right\}⟶\left\{A\right\}$$
10		velsn	$$⊢x\in \left\{A\right\}\leftrightarrow x=A$$
11		velsn	$$⊢y\in \left\{A\right\}\leftrightarrow y=A$$
12		velsn	$$⊢z\in \left\{A\right\}\leftrightarrow z=A$$
13		oveq2	$$⊢z=A\to \left(x\left\{⟨⟨A,A⟩,A⟩\right\}y\right)\left\{⟨⟨A,A⟩,A⟩\right\}z=\left(x\left\{⟨⟨A,A⟩,A⟩\right\}y\right)\left\{⟨⟨A,A⟩,A⟩\right\}A$$
14		oveq1	$$⊢x=A\to x\left\{⟨⟨A,A⟩,A⟩\right\}y=A\left\{⟨⟨A,A⟩,A⟩\right\}y$$
15		oveq2	$$⊢y=A\to A\left\{⟨⟨A,A⟩,A⟩\right\}y=A\left\{⟨⟨A,A⟩,A⟩\right\}A$$
16		df-ov	$$⊢A\left\{⟨⟨A,A⟩,A⟩\right\}A=\left\{⟨⟨A,A⟩,A⟩\right\}\left(⟨A,A⟩\right)$$
17	3 1	fvsn	$$⊢\left\{⟨⟨A,A⟩,A⟩\right\}\left(⟨A,A⟩\right)=A$$
18	16 17	eqtri	$$⊢A\left\{⟨⟨A,A⟩,A⟩\right\}A=A$$
19	15 18	eqtrdi	$$⊢y=A\to A\left\{⟨⟨A,A⟩,A⟩\right\}y=A$$
20	14 19	sylan9eq	$$⊢\left(x=A\wedge y=A\right)\to x\left\{⟨⟨A,A⟩,A⟩\right\}y=A$$
21	20	oveq1d	$$⊢\left(x=A\wedge y=A\right)\to \left(x\left\{⟨⟨A,A⟩,A⟩\right\}y\right)\left\{⟨⟨A,A⟩,A⟩\right\}A=A\left\{⟨⟨A,A⟩,A⟩\right\}A$$
22	21 18	eqtrdi	$$⊢\left(x=A\wedge y=A\right)\to \left(x\left\{⟨⟨A,A⟩,A⟩\right\}y\right)\left\{⟨⟨A,A⟩,A⟩\right\}A=A$$
23	13 22	sylan9eqr	$$⊢\left(\left(x=A\wedge y=A\right)\wedge z=A\right)\to \left(x\left\{⟨⟨A,A⟩,A⟩\right\}y\right)\left\{⟨⟨A,A⟩,A⟩\right\}z=A$$
24	23	3impa	$$⊢\left(x=A\wedge y=A\wedge z=A\right)\to \left(x\left\{⟨⟨A,A⟩,A⟩\right\}y\right)\left\{⟨⟨A,A⟩,A⟩\right\}z=A$$
25		oveq1	$$⊢x=A\to x\left\{⟨⟨A,A⟩,A⟩\right\}\left(y\left\{⟨⟨A,A⟩,A⟩\right\}z\right)=A\left\{⟨⟨A,A⟩,A⟩\right\}\left(y\left\{⟨⟨A,A⟩,A⟩\right\}z\right)$$
26		oveq1	$$⊢y=A\to y\left\{⟨⟨A,A⟩,A⟩\right\}z=A\left\{⟨⟨A,A⟩,A⟩\right\}z$$
27		oveq2	$$⊢z=A\to A\left\{⟨⟨A,A⟩,A⟩\right\}z=A\left\{⟨⟨A,A⟩,A⟩\right\}A$$
28	27 18	eqtrdi	$$⊢z=A\to A\left\{⟨⟨A,A⟩,A⟩\right\}z=A$$
29	26 28	sylan9eq	$$⊢\left(y=A\wedge z=A\right)\to y\left\{⟨⟨A,A⟩,A⟩\right\}z=A$$
30	29	oveq2d	$$⊢\left(y=A\wedge z=A\right)\to A\left\{⟨⟨A,A⟩,A⟩\right\}\left(y\left\{⟨⟨A,A⟩,A⟩\right\}z\right)=A\left\{⟨⟨A,A⟩,A⟩\right\}A$$
31	30 18	eqtrdi	$$⊢\left(y=A\wedge z=A\right)\to A\left\{⟨⟨A,A⟩,A⟩\right\}\left(y\left\{⟨⟨A,A⟩,A⟩\right\}z\right)=A$$
32	25 31	sylan9eq	$$⊢\left(x=A\wedge \left(y=A\wedge z=A\right)\right)\to x\left\{⟨⟨A,A⟩,A⟩\right\}\left(y\left\{⟨⟨A,A⟩,A⟩\right\}z\right)=A$$
33	32	3impb	$$⊢\left(x=A\wedge y=A\wedge z=A\right)\to x\left\{⟨⟨A,A⟩,A⟩\right\}\left(y\left\{⟨⟨A,A⟩,A⟩\right\}z\right)=A$$
34	24 33	eqtr4d	$$⊢\left(x=A\wedge y=A\wedge z=A\right)\to \left(x\left\{⟨⟨A,A⟩,A⟩\right\}y\right)\left\{⟨⟨A,A⟩,A⟩\right\}z=x\left\{⟨⟨A,A⟩,A⟩\right\}\left(y\left\{⟨⟨A,A⟩,A⟩\right\}z\right)$$
35	10 11 12 34	syl3anb	$$⊢\left(x\in \left\{A\right\}\wedge y\in \left\{A\right\}\wedge z\in \left\{A\right\}\right)\to \left(x\left\{⟨⟨A,A⟩,A⟩\right\}y\right)\left\{⟨⟨A,A⟩,A⟩\right\}z=x\left\{⟨⟨A,A⟩,A⟩\right\}\left(y\left\{⟨⟨A,A⟩,A⟩\right\}z\right)$$
36	1	snid	$$⊢A\in \left\{A\right\}$$
37		oveq2	$$⊢x=A\to A\left\{⟨⟨A,A⟩,A⟩\right\}x=A\left\{⟨⟨A,A⟩,A⟩\right\}A$$
38	37 18	eqtrdi	$$⊢x=A\to A\left\{⟨⟨A,A⟩,A⟩\right\}x=A$$
39		id	$$⊢x=A\to x=A$$
40	38 39	eqtr4d	$$⊢x=A\to A\left\{⟨⟨A,A⟩,A⟩\right\}x=x$$
41	10 40	sylbi	$$⊢x\in \left\{A\right\}\to A\left\{⟨⟨A,A⟩,A⟩\right\}x=x$$
42	36	a1i	$$⊢x\in \left\{A\right\}\to A\in \left\{A\right\}$$
43	10 38	sylbi	$$⊢x\in \left\{A\right\}\to A\left\{⟨⟨A,A⟩,A⟩\right\}x=A$$
44	2 9 35 36 41 42 43	isgrpoi	$$⊢\left\{⟨⟨A,A⟩,A⟩\right\}\in \mathrm{GrpOp}$$