Theorem grpoidinvlem3 30593

Description: Lemma for grpoidinv 30595. (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 7375	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧𝐺𝑥) = (𝑦𝐺𝑥))
3	2	eqeq1d 2739	. . . . . . . 8 ⊢ (𝑧 = 𝑦 → ((𝑧𝐺𝑥) = 𝑈 ↔ (𝑦𝐺𝑥) = 𝑈))
4	3	cbvrexvw 3217	. . . . . . 7 ⊢ (∃𝑧 ∈ 𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈)
5	4	ralbii 3084	. . . . . 6 ⊢ (∀𝑥 ∈ 𝑋 ∃𝑧 ∈ 𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈)
6	1, 5	bitri 275	. . . . 5 ⊢ (𝜓 ↔ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈)
7		oveq2 7376	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑦𝐺𝑥) = (𝑦𝐺𝐴))
8	7	eqeq1d 2739	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((𝑦𝐺𝑥) = 𝑈 ↔ (𝑦𝐺𝐴) = 𝑈))
9	8	rexbidv 3162	. . . . . 6 ⊢ (𝑥 = 𝐴 → (∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈 ↔ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈))
10	9	rspccva 3577	. . . . 5 ⊢ ((∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈 ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈)
11	6, 10	sylanb 582	. . . 4 ⊢ ((𝜓 ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈)
12	11	adantll 715	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈)
13	12	adantll 715	. 2 ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈)
14		grpfo.1	. . . . . . . . . . . 12 ⊢ 𝑋 = ran 𝐺
15	14	grpocl 30587	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
16	15	3expa 1119	. . . . . . . . . 10 ⊢ (((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
17	16	adantllr 720	. . . . . . . . 9 ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
18	17	adantllr 720	. . . . . . . 8 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
19		grpidinvlem3.2	. . . . . . . . . . 11 ⊢ (𝜑 ↔ ∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥)
20	19	biimpi 216	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥)
21	20	ad2antrl 729	. . . . . . . . 9 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) → ∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥)
22	21	ad2antrr 727	. . . . . . . 8 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥)
23		oveq2 7376	. . . . . . . . . 10 ⊢ (𝑥 = (𝐴𝐺𝑦) → (𝑈𝐺𝑥) = (𝑈𝐺(𝐴𝐺𝑦)))
24		id 22	. . . . . . . . . 10 ⊢ (𝑥 = (𝐴𝐺𝑦) → 𝑥 = (𝐴𝐺𝑦))
25	23, 24	eqeq12d 2753	. . . . . . . . 9 ⊢ (𝑥 = (𝐴𝐺𝑦) → ((𝑈𝐺𝑥) = 𝑥 ↔ (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦)))
26	25	rspcva 3576	. . . . . . . 8 ⊢ (((𝐴𝐺𝑦) ∈ 𝑋 ∧ ∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥) → (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
27	18, 22, 26	syl2anc 585	. . . . . . 7 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
28	27	adantr 480	. . . . . 6 ⊢ ((((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
29		pm3.22 459	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐺 ∈ GrpOp) → (𝐺 ∈ GrpOp ∧ (𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)))
30	29	an31s 655	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝐺 ∈ GrpOp ∧ (𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)))
31	30	adantllr 720	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝐺 ∈ GrpOp ∧ (𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)))
32	31	adantllr 720	. . . . . . . . 9 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝐺 ∈ GrpOp ∧ (𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)))
33	32	adantr 480	. . . . . . . 8 ⊢ ((((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝐺 ∈ GrpOp ∧ (𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)))
34		oveq2 7376	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑈𝐺𝑥) = (𝑈𝐺𝑦))
35		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦)
36	34, 35	eqeq12d 2753	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((𝑈𝐺𝑥) = 𝑥 ↔ (𝑈𝐺𝑦) = 𝑦))
37	36	rspccva 3577	. . . . . . . . . . . . 13 ⊢ ((∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥 ∧ 𝑦 ∈ 𝑋) → (𝑈𝐺𝑦) = 𝑦)
38	19, 37	sylanb 582	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑈𝐺𝑦) = 𝑦)
39	38	adantlr 716	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑦 ∈ 𝑋) → (𝑈𝐺𝑦) = 𝑦)
40	39	adantlr 716	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑈𝐺𝑦) = 𝑦)
41	40	adantlll 719	. . . . . . . . 9 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑈𝐺𝑦) = 𝑦)
42	41	anim1i 616	. . . . . . . 8 ⊢ ((((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → ((𝑈𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝐴) = 𝑈))
43	14	grpoidinvlem2 30592	. . . . . . . 8 ⊢ (((𝐺 ∈ GrpOp ∧ (𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) ∧ ((𝑈𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝐴) = 𝑈)) → ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
44	33, 42, 43	syl2anc 585	. . . . . . 7 ⊢ ((((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
45	15	3expb 1121	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝐴𝐺𝑦) ∈ 𝑋)
46	45	ad2ant2rl 750	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) → (𝐴𝐺𝑦) ∈ 𝑋)
47		oveq1 7375	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑤 → (𝑧𝐺𝑥) = (𝑤𝐺𝑥))
48	47	eqeq1d 2739	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑤 → ((𝑧𝐺𝑥) = 𝑈 ↔ (𝑤𝐺𝑥) = 𝑈))
49	48	cbvrexvw 3217	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑧 ∈ 𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∃𝑤 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑈)
50	49	ralbii 3084	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑥 ∈ 𝑋 ∃𝑧 ∈ 𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∀𝑥 ∈ 𝑋 ∃𝑤 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑈)
51	1, 50	bitri 275	. . . . . . . . . . . . . . 15 ⊢ (𝜓 ↔ ∀𝑥 ∈ 𝑋 ∃𝑤 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑈)
52		oveq2 7376	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝐴𝐺𝑦) → (𝑤𝐺𝑥) = (𝑤𝐺(𝐴𝐺𝑦)))
53	52	eqeq1d 2739	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝐴𝐺𝑦) → ((𝑤𝐺𝑥) = 𝑈 ↔ (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈))
54	53	rexbidv 3162	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝐴𝐺𝑦) → (∃𝑤 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑈 ↔ ∃𝑤 ∈ 𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈))
55	54	rspcva 3576	. . . . . . . . . . . . . . 15 ⊢ (((𝐴𝐺𝑦) ∈ 𝑋 ∧ ∀𝑥 ∈ 𝑋 ∃𝑤 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑈) → ∃𝑤 ∈ 𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈)
56	51, 55	sylan2b 595	. . . . . . . . . . . . . 14 ⊢ (((𝐴𝐺𝑦) ∈ 𝑋 ∧ 𝜓) → ∃𝑤 ∈ 𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈)
57		anass 468	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑤 ∈ 𝑋) ∧ (𝐴𝐺𝑦) ∈ 𝑋) ↔ (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
58	57	biimpi 216	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑤 ∈ 𝑋) ∧ (𝐴𝐺𝑦) ∈ 𝑋) → (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
59	58	an32s 653	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐺 ∈ GrpOp ∧ (𝐴𝐺𝑦) ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) → (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
60	59	ex 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴𝐺𝑦) ∈ 𝑋) → (𝑤 ∈ 𝑋 → (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋))))
61	45, 60	syldan 592	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑤 ∈ 𝑋 → (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋))))
62	61	ad2ant2rl 750	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) → (𝑤 ∈ 𝑋 → (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋))))
63	62	imp 406	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) ∧ 𝑤 ∈ 𝑋) → (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
64	14	grpoidinvlem1 30591	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)) ∧ ((𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 ∧ ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)
65	63, 64	sylan 581	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) ∧ 𝑤 ∈ 𝑋) ∧ ((𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 ∧ ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)
66	65	exp43 436	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) → (𝑤 ∈ 𝑋 → ((𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈))))
67	66	rexlimdv 3137	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) → (∃𝑤 ∈ 𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
68	56, 67	syl5 34	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) → (((𝐴𝐺𝑦) ∈ 𝑋 ∧ 𝜓) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
69	46, 68	mpand 696	. . . . . . . . . . . 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 2774	. . . . 5 ⊢ ((((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝐴𝐺𝑦) = 𝑈)
77	76	ex 412	. . . 4 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝑦𝐺𝐴) = 𝑈 → (𝐴𝐺𝑦) = 𝑈))
78	77	ancld 550	. . 3 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝑦𝐺𝐴) = 𝑈 → ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈)))
79	78	reximdva 3151	. 2 ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) → (∃𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈 → ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈)))
80	13, 79	mpd 15	1 ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ∃wrex 3062  ran crn 5633  (class class class)co 7368  GrpOpcgr 30576

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fo 6506  df-fv 6508  df-ov 7371  df-grpo 30580

This theorem is referenced by:  grpoidinv  30595