Theorem grpoidinvlem3 28769

Description: Lemma for grpoidinv 28771. (Contributed by NM, 11-Oct-2006.) (New usage is discouraged.)

Hypotheses

Ref	Expression
grpfo.1	⊢ 𝑋 = ran 𝐺
grpidinvlem3.2	⊢ (𝜑 ↔ ∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥)
grpidinvlem3.3	⊢ (𝜓 ↔ ∀𝑥 ∈ 𝑋 ∃𝑧 ∈ 𝑋 (𝑧𝐺𝑥) = 𝑈)

Assertion

Ref	Expression
grpoidinvlem3	⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈))

Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝑥,𝐺,𝑦,𝑧   𝑥,𝑋,𝑦,𝑧   𝑦,𝑈,𝑥,𝑧   𝜑,𝑦   𝜓,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑧)   𝜓(𝑥,𝑧)

Proof of Theorem grpoidinvlem3

Dummy variable 𝑤 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		grpidinvlem3.3	. . . . . 6 ⊢ (𝜓 ↔ ∀𝑥 ∈ 𝑋 ∃𝑧 ∈ 𝑋 (𝑧𝐺𝑥) = 𝑈)
2		oveq1 7262	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧𝐺𝑥) = (𝑦𝐺𝑥))
3	2	eqeq1d 2740	. . . . . . . 8 ⊢ (𝑧 = 𝑦 → ((𝑧𝐺𝑥) = 𝑈 ↔ (𝑦𝐺𝑥) = 𝑈))
4	3	cbvrexvw 3373	. . . . . . 7 ⊢ (∃𝑧 ∈ 𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈)
5	4	ralbii 3090	. . . . . 6 ⊢ (∀𝑥 ∈ 𝑋 ∃𝑧 ∈ 𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈)
6	1, 5	bitri 274	. . . . 5 ⊢ (𝜓 ↔ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈)
7		oveq2 7263	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑦𝐺𝑥) = (𝑦𝐺𝐴))
8	7	eqeq1d 2740	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((𝑦𝐺𝑥) = 𝑈 ↔ (𝑦𝐺𝐴) = 𝑈))
9	8	rexbidv 3225	. . . . . 6 ⊢ (𝑥 = 𝐴 → (∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈 ↔ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈))
10	9	rspccva 3551	. . . . 5 ⊢ ((∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈 ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈)
11	6, 10	sylanb 580	. . . 4 ⊢ ((𝜓 ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈)
12	11	adantll 710	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈)
13	12	adantll 710	. 2 ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈)
14		grpfo.1	. . . . . . . . . . . 12 ⊢ 𝑋 = ran 𝐺
15	14	grpocl 28763	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
16	15	3expa 1116	. . . . . . . . . 10 ⊢ (((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
17	16	adantllr 715	. . . . . . . . 9 ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
18	17	adantllr 715	. . . . . . . 8 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
19		grpidinvlem3.2	. . . . . . . . . . 11 ⊢ (𝜑 ↔ ∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥)
20	19	biimpi 215	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥)
21	20	ad2antrl 724	. . . . . . . . 9 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) → ∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥)
22	21	ad2antrr 722	. . . . . . . 8 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥)
23		oveq2 7263	. . . . . . . . . 10 ⊢ (𝑥 = (𝐴𝐺𝑦) → (𝑈𝐺𝑥) = (𝑈𝐺(𝐴𝐺𝑦)))
24		id 22	. . . . . . . . . 10 ⊢ (𝑥 = (𝐴𝐺𝑦) → 𝑥 = (𝐴𝐺𝑦))
25	23, 24	eqeq12d 2754	. . . . . . . . 9 ⊢ (𝑥 = (𝐴𝐺𝑦) → ((𝑈𝐺𝑥) = 𝑥 ↔ (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦)))
26	25	rspcva 3550	. . . . . . . 8 ⊢ (((𝐴𝐺𝑦) ∈ 𝑋 ∧ ∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥) → (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
27	18, 22, 26	syl2anc 583	. . . . . . 7 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
28	27	adantr 480	. . . . . 6 ⊢ ((((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
29		pm3.22 459	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐺 ∈ GrpOp) → (𝐺 ∈ GrpOp ∧ (𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)))
30	29	an31s 650	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝐺 ∈ GrpOp ∧ (𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)))
31	30	adantllr 715	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝐺 ∈ GrpOp ∧ (𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)))
32	31	adantllr 715	. . . . . . . . 9 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝐺 ∈ GrpOp ∧ (𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)))
33	32	adantr 480	. . . . . . . 8 ⊢ ((((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝐺 ∈ GrpOp ∧ (𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)))
34		oveq2 7263	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑈𝐺𝑥) = (𝑈𝐺𝑦))
35		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦)
36	34, 35	eqeq12d 2754	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((𝑈𝐺𝑥) = 𝑥 ↔ (𝑈𝐺𝑦) = 𝑦))
37	36	rspccva 3551	. . . . . . . . . . . . 13 ⊢ ((∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥 ∧ 𝑦 ∈ 𝑋) → (𝑈𝐺𝑦) = 𝑦)
38	19, 37	sylanb 580	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑈𝐺𝑦) = 𝑦)
39	38	adantlr 711	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑦 ∈ 𝑋) → (𝑈𝐺𝑦) = 𝑦)
40	39	adantlr 711	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑈𝐺𝑦) = 𝑦)
41	40	adantlll 714	. . . . . . . . 9 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑈𝐺𝑦) = 𝑦)
42	41	anim1i 614	. . . . . . . 8 ⊢ ((((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → ((𝑈𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝐴) = 𝑈))
43	14	grpoidinvlem2 28768	. . . . . . . 8 ⊢ (((𝐺 ∈ GrpOp ∧ (𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) ∧ ((𝑈𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝐴) = 𝑈)) → ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
44	33, 42, 43	syl2anc 583	. . . . . . 7 ⊢ ((((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
45	15	3expb 1118	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝐴𝐺𝑦) ∈ 𝑋)
46	45	ad2ant2rl 745	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) → (𝐴𝐺𝑦) ∈ 𝑋)
47		oveq1 7262	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑤 → (𝑧𝐺𝑥) = (𝑤𝐺𝑥))
48	47	eqeq1d 2740	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑤 → ((𝑧𝐺𝑥) = 𝑈 ↔ (𝑤𝐺𝑥) = 𝑈))
49	48	cbvrexvw 3373	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑧 ∈ 𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∃𝑤 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑈)
50	49	ralbii 3090	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑥 ∈ 𝑋 ∃𝑧 ∈ 𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∀𝑥 ∈ 𝑋 ∃𝑤 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑈)
51	1, 50	bitri 274	. . . . . . . . . . . . . . 15 ⊢ (𝜓 ↔ ∀𝑥 ∈ 𝑋 ∃𝑤 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑈)
52		oveq2 7263	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝐴𝐺𝑦) → (𝑤𝐺𝑥) = (𝑤𝐺(𝐴𝐺𝑦)))
53	52	eqeq1d 2740	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝐴𝐺𝑦) → ((𝑤𝐺𝑥) = 𝑈 ↔ (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈))
54	53	rexbidv 3225	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝐴𝐺𝑦) → (∃𝑤 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑈 ↔ ∃𝑤 ∈ 𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈))
55	54	rspcva 3550	. . . . . . . . . . . . . . 15 ⊢ (((𝐴𝐺𝑦) ∈ 𝑋 ∧ ∀𝑥 ∈ 𝑋 ∃𝑤 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑈) → ∃𝑤 ∈ 𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈)
56	51, 55	sylan2b 593	. . . . . . . . . . . . . 14 ⊢ (((𝐴𝐺𝑦) ∈ 𝑋 ∧ 𝜓) → ∃𝑤 ∈ 𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈)
57		anass 468	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑤 ∈ 𝑋) ∧ (𝐴𝐺𝑦) ∈ 𝑋) ↔ (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
58	57	biimpi 215	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑤 ∈ 𝑋) ∧ (𝐴𝐺𝑦) ∈ 𝑋) → (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
59	58	an32s 648	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐺 ∈ GrpOp ∧ (𝐴𝐺𝑦) ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) → (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
60	59	ex 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴𝐺𝑦) ∈ 𝑋) → (𝑤 ∈ 𝑋 → (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋))))
61	45, 60	syldan 590	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑤 ∈ 𝑋 → (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋))))
62	61	ad2ant2rl 745	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) → (𝑤 ∈ 𝑋 → (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋))))
63	62	imp 406	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) ∧ 𝑤 ∈ 𝑋) → (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
64	14	grpoidinvlem1 28767	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)) ∧ ((𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 ∧ ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)
65	63, 64	sylan 579	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) ∧ 𝑤 ∈ 𝑋) ∧ ((𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 ∧ ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)
66	65	exp43 436	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) → (𝑤 ∈ 𝑋 → ((𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈))))
67	66	rexlimdv 3211	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) → (∃𝑤 ∈ 𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
68	56, 67	syl5 34	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) → (((𝐴𝐺𝑦) ∈ 𝑋 ∧ 𝜓) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
69	46, 68	mpand 691	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) → (𝜓 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
70	69	exp32 420	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) → (𝜑 → ((𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝜓 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))))
71	70	com34 91	. . . . . . . . . 10 ⊢ ((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) → (𝜑 → (𝜓 → ((𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))))
72	71	imp32 418	. . . . . . . . 9 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) → ((𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
73	72	impl 455	. . . . . . . 8 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈))
74	73	adantr 480	. . . . . . 7 ⊢ ((((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈))
75	44, 74	mpd 15	. . . . . 6 ⊢ ((((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)
76	28, 75	eqtr3d 2780	. . . . 5 ⊢ ((((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝐴𝐺𝑦) = 𝑈)
77	76	ex 412	. . . 4 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝑦𝐺𝐴) = 𝑈 → (𝐴𝐺𝑦) = 𝑈))
78	77	ancld 550	. . 3 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝑦𝐺𝐴) = 𝑈 → ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈)))
79	78	reximdva 3202	. 2 ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) → (∃𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈 → ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈)))
80	13, 79	mpd 15	1 ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539   ∈ wcel 2108  ∀wral 3063  ∃wrex 3064  ran crn 5581  (class class class)co 7255  GrpOpcgr 28752

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-fo 6424  df-fv 6426  df-ov 7258  df-grpo 28756

This theorem is referenced by:  grpoidinv  28771