Theorem grpoidinvlem3 29759

Description: Lemma for grpoidinv 29761. (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 7416	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧𝐺𝑥) = (𝑦𝐺𝑥))
3	2	eqeq1d 2735	. . . . . . . 8 ⊢ (𝑧 = 𝑦 → ((𝑧𝐺𝑥) = 𝑈 ↔ (𝑦𝐺𝑥) = 𝑈))
4	3	cbvrexvw 3236	. . . . . . 7 ⊢ (∃𝑧 ∈ 𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈)
5	4	ralbii 3094	. . . . . 6 ⊢ (∀𝑥 ∈ 𝑋 ∃𝑧 ∈ 𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈)
6	1, 5	bitri 275	. . . . 5 ⊢ (𝜓 ↔ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈)
7		oveq2 7417	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑦𝐺𝑥) = (𝑦𝐺𝐴))
8	7	eqeq1d 2735	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((𝑦𝐺𝑥) = 𝑈 ↔ (𝑦𝐺𝐴) = 𝑈))
9	8	rexbidv 3179	. . . . . 6 ⊢ (𝑥 = 𝐴 → (∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈 ↔ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈))
10	9	rspccva 3612	. . . . 5 ⊢ ((∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈 ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈)
11	6, 10	sylanb 582	. . . 4 ⊢ ((𝜓 ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈)
12	11	adantll 713	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈)
13	12	adantll 713	. 2 ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈)
14		grpfo.1	. . . . . . . . . . . 12 ⊢ 𝑋 = ran 𝐺
15	14	grpocl 29753	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
16	15	3expa 1119	. . . . . . . . . 10 ⊢ (((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
17	16	adantllr 718	. . . . . . . . 9 ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
18	17	adantllr 718	. . . . . . . 8 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
19		grpidinvlem3.2	. . . . . . . . . . 11 ⊢ (𝜑 ↔ ∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥)
20	19	biimpi 215	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥)
21	20	ad2antrl 727	. . . . . . . . 9 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) → ∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥)
22	21	ad2antrr 725	. . . . . . . 8 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥)
23		oveq2 7417	. . . . . . . . . 10 ⊢ (𝑥 = (𝐴𝐺𝑦) → (𝑈𝐺𝑥) = (𝑈𝐺(𝐴𝐺𝑦)))
24		id 22	. . . . . . . . . 10 ⊢ (𝑥 = (𝐴𝐺𝑦) → 𝑥 = (𝐴𝐺𝑦))
25	23, 24	eqeq12d 2749	. . . . . . . . 9 ⊢ (𝑥 = (𝐴𝐺𝑦) → ((𝑈𝐺𝑥) = 𝑥 ↔ (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦)))
26	25	rspcva 3611	. . . . . . . 8 ⊢ (((𝐴𝐺𝑦) ∈ 𝑋 ∧ ∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥) → (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
27	18, 22, 26	syl2anc 585	. . . . . . 7 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
28	27	adantr 482	. . . . . 6 ⊢ ((((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
29		pm3.22 461	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐺 ∈ GrpOp) → (𝐺 ∈ GrpOp ∧ (𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)))
30	29	an31s 653	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝐺 ∈ GrpOp ∧ (𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)))
31	30	adantllr 718	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝐺 ∈ GrpOp ∧ (𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)))
32	31	adantllr 718	. . . . . . . . 9 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝐺 ∈ GrpOp ∧ (𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)))
33	32	adantr 482	. . . . . . . 8 ⊢ ((((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝐺 ∈ GrpOp ∧ (𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)))
34		oveq2 7417	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑈𝐺𝑥) = (𝑈𝐺𝑦))
35		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦)
36	34, 35	eqeq12d 2749	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((𝑈𝐺𝑥) = 𝑥 ↔ (𝑈𝐺𝑦) = 𝑦))
37	36	rspccva 3612	. . . . . . . . . . . . 13 ⊢ ((∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥 ∧ 𝑦 ∈ 𝑋) → (𝑈𝐺𝑦) = 𝑦)
38	19, 37	sylanb 582	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑈𝐺𝑦) = 𝑦)
39	38	adantlr 714	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑦 ∈ 𝑋) → (𝑈𝐺𝑦) = 𝑦)
40	39	adantlr 714	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑈𝐺𝑦) = 𝑦)
41	40	adantlll 717	. . . . . . . . 9 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑈𝐺𝑦) = 𝑦)
42	41	anim1i 616	. . . . . . . 8 ⊢ ((((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → ((𝑈𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝐴) = 𝑈))
43	14	grpoidinvlem2 29758	. . . . . . . 8 ⊢ (((𝐺 ∈ GrpOp ∧ (𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) ∧ ((𝑈𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝐴) = 𝑈)) → ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
44	33, 42, 43	syl2anc 585	. . . . . . 7 ⊢ ((((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
45	15	3expb 1121	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝐴𝐺𝑦) ∈ 𝑋)
46	45	ad2ant2rl 748	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) → (𝐴𝐺𝑦) ∈ 𝑋)
47		oveq1 7416	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑤 → (𝑧𝐺𝑥) = (𝑤𝐺𝑥))
48	47	eqeq1d 2735	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑤 → ((𝑧𝐺𝑥) = 𝑈 ↔ (𝑤𝐺𝑥) = 𝑈))
49	48	cbvrexvw 3236	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑧 ∈ 𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∃𝑤 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑈)
50	49	ralbii 3094	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑥 ∈ 𝑋 ∃𝑧 ∈ 𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∀𝑥 ∈ 𝑋 ∃𝑤 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑈)
51	1, 50	bitri 275	. . . . . . . . . . . . . . 15 ⊢ (𝜓 ↔ ∀𝑥 ∈ 𝑋 ∃𝑤 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑈)
52		oveq2 7417	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝐴𝐺𝑦) → (𝑤𝐺𝑥) = (𝑤𝐺(𝐴𝐺𝑦)))
53	52	eqeq1d 2735	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝐴𝐺𝑦) → ((𝑤𝐺𝑥) = 𝑈 ↔ (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈))
54	53	rexbidv 3179	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝐴𝐺𝑦) → (∃𝑤 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑈 ↔ ∃𝑤 ∈ 𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈))
55	54	rspcva 3611	. . . . . . . . . . . . . . 15 ⊢ (((𝐴𝐺𝑦) ∈ 𝑋 ∧ ∀𝑥 ∈ 𝑋 ∃𝑤 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑈) → ∃𝑤 ∈ 𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈)
56	51, 55	sylan2b 595	. . . . . . . . . . . . . 14 ⊢ (((𝐴𝐺𝑦) ∈ 𝑋 ∧ 𝜓) → ∃𝑤 ∈ 𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈)
57		anass 470	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑤 ∈ 𝑋) ∧ (𝐴𝐺𝑦) ∈ 𝑋) ↔ (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
58	57	biimpi 215	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑤 ∈ 𝑋) ∧ (𝐴𝐺𝑦) ∈ 𝑋) → (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
59	58	an32s 651	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐺 ∈ GrpOp ∧ (𝐴𝐺𝑦) ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) → (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
60	59	ex 414	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴𝐺𝑦) ∈ 𝑋) → (𝑤 ∈ 𝑋 → (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋))))
61	45, 60	syldan 592	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑤 ∈ 𝑋 → (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋))))
62	61	ad2ant2rl 748	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) → (𝑤 ∈ 𝑋 → (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋))))
63	62	imp 408	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) ∧ 𝑤 ∈ 𝑋) → (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
64	14	grpoidinvlem1 29757	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)) ∧ ((𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 ∧ ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)
65	63, 64	sylan 581	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) ∧ 𝑤 ∈ 𝑋) ∧ ((𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 ∧ ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)
66	65	exp43 438	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) → (𝑤 ∈ 𝑋 → ((𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈))))
67	66	rexlimdv 3154	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) → (∃𝑤 ∈ 𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
68	56, 67	syl5 34	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) → (((𝐴𝐺𝑦) ∈ 𝑋 ∧ 𝜓) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
69	46, 68	mpand 694	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) → (𝜓 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
70	69	exp32 422	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) → (𝜑 → ((𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝜓 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))))
71	70	com34 91	. . . . . . . . . 10 ⊢ ((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) → (𝜑 → (𝜓 → ((𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))))
72	71	imp32 420	. . . . . . . . 9 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) → ((𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
73	72	impl 457	. . . . . . . 8 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈))
74	73	adantr 482	. . . . . . 7 ⊢ ((((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈))
75	44, 74	mpd 15	. . . . . 6 ⊢ ((((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)
76	28, 75	eqtr3d 2775	. . . . 5 ⊢ ((((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝐴𝐺𝑦) = 𝑈)
77	76	ex 414	. . . 4 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝑦𝐺𝐴) = 𝑈 → (𝐴𝐺𝑦) = 𝑈))
78	77	ancld 552	. . 3 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝑦𝐺𝐴) = 𝑈 → ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈)))
79	78	reximdva 3169	. 2 ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) → (∃𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈 → ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈)))
80	13, 79	mpd 15	1 ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ∀wral 3062  ∃wrex 3071  ran crn 5678  (class class class)co 7409  GrpOpcgr 29742

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fo 6550  df-fv 6552  df-ov 7412  df-grpo 29746

This theorem is referenced by:  grpoidinv  29761