Theorem caovmo

Description: Uniqueness of inverse element in commutative, associative operation with identity. Remark in proof of Proposition 9-2.4 of Gleason p. 119. (Contributed by NM, 4-Mar-1996)

	Ref	Expression
Hypotheses	caovmo.2	$$⊢B\in S$$
	caovmo.dom	$$⊢\mathrm{dom}F=S\times S$$
	caovmo.3	$$⊢\neg \varnothing \in S$$
	caovmo.com	$$⊢xFy=yFx$$
	caovmo.ass	$$⊢\left(xFy\right)Fz=xF\left(yFz\right)$$
	caovmo.id	$$⊢x\in S\to xFB=x$$
Assertion	caovmo	$$⊢{\exists }^{*}wAFw=B$$

Proof

Step	Hyp	Ref	Expression
1		caovmo.2	$$⊢B\in S$$
2		caovmo.dom	$$⊢\mathrm{dom}F=S\times S$$
3		caovmo.3	$$⊢\neg \varnothing \in S$$
4		caovmo.com	$$⊢xFy=yFx$$
5		caovmo.ass	$$⊢\left(xFy\right)Fz=xF\left(yFz\right)$$
6		caovmo.id	$$⊢x\in S\to xFB=x$$
7		oveq1	$$⊢u=A\to uFw=AFw$$
8	7	eqeq1d	$$⊢u=A\to \left(uFw=B\leftrightarrow AFw=B\right)$$
9	8	mobidv	$$⊢u=A\to \left({\exists }^{*}wuFw=B\leftrightarrow {\exists }^{*}wAFw=B\right)$$
10		oveq2	$$⊢w=v\to uFw=uFv$$
11	10	eqeq1d	$$⊢w=v\to \left(uFw=B\leftrightarrow uFv=B\right)$$
12	11	mo4	$$⊢{\exists }^{*}wuFw=B\leftrightarrow \forall w\forall v\left(\left(uFw=B\wedge uFv=B\right)\to w=v\right)$$
13		simpr	$$⊢\left(uFw=B\wedge uFv=B\right)\to uFv=B$$
14	13	oveq2d	$$⊢\left(uFw=B\wedge uFv=B\right)\to wF\left(uFv\right)=wFB$$
15		simpl	$$⊢\left(uFw=B\wedge uFv=B\right)\to uFw=B$$
16	15	oveq1d	$$⊢\left(uFw=B\wedge uFv=B\right)\to \left(uFw\right)Fv=BFv$$
17		vex	$$⊢u\in \mathrm{V}$$
18		vex	$$⊢w\in \mathrm{V}$$
19		vex	$$⊢v\in \mathrm{V}$$
20	17 18 19 5	caovass	$$⊢\left(uFw\right)Fv=uF\left(wFv\right)$$
21	17 18 19 4 5	caov12	$$⊢uF\left(wFv\right)=wF\left(uFv\right)$$
22	20 21	eqtri	$$⊢\left(uFw\right)Fv=wF\left(uFv\right)$$
23	1	elexi	$$⊢B\in \mathrm{V}$$
24	23 19 4	caovcom	$$⊢BFv=vFB$$
25	16 22 24	3eqtr3g	$$⊢\left(uFw=B\wedge uFv=B\right)\to wF\left(uFv\right)=vFB$$
26	14 25	eqtr3d	$$⊢\left(uFw=B\wedge uFv=B\right)\to wFB=vFB$$
27	15 1	eqeltrdi	$$⊢\left(uFw=B\wedge uFv=B\right)\to uFw\in S$$
28	2 3	ndmovrcl	$$⊢uFw\in S\to \left(u\in S\wedge w\in S\right)$$
29	27 28	syl	$$⊢\left(uFw=B\wedge uFv=B\right)\to \left(u\in S\wedge w\in S\right)$$
30		oveq1	$$⊢x=w\to xFB=wFB$$
31		id	$$⊢x=w\to x=w$$
32	30 31	eqeq12d	$$⊢x=w\to \left(xFB=x\leftrightarrow wFB=w\right)$$
33	32 6	vtoclga	$$⊢w\in S\to wFB=w$$
34	29 33	simpl2im	$$⊢\left(uFw=B\wedge uFv=B\right)\to wFB=w$$
35	13 1	eqeltrdi	$$⊢\left(uFw=B\wedge uFv=B\right)\to uFv\in S$$
36	2 3	ndmovrcl	$$⊢uFv\in S\to \left(u\in S\wedge v\in S\right)$$
37	35 36	syl	$$⊢\left(uFw=B\wedge uFv=B\right)\to \left(u\in S\wedge v\in S\right)$$
38		oveq1	$$⊢x=v\to xFB=vFB$$
39		id	$$⊢x=v\to x=v$$
40	38 39	eqeq12d	$$⊢x=v\to \left(xFB=x\leftrightarrow vFB=v\right)$$
41	40 6	vtoclga	$$⊢v\in S\to vFB=v$$
42	37 41	simpl2im	$$⊢\left(uFw=B\wedge uFv=B\right)\to vFB=v$$
43	26 34 42	3eqtr3d	$$⊢\left(uFw=B\wedge uFv=B\right)\to w=v$$
44	43	ax-gen	$$⊢\forall v\left(\left(uFw=B\wedge uFv=B\right)\to w=v\right)$$
45	12 44	mpgbir	$$⊢{\exists }^{*}wuFw=B$$
46	9 45	vtoclg	$$⊢A\in S\to {\exists }^{*}wAFw=B$$
47		moanimv	$$⊢{\exists }^{*}w\left(A\in S\wedge AFw=B\right)\leftrightarrow \left(A\in S\to {\exists }^{*}wAFw=B\right)$$
48	46 47	mpbir	$$⊢{\exists }^{*}w\left(A\in S\wedge AFw=B\right)$$
49		eleq1	$$⊢AFw=B\to \left(AFw\in S\leftrightarrow B\in S\right)$$
50	1 49	mpbiri	$$⊢AFw=B\to AFw\in S$$
51	2 3	ndmovrcl	$$⊢AFw\in S\to \left(A\in S\wedge w\in S\right)$$
52	50 51	syl	$$⊢AFw=B\to \left(A\in S\wedge w\in S\right)$$
53	52	simpld	$$⊢AFw=B\to A\in S$$
54	53	ancri	$$⊢AFw=B\to \left(A\in S\wedge AFw=B\right)$$
55	54	moimi	$$⊢{\exists }^{*}w\left(A\in S\wedge AFw=B\right)\to {\exists }^{*}wAFw=B$$
56	48 55	ax-mp	$$⊢{\exists }^{*}wAFw=B$$