Theorem dfgrp3lem

Description: Lemma for dfgrp3 . (Contributed by AV, 28-Aug-2021)

	Ref	Expression
Hypotheses	dfgrp3.b	$$⊢B={\mathrm{Base}}_G$$
	dfgrp3.p	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	dfgrp3lem	$$⊢\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\to \exists u\in B\forall a\in B\left(u\underset{\dot{}}{+}a=a\wedge \exists i\in Bi\underset{\dot{}}{+}a=u\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfgrp3.b	$$⊢B={\mathrm{Base}}_G$$
2		dfgrp3.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		simp2	$$⊢\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\to B\ne \varnothing$$
4		n0	$$⊢B\ne \varnothing \leftrightarrow \exists ww\in B$$
5	3 4	sylib	$$⊢\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\to \exists ww\in B$$
6		oveq2	$$⊢x=w\to l\underset{\dot{}}{+}x=l\underset{\dot{}}{+}w$$
7	6	eqeq1d	$$⊢x=w\to \left(l\underset{\dot{}}{+}x=y\leftrightarrow l\underset{\dot{}}{+}w=y\right)$$
8	7	rexbidv	$$⊢x=w\to \left(\exists l\in Bl\underset{\dot{}}{+}x=y\leftrightarrow \exists l\in Bl\underset{\dot{}}{+}w=y\right)$$
9		oveq1	$$⊢x=w\to x\underset{\dot{}}{+}r=w\underset{\dot{}}{+}r$$
10	9	eqeq1d	$$⊢x=w\to \left(x\underset{\dot{}}{+}r=y\leftrightarrow w\underset{\dot{}}{+}r=y\right)$$
11	10	rexbidv	$$⊢x=w\to \left(\exists r\in Bx\underset{\dot{}}{+}r=y\leftrightarrow \exists r\in Bw\underset{\dot{}}{+}r=y\right)$$
12	8 11	anbi12d	$$⊢x=w\to \left(\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\leftrightarrow \left(\exists l\in Bl\underset{\dot{}}{+}w=y\wedge \exists r\in Bw\underset{\dot{}}{+}r=y\right)\right)$$
13	12	ralbidv	$$⊢x=w\to \left(\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\leftrightarrow \forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}w=y\wedge \exists r\in Bw\underset{\dot{}}{+}r=y\right)\right)$$
14	13	rspcv	$$⊢w\in B\to \left(\forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\to \forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}w=y\wedge \exists r\in Bw\underset{\dot{}}{+}r=y\right)\right)$$
15		eqeq2	$$⊢y=w\to \left(l\underset{\dot{}}{+}w=y\leftrightarrow l\underset{\dot{}}{+}w=w\right)$$
16	15	rexbidv	$$⊢y=w\to \left(\exists l\in Bl\underset{\dot{}}{+}w=y\leftrightarrow \exists l\in Bl\underset{\dot{}}{+}w=w\right)$$
17		eqeq2	$$⊢y=w\to \left(w\underset{\dot{}}{+}r=y\leftrightarrow w\underset{\dot{}}{+}r=w\right)$$
18	17	rexbidv	$$⊢y=w\to \left(\exists r\in Bw\underset{\dot{}}{+}r=y\leftrightarrow \exists r\in Bw\underset{\dot{}}{+}r=w\right)$$
19	16 18	anbi12d	$$⊢y=w\to \left(\left(\exists l\in Bl\underset{\dot{}}{+}w=y\wedge \exists r\in Bw\underset{\dot{}}{+}r=y\right)\leftrightarrow \left(\exists l\in Bl\underset{\dot{}}{+}w=w\wedge \exists r\in Bw\underset{\dot{}}{+}r=w\right)\right)$$
20	19	rspcva	$$⊢\left(w\in B\wedge \forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}w=y\wedge \exists r\in Bw\underset{\dot{}}{+}r=y\right)\right)\to \left(\exists l\in Bl\underset{\dot{}}{+}w=w\wedge \exists r\in Bw\underset{\dot{}}{+}r=w\right)$$
21		oveq1	$$⊢l=u\to l\underset{\dot{}}{+}w=u\underset{\dot{}}{+}w$$
22	21	eqeq1d	$$⊢l=u\to \left(l\underset{\dot{}}{+}w=w\leftrightarrow u\underset{\dot{}}{+}w=w\right)$$
23	22	cbvrexvw	$$⊢\exists l\in Bl\underset{\dot{}}{+}w=w\leftrightarrow \exists u\in Bu\underset{\dot{}}{+}w=w$$
24	23	biimpi	$$⊢\exists l\in Bl\underset{\dot{}}{+}w=w\to \exists u\in Bu\underset{\dot{}}{+}w=w$$
25	24	adantr	$$⊢\left(\exists l\in Bl\underset{\dot{}}{+}w=w\wedge \exists r\in Bw\underset{\dot{}}{+}r=w\right)\to \exists u\in Bu\underset{\dot{}}{+}w=w$$
26	20 25	syl	$$⊢\left(w\in B\wedge \forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}w=y\wedge \exists r\in Bw\underset{\dot{}}{+}r=y\right)\right)\to \exists u\in Bu\underset{\dot{}}{+}w=w$$
27	26	ex	$$⊢w\in B\to \left(\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}w=y\wedge \exists r\in Bw\underset{\dot{}}{+}r=y\right)\to \exists u\in Bu\underset{\dot{}}{+}w=w\right)$$
28	14 27	syldc	$$⊢\forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\to \left(w\in B\to \exists u\in Bu\underset{\dot{}}{+}w=w\right)$$
29	28	3ad2ant3	$$⊢\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\to \left(w\in B\to \exists u\in Bu\underset{\dot{}}{+}w=w\right)$$
30	29	imp	$$⊢\left(\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\wedge w\in B\right)\to \exists u\in Bu\underset{\dot{}}{+}w=w$$
31		eqeq2	$$⊢y=a\to \left(l\underset{\dot{}}{+}w=y\leftrightarrow l\underset{\dot{}}{+}w=a\right)$$
32	31	rexbidv	$$⊢y=a\to \left(\exists l\in Bl\underset{\dot{}}{+}w=y\leftrightarrow \exists l\in Bl\underset{\dot{}}{+}w=a\right)$$
33		eqeq2	$$⊢y=a\to \left(w\underset{\dot{}}{+}r=y\leftrightarrow w\underset{\dot{}}{+}r=a\right)$$
34	33	rexbidv	$$⊢y=a\to \left(\exists r\in Bw\underset{\dot{}}{+}r=y\leftrightarrow \exists r\in Bw\underset{\dot{}}{+}r=a\right)$$
35	32 34	anbi12d	$$⊢y=a\to \left(\left(\exists l\in Bl\underset{\dot{}}{+}w=y\wedge \exists r\in Bw\underset{\dot{}}{+}r=y\right)\leftrightarrow \left(\exists l\in Bl\underset{\dot{}}{+}w=a\wedge \exists r\in Bw\underset{\dot{}}{+}r=a\right)\right)$$
36	12 35	rspc2va	$$⊢\left(\left(w\in B\wedge a\in B\right)\wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\to \left(\exists l\in Bl\underset{\dot{}}{+}w=a\wedge \exists r\in Bw\underset{\dot{}}{+}r=a\right)$$
37	36	simprd	$$⊢\left(\left(w\in B\wedge a\in B\right)\wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\to \exists r\in Bw\underset{\dot{}}{+}r=a$$
38	37	expcom	$$⊢\forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\to \left(\left(w\in B\wedge a\in B\right)\to \exists r\in Bw\underset{\dot{}}{+}r=a\right)$$
39	38	3ad2ant3	$$⊢\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\to \left(\left(w\in B\wedge a\in B\right)\to \exists r\in Bw\underset{\dot{}}{+}r=a\right)$$
40	39	impl	$$⊢\left(\left(\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\wedge w\in B\right)\wedge a\in B\right)\to \exists r\in Bw\underset{\dot{}}{+}r=a$$
41	40	ad2ant2r	$$⊢\left(\left(\left(\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\wedge w\in B\right)\wedge u\in B\right)\wedge \left(a\in B\wedge u\underset{\dot{}}{+}w=w\right)\right)\to \exists r\in Bw\underset{\dot{}}{+}r=a$$
42		oveq2	$$⊢r=z\to w\underset{\dot{}}{+}r=w\underset{\dot{}}{+}z$$
43	42	eqeq1d	$$⊢r=z\to \left(w\underset{\dot{}}{+}r=a\leftrightarrow w\underset{\dot{}}{+}z=a\right)$$
44	43	cbvrexvw	$$⊢\exists r\in Bw\underset{\dot{}}{+}r=a\leftrightarrow \exists z\in Bw\underset{\dot{}}{+}z=a$$
45		simpll1	$$⊢\left(\left(\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\wedge w\in B\right)\wedge u\in B\right)\to G\in \mathrm{Smgrp}$$
46	45	adantr	$$⊢\left(\left(\left(\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\wedge w\in B\right)\wedge u\in B\right)\wedge \left(u\underset{\dot{}}{+}w=w\wedge z\in B\right)\right)\to G\in \mathrm{Smgrp}$$
47		simplr	$$⊢\left(\left(\left(\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\wedge w\in B\right)\wedge u\in B\right)\wedge \left(u\underset{\dot{}}{+}w=w\wedge z\in B\right)\right)\to u\in B$$
48		simpllr	$$⊢\left(\left(\left(\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\wedge w\in B\right)\wedge u\in B\right)\wedge \left(u\underset{\dot{}}{+}w=w\wedge z\in B\right)\right)\to w\in B$$
49		simprr	$$⊢\left(\left(\left(\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\wedge w\in B\right)\wedge u\in B\right)\wedge \left(u\underset{\dot{}}{+}w=w\wedge z\in B\right)\right)\to z\in B$$
50	1 2	sgrpass	$$⊢\left(G\in \mathrm{Smgrp}\wedge \left(u\in B\wedge w\in B\wedge z\in B\right)\right)\to \left(u\underset{\dot{}}{+}w\right)\underset{\dot{}}{+}z=u\underset{\dot{}}{+}\left(w\underset{\dot{}}{+}z\right)$$
51	46 47 48 49 50	syl13anc	$$⊢\left(\left(\left(\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\wedge w\in B\right)\wedge u\in B\right)\wedge \left(u\underset{\dot{}}{+}w=w\wedge z\in B\right)\right)\to \left(u\underset{\dot{}}{+}w\right)\underset{\dot{}}{+}z=u\underset{\dot{}}{+}\left(w\underset{\dot{}}{+}z\right)$$
52		simprl	$$⊢\left(\left(\left(\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\wedge w\in B\right)\wedge u\in B\right)\wedge \left(u\underset{\dot{}}{+}w=w\wedge z\in B\right)\right)\to u\underset{\dot{}}{+}w=w$$
53	52	oveq1d	$$⊢\left(\left(\left(\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\wedge w\in B\right)\wedge u\in B\right)\wedge \left(u\underset{\dot{}}{+}w=w\wedge z\in B\right)\right)\to \left(u\underset{\dot{}}{+}w\right)\underset{\dot{}}{+}z=w\underset{\dot{}}{+}z$$
54	51 53	eqtr3d	$$⊢\left(\left(\left(\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\wedge w\in B\right)\wedge u\in B\right)\wedge \left(u\underset{\dot{}}{+}w=w\wedge z\in B\right)\right)\to u\underset{\dot{}}{+}\left(w\underset{\dot{}}{+}z\right)=w\underset{\dot{}}{+}z$$
55	54	anassrs	$$⊢\left(\left(\left(\left(\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\wedge w\in B\right)\wedge u\in B\right)\wedge u\underset{\dot{}}{+}w=w\right)\wedge z\in B\right)\to u\underset{\dot{}}{+}\left(w\underset{\dot{}}{+}z\right)=w\underset{\dot{}}{+}z$$
56		oveq2	$$⊢w\underset{\dot{}}{+}z=a\to u\underset{\dot{}}{+}\left(w\underset{\dot{}}{+}z\right)=u\underset{\dot{}}{+}a$$
57		id	$$⊢w\underset{\dot{}}{+}z=a\to w\underset{\dot{}}{+}z=a$$
58	56 57	eqeq12d	$$⊢w\underset{\dot{}}{+}z=a\to \left(u\underset{\dot{}}{+}\left(w\underset{\dot{}}{+}z\right)=w\underset{\dot{}}{+}z\leftrightarrow u\underset{\dot{}}{+}a=a\right)$$
59	55 58	syl5ibcom	$$⊢\left(\left(\left(\left(\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\wedge w\in B\right)\wedge u\in B\right)\wedge u\underset{\dot{}}{+}w=w\right)\wedge z\in B\right)\to \left(w\underset{\dot{}}{+}z=a\to u\underset{\dot{}}{+}a=a\right)$$
60	59	rexlimdva	$$⊢\left(\left(\left(\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\wedge w\in B\right)\wedge u\in B\right)\wedge u\underset{\dot{}}{+}w=w\right)\to \left(\exists z\in Bw\underset{\dot{}}{+}z=a\to u\underset{\dot{}}{+}a=a\right)$$
61	44 60	biimtrid	$$⊢\left(\left(\left(\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\wedge w\in B\right)\wedge u\in B\right)\wedge u\underset{\dot{}}{+}w=w\right)\to \left(\exists r\in Bw\underset{\dot{}}{+}r=a\to u\underset{\dot{}}{+}a=a\right)$$
62	61	adantrl	$$⊢\left(\left(\left(\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\wedge w\in B\right)\wedge u\in B\right)\wedge \left(a\in B\wedge u\underset{\dot{}}{+}w=w\right)\right)\to \left(\exists r\in Bw\underset{\dot{}}{+}r=a\to u\underset{\dot{}}{+}a=a\right)$$
63	41 62	mpd	$$⊢\left(\left(\left(\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\wedge w\in B\right)\wedge u\in B\right)\wedge \left(a\in B\wedge u\underset{\dot{}}{+}w=w\right)\right)\to u\underset{\dot{}}{+}a=a$$
64		oveq2	$$⊢x=a\to l\underset{\dot{}}{+}x=l\underset{\dot{}}{+}a$$
65	64	eqeq1d	$$⊢x=a\to \left(l\underset{\dot{}}{+}x=y\leftrightarrow l\underset{\dot{}}{+}a=y\right)$$
66	65	rexbidv	$$⊢x=a\to \left(\exists l\in Bl\underset{\dot{}}{+}x=y\leftrightarrow \exists l\in Bl\underset{\dot{}}{+}a=y\right)$$
67		oveq1	$$⊢x=a\to x\underset{\dot{}}{+}r=a\underset{\dot{}}{+}r$$
68	67	eqeq1d	$$⊢x=a\to \left(x\underset{\dot{}}{+}r=y\leftrightarrow a\underset{\dot{}}{+}r=y\right)$$
69	68	rexbidv	$$⊢x=a\to \left(\exists r\in Bx\underset{\dot{}}{+}r=y\leftrightarrow \exists r\in Ba\underset{\dot{}}{+}r=y\right)$$
70	66 69	anbi12d	$$⊢x=a\to \left(\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\leftrightarrow \left(\exists l\in Bl\underset{\dot{}}{+}a=y\wedge \exists r\in Ba\underset{\dot{}}{+}r=y\right)\right)$$
71		eqeq2	$$⊢y=u\to \left(l\underset{\dot{}}{+}a=y\leftrightarrow l\underset{\dot{}}{+}a=u\right)$$
72	71	rexbidv	$$⊢y=u\to \left(\exists l\in Bl\underset{\dot{}}{+}a=y\leftrightarrow \exists l\in Bl\underset{\dot{}}{+}a=u\right)$$
73		eqeq2	$$⊢y=u\to \left(a\underset{\dot{}}{+}r=y\leftrightarrow a\underset{\dot{}}{+}r=u\right)$$
74	73	rexbidv	$$⊢y=u\to \left(\exists r\in Ba\underset{\dot{}}{+}r=y\leftrightarrow \exists r\in Ba\underset{\dot{}}{+}r=u\right)$$
75	72 74	anbi12d	$$⊢y=u\to \left(\left(\exists l\in Bl\underset{\dot{}}{+}a=y\wedge \exists r\in Ba\underset{\dot{}}{+}r=y\right)\leftrightarrow \left(\exists l\in Bl\underset{\dot{}}{+}a=u\wedge \exists r\in Ba\underset{\dot{}}{+}r=u\right)\right)$$
76	70 75	rspc2va	$$⊢\left(\left(a\in B\wedge u\in B\right)\wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\to \left(\exists l\in Bl\underset{\dot{}}{+}a=u\wedge \exists r\in Ba\underset{\dot{}}{+}r=u\right)$$
77	76	simpld	$$⊢\left(\left(a\in B\wedge u\in B\right)\wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\to \exists l\in Bl\underset{\dot{}}{+}a=u$$
78	77	ex	$$⊢\left(a\in B\wedge u\in B\right)\to \left(\forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\to \exists l\in Bl\underset{\dot{}}{+}a=u\right)$$
79	78	ancoms	$$⊢\left(u\in B\wedge a\in B\right)\to \left(\forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\to \exists l\in Bl\underset{\dot{}}{+}a=u\right)$$
80	79	com12	$$⊢\forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\to \left(\left(u\in B\wedge a\in B\right)\to \exists l\in Bl\underset{\dot{}}{+}a=u\right)$$
81	80	3ad2ant3	$$⊢\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\to \left(\left(u\in B\wedge a\in B\right)\to \exists l\in Bl\underset{\dot{}}{+}a=u\right)$$
82	81	impl	$$⊢\left(\left(\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\wedge u\in B\right)\wedge a\in B\right)\to \exists l\in Bl\underset{\dot{}}{+}a=u$$
83		oveq1	$$⊢l=i\to l\underset{\dot{}}{+}a=i\underset{\dot{}}{+}a$$
84	83	eqeq1d	$$⊢l=i\to \left(l\underset{\dot{}}{+}a=u\leftrightarrow i\underset{\dot{}}{+}a=u\right)$$
85	84	cbvrexvw	$$⊢\exists l\in Bl\underset{\dot{}}{+}a=u\leftrightarrow \exists i\in Bi\underset{\dot{}}{+}a=u$$
86	82 85	sylib	$$⊢\left(\left(\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\wedge u\in B\right)\wedge a\in B\right)\to \exists i\in Bi\underset{\dot{}}{+}a=u$$
87	86	adantllr	$$⊢\left(\left(\left(\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\wedge w\in B\right)\wedge u\in B\right)\wedge a\in B\right)\to \exists i\in Bi\underset{\dot{}}{+}a=u$$
88	87	adantrr	$$⊢\left(\left(\left(\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\wedge w\in B\right)\wedge u\in B\right)\wedge \left(a\in B\wedge u\underset{\dot{}}{+}w=w\right)\right)\to \exists i\in Bi\underset{\dot{}}{+}a=u$$
89	63 88	jca	$$⊢\left(\left(\left(\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\wedge w\in B\right)\wedge u\in B\right)\wedge \left(a\in B\wedge u\underset{\dot{}}{+}w=w\right)\right)\to \left(u\underset{\dot{}}{+}a=a\wedge \exists i\in Bi\underset{\dot{}}{+}a=u\right)$$
90	89	expr	$$⊢\left(\left(\left(\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\wedge w\in B\right)\wedge u\in B\right)\wedge a\in B\right)\to \left(u\underset{\dot{}}{+}w=w\to \left(u\underset{\dot{}}{+}a=a\wedge \exists i\in Bi\underset{\dot{}}{+}a=u\right)\right)$$
91	90	ralrimdva	$$⊢\left(\left(\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\wedge w\in B\right)\wedge u\in B\right)\to \left(u\underset{\dot{}}{+}w=w\to \forall a\in B\left(u\underset{\dot{}}{+}a=a\wedge \exists i\in Bi\underset{\dot{}}{+}a=u\right)\right)$$
92	91	reximdva	$$⊢\left(\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\wedge w\in B\right)\to \left(\exists u\in Bu\underset{\dot{}}{+}w=w\to \exists u\in B\forall a\in B\left(u\underset{\dot{}}{+}a=a\wedge \exists i\in Bi\underset{\dot{}}{+}a=u\right)\right)$$
93	30 92	mpd	$$⊢\left(\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\wedge w\in B\right)\to \exists u\in B\forall a\in B\left(u\underset{\dot{}}{+}a=a\wedge \exists i\in Bi\underset{\dot{}}{+}a=u\right)$$
94	5 93	exlimddv	$$⊢\left(G\in \mathrm{Smgrp}\wedge B\ne \varnothing \wedge \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)\right)\to \exists u\in B\forall a\in B\left(u\underset{\dot{}}{+}a=a\wedge \exists i\in Bi\underset{\dot{}}{+}a=u\right)$$