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	birani	$$⊢\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$$
25	20 24	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$$
26	25	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)$$
27	14 26	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)$$
28	27	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)$$
29	28	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$$
30		eqeq2	$$⊢y=a\to \left(l\underset{\dot{}}{+}w=y\leftrightarrow l\underset{\dot{}}{+}w=a\right)$$
31	30	rexbidv	$$⊢y=a\to \left(\exists l\in Bl\underset{\dot{}}{+}w=y\leftrightarrow \exists l\in Bl\underset{\dot{}}{+}w=a\right)$$
32		eqeq2	$$⊢y=a\to \left(w\underset{\dot{}}{+}r=y\leftrightarrow w\underset{\dot{}}{+}r=a\right)$$
33	32	rexbidv	$$⊢y=a\to \left(\exists r\in Bw\underset{\dot{}}{+}r=y\leftrightarrow \exists r\in Bw\underset{\dot{}}{+}r=a\right)$$
34	31 33	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)$$
35	12 34	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)$$
36	35	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$$
37	36	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)$$
38	37	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)$$
39	38	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$$
40	39	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$$
41		oveq2	$$⊢r=z\to w\underset{\dot{}}{+}r=w\underset{\dot{}}{+}z$$
42	41	eqeq1d	$$⊢r=z\to \left(w\underset{\dot{}}{+}r=a\leftrightarrow w\underset{\dot{}}{+}z=a\right)$$
43	42	cbvrexvw	$$⊢\exists r\in Bw\underset{\dot{}}{+}r=a\leftrightarrow \exists z\in Bw\underset{\dot{}}{+}z=a$$
44		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}$$
45	44	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}$$
46		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$$
47		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$$
48		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$$
49	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)$$
50	45 46 47 48 49	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)$$
51		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$$
52	51	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$$
53	50 52	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$$
54	53	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$$
55		oveq2	$$⊢w\underset{\dot{}}{+}z=a\to u\underset{\dot{}}{+}\left(w\underset{\dot{}}{+}z\right)=u\underset{\dot{}}{+}a$$
56		id	$$⊢w\underset{\dot{}}{+}z=a\to w\underset{\dot{}}{+}z=a$$
57	55 56	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)$$
58	54 57	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)$$
59	58	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)$$
60	43 59	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)$$
61	60	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)$$
62	40 61	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$$
63		oveq2	$$⊢x=a\to l\underset{\dot{}}{+}x=l\underset{\dot{}}{+}a$$
64	63	eqeq1d	$$⊢x=a\to \left(l\underset{\dot{}}{+}x=y\leftrightarrow l\underset{\dot{}}{+}a=y\right)$$
65	64	rexbidv	$$⊢x=a\to \left(\exists l\in Bl\underset{\dot{}}{+}x=y\leftrightarrow \exists l\in Bl\underset{\dot{}}{+}a=y\right)$$
66		oveq1	$$⊢x=a\to x\underset{\dot{}}{+}r=a\underset{\dot{}}{+}r$$
67	66	eqeq1d	$$⊢x=a\to \left(x\underset{\dot{}}{+}r=y\leftrightarrow a\underset{\dot{}}{+}r=y\right)$$
68	67	rexbidv	$$⊢x=a\to \left(\exists r\in Bx\underset{\dot{}}{+}r=y\leftrightarrow \exists r\in Ba\underset{\dot{}}{+}r=y\right)$$
69	65 68	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)$$
70		eqeq2	$$⊢y=u\to \left(l\underset{\dot{}}{+}a=y\leftrightarrow l\underset{\dot{}}{+}a=u\right)$$
71	70	rexbidv	$$⊢y=u\to \left(\exists l\in Bl\underset{\dot{}}{+}a=y\leftrightarrow \exists l\in Bl\underset{\dot{}}{+}a=u\right)$$
72		eqeq2	$$⊢y=u\to \left(a\underset{\dot{}}{+}r=y\leftrightarrow a\underset{\dot{}}{+}r=u\right)$$
73	72	rexbidv	$$⊢y=u\to \left(\exists r\in Ba\underset{\dot{}}{+}r=y\leftrightarrow \exists r\in Ba\underset{\dot{}}{+}r=u\right)$$
74	71 73	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)$$
75	69 74	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)$$
76	75	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$$
77	76	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)$$
78	77	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)$$
79	78	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)$$
80	79	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)$$
81	80	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$$
82		oveq1	$$⊢l=i\to l\underset{\dot{}}{+}a=i\underset{\dot{}}{+}a$$
83	82	eqeq1d	$$⊢l=i\to \left(l\underset{\dot{}}{+}a=u\leftrightarrow i\underset{\dot{}}{+}a=u\right)$$
84	83	cbvrexvw	$$⊢\exists l\in Bl\underset{\dot{}}{+}a=u\leftrightarrow \exists i\in Bi\underset{\dot{}}{+}a=u$$
85	81 84	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$$
86	85	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$$
87	86	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$$
88	62 87	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)$$
89	88	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)$$
90	89	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)$$
91	90	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)$$
92	29 91	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)$$
93	5 92	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)$$