Theorem caoprmo 4056

Description: Uniqueness of inverse element in commutative, associative operation with identity. Remark in proof of Proposition 9-2.4 of [Gleason] p. 119.

Hypotheses

Ref	Expression
caoprmo.1	⊢ A ∈ V
caoprmo.2	⊢ B ∈ S
caoprmo.dom	⊢ dom F = (S × S)
caoprmo.3	⊢ ¬ ∅ ∈ S
caoprmo.com	⊢ (xFy) = (yFx)
caoprmo.ass	⊢ ((xFy)Fz) = (xF(yFz))
caoprmo.id	⊢ (x ∈ S → (xFB) = x)

Assertion

Ref	Expression
caoprmo	⊢ ∃*w(AFw) = B

Distinct variable groups:   x,y,z,F   x,S,y,z   x,A,y,z   x,B,y,z,w   w,S   w,A   w,B   w,F

Proof of Theorem caoprmo

Step	Hyp	Ref	Expression
1		eleq1 1526	. . . . 5 ⊢ (w = v → (w ∈ S ↔ v ∈ S))
2		opreq2 3954	. . . . . 6 ⊢ (w = v → (AFw) = (AFv))
3	2	eqeq1d 1475	. . . . 5 ⊢ (w = v → ((AFw) = B ↔ (AFv) = B))
4	1, 3	anbi12d 626	. . . 4 ⊢ (w = v → ((w ∈ S ⋀ (AFw) = B) ↔ (v ∈ S ⋀ (AFv) = B)))
5	4	mo4 1396	. . 3 ⊢ (∃*w(w ∈ S ⋀ (AFw) = B) ↔ ∀w∀v(((w ∈ S ⋀ (AFw) = B) ⋀ (v ∈ S ⋀ (AFv) = B)) → w = v))
6		opreq2 3954	. . . . . . . 8 ⊢ ((AFv) = B → (wF(AFv)) = (wFB))
7		opreq1 3953	. . . . . . . . . 10 ⊢ (x = w → (xFB) = (wFB))
8		id 59	. . . . . . . . . 10 ⊢ (x = w → x = w)
9	7, 8	eqeq12d 1481	. . . . . . . . 9 ⊢ (x = w → ((xFB) = x ↔ (wFB) = w))
10		caoprmo.id	. . . . . . . . 9 ⊢ (x ∈ S → (xFB) = x)
11	9, 10	vtoclga 1843	. . . . . . . 8 ⊢ (w ∈ S → (wFB) = w)
12	6, 11	sylan9eqr 1521	. . . . . . 7 ⊢ ((w ∈ S ⋀ (AFv) = B) → (wF(AFv)) = w)
13		caoprmo.1	. . . . . . . . 9 ⊢ A ∈ V
14		visset 1804	. . . . . . . . 9 ⊢ w ∈ V
15		visset 1804	. . . . . . . . 9 ⊢ v ∈ V
16		caoprmo.ass	. . . . . . . . 9 ⊢ ((xFy)Fz) = (xF(yFz))
17	13, 14, 15, 16	caoprass 4040	. . . . . . . 8 ⊢ ((AFw)Fv) = (AF(wFv))
18		caoprmo.com	. . . . . . . . 9 ⊢ (xFy) = (yFx)
19	13, 14, 15, 18, 16	caopr12 4047	. . . . . . . 8 ⊢ (AF(wFv)) = (wF(AFv))
20	17, 19	eqtr 1487	. . . . . . 7 ⊢ ((AFw)Fv) = (wF(AFv))
21	12, 20	syl5eq 1511	. . . . . 6 ⊢ ((w ∈ S ⋀ (AFv) = B) → ((AFw)Fv) = w)
22	21	ad2ant2rl 411	. . . . 5 ⊢ (((w ∈ S ⋀ (AFw) = B) ⋀ (v ∈ S ⋀ (AFv) = B)) → ((AFw)Fv) = w)
23		opreq1 3953	. . . . . . 7 ⊢ ((AFw) = B → ((AFw)Fv) = (BFv))
24		opreq1 3953	. . . . . . . . . 10 ⊢ (x = v → (xFB) = (vFB))
25		id 59	. . . . . . . . . 10 ⊢ (x = v → x = v)
26	24, 25	eqeq12d 1481	. . . . . . . . 9 ⊢ (x = v → ((xFB) = x ↔ (vFB) = v))
27	26, 10	vtoclga 1843	. . . . . . . 8 ⊢ (v ∈ S → (vFB) = v)
28		caoprmo.2	. . . . . . . . . 10 ⊢ B ∈ S
29	28	elisseti 1809	. . . . . . . . 9 ⊢ B ∈ V
30	29, 15, 18	caoprcom 4039	. . . . . . . 8 ⊢ (BFv) = (vFB)
31	27, 30	syl5eq 1511	. . . . . . 7 ⊢ (v ∈ S → (BFv) = v)
32	23, 31	sylan9eq 1519	. . . . . 6 ⊢ (((AFw) = B ⋀ v ∈ S) → ((AFw)Fv) = v)
33	32	ad2ant2lr 410	. . . . 5 ⊢ (((w ∈ S ⋀ (AFw) = B) ⋀ (v ∈ S ⋀ (AFv) = B)) → ((AFw)Fv) = v)
34	22, 33	eqtr3d 1501	. . . 4 ⊢ (((w ∈ S ⋀ (AFw) = B) ⋀ (v ∈ S ⋀ (AFv) = B)) → w = v)
35	34	ax-gen 960	. . 3 ⊢ ∀v(((w ∈ S ⋀ (AFw) = B) ⋀ (v ∈ S ⋀ (AFv) = B)) → w = v)
36	5, 35	mpgbir 985	. 2 ⊢ ∃*w(w ∈ S ⋀ (AFw) = B)
37		eleq1 1526	. . . . . 6 ⊢ ((AFw) = B → ((AFw) ∈ S ↔ B ∈ S))
38	28, 37	mpbiri 194	. . . . 5 ⊢ ((AFw) = B → (AFw) ∈ S)
39		caoprmo.dom	. . . . . . 7 ⊢ dom F = (S × S)
40		caoprmo.3	. . . . . . 7 ⊢ ¬ ∅ ∈ S
41	14, 39, 40	ndmoprrcl 4032	. . . . . 6 ⊢ ((AFw) ∈ S → (A ∈ S ⋀ w ∈ S))
42	41	pm3.27d 325	. . . . 5 ⊢ ((AFw) ∈ S → w ∈ S)
43	38, 42	syl 10	. . . 4 ⊢ ((AFw) = B → w ∈ S)
44	43	ancri 297	. . 3 ⊢ ((AFw) = B → (w ∈ S ⋀ (AFw) = B))
45	44	immoi 1411	. 2 ⊢ (∃*w(w ∈ S ⋀ (AFw) = B) → ∃*w(AFw) = B)
46	36, 45	ax-mp 7	1 ⊢ ∃*w(AFw) = B

Syntax hints:  ¬ wn 2   → wi 3   ⋀ wa 223  ∀wal 951   = wceq 953   ∈ wcel 955  ∃*wmo 1374  Vcvv 1802  ∅c0 2270   × cxp 3158  dom cdm 3160  (class class class)co 3948

This theorem is referenced by:  recmulpq 5042

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-pow 2732  ax-pr 2769

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 775  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-ral 1641  df-rex 1642  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-op 2406  df-uni 2494  df-br 2610  df-opab 2657  df-xp 3174  df-cnv 3176  df-dm 3178  df-rn 3179  df-res 3180  df-ima 3181  df-fv 3188  df-opr 3950

Copyright terms: Public domain