Theorem grpoidinvlem3 30665

Description: Lemma for grpoidinv 30667. (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 7397	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧𝐺𝑥) = (𝑦𝐺𝑥))
3	2	eqeq1d 2763	. . . . . . . 8 ⊢ (𝑧 = 𝑦 → ((𝑧𝐺𝑥) = 𝑈 ↔ (𝑦𝐺𝑥) = 𝑈))
4	3	cbvrexvw 3240	. . . . . . 7 ⊢ (∃𝑧 ∈ 𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈)
5	4	ralbii 3107	. . . . . 6 ⊢ (∀𝑥 ∈ 𝑋 ∃𝑧 ∈ 𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈)
6	1, 5	bitri 277	. . . . 5 ⊢ (𝜓 ↔ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈)
7		oveq2 7398	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑦𝐺𝑥) = (𝑦𝐺𝐴))
8	7	eqeq1d 2763	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((𝑦𝐺𝑥) = 𝑈 ↔ (𝑦𝐺𝐴) = 𝑈))
9	8	rexbidv 3185	. . . . . 6 ⊢ (𝑥 = 𝐴 → (∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈 ↔ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈))
10	9	rspccva 3579	. . . . 5 ⊢ ((∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈 ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈)
11	6, 10	sylanb 590	. . . 4 ⊢ ((𝜓 ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈)
12	11	adantll 724	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈)
13	12	adantll 724	. 2 ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈)
14		grpfo.1	. . . . . . . . . . . 12 ⊢ 𝑋 = ran 𝐺
15	14	grpocl 30659	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
16	15	3expa 1130	. . . . . . . . . 10 ⊢ (((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
17	16	adantllr 729	. . . . . . . . 9 ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
18	17	adantllr 729	. . . . . . . 8 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
19		grpidinvlem3.2	. . . . . . . . . . 11 ⊢ (𝜑 ↔ ∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥)
20	19	biimpi 218	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥)
21	20	ad2antrl 738	. . . . . . . . 9 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) → ∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥)
22	21	ad2antrr 736	. . . . . . . 8 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥)
23		oveq2 7398	. . . . . . . . . 10 ⊢ (𝑥 = (𝐴𝐺𝑦) → (𝑈𝐺𝑥) = (𝑈𝐺(𝐴𝐺𝑦)))
24		id 22	. . . . . . . . . 10 ⊢ (𝑥 = (𝐴𝐺𝑦) → 𝑥 = (𝐴𝐺𝑦))
25	23, 24	eqeq12d 2777	. . . . . . . . 9 ⊢ (𝑥 = (𝐴𝐺𝑦) → ((𝑈𝐺𝑥) = 𝑥 ↔ (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦)))
26	25	rspcva 3578	. . . . . . . 8 ⊢ (((𝐴𝐺𝑦) ∈ 𝑋 ∧ ∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥) → (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
27	18, 22, 26	syl2anc 593	. . . . . . 7 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
28	27	adantr 484	. . . . . 6 ⊢ ((((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
29		pm3.22 463	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐺 ∈ GrpOp) → (𝐺 ∈ GrpOp ∧ (𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)))
30	29	an31s 664	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝐺 ∈ GrpOp ∧ (𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)))
31	30	adantllr 729	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝐺 ∈ GrpOp ∧ (𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)))
32	31	adantllr 729	. . . . . . . . 9 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝐺 ∈ GrpOp ∧ (𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)))
33	32	adantr 484	. . . . . . . 8 ⊢ ((((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝐺 ∈ GrpOp ∧ (𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)))
34		oveq2 7398	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑈𝐺𝑥) = (𝑈𝐺𝑦))
35		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦)
36	34, 35	eqeq12d 2777	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((𝑈𝐺𝑥) = 𝑥 ↔ (𝑈𝐺𝑦) = 𝑦))
37	36	rspccva 3579	. . . . . . . . . . . . 13 ⊢ ((∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥 ∧ 𝑦 ∈ 𝑋) → (𝑈𝐺𝑦) = 𝑦)
38	19, 37	sylanb 590	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑈𝐺𝑦) = 𝑦)
39	38	adantlr 725	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑦 ∈ 𝑋) → (𝑈𝐺𝑦) = 𝑦)
40	39	adantlr 725	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑈𝐺𝑦) = 𝑦)
41	40	adantlll 728	. . . . . . . . 9 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑈𝐺𝑦) = 𝑦)
42	41	anim1i 624	. . . . . . . 8 ⊢ ((((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → ((𝑈𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝐴) = 𝑈))
43	14	grpoidinvlem2 30664	. . . . . . . 8 ⊢ (((𝐺 ∈ GrpOp ∧ (𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) ∧ ((𝑈𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝐴) = 𝑈)) → ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
44	33, 42, 43	syl2anc 593	. . . . . . 7 ⊢ ((((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
45	15	3expb 1132	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝐴𝐺𝑦) ∈ 𝑋)
46	45	ad2ant2rl 759	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) → (𝐴𝐺𝑦) ∈ 𝑋)
47		oveq1 7397	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑤 → (𝑧𝐺𝑥) = (𝑤𝐺𝑥))
48	47	eqeq1d 2763	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑤 → ((𝑧𝐺𝑥) = 𝑈 ↔ (𝑤𝐺𝑥) = 𝑈))
49	48	cbvrexvw 3240	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑧 ∈ 𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∃𝑤 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑈)
50	49	ralbii 3107	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑥 ∈ 𝑋 ∃𝑧 ∈ 𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∀𝑥 ∈ 𝑋 ∃𝑤 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑈)
51	1, 50	bitri 277	. . . . . . . . . . . . . . 15 ⊢ (𝜓 ↔ ∀𝑥 ∈ 𝑋 ∃𝑤 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑈)
52		oveq2 7398	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝐴𝐺𝑦) → (𝑤𝐺𝑥) = (𝑤𝐺(𝐴𝐺𝑦)))
53	52	eqeq1d 2763	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝐴𝐺𝑦) → ((𝑤𝐺𝑥) = 𝑈 ↔ (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈))
54	53	rexbidv 3185	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝐴𝐺𝑦) → (∃𝑤 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑈 ↔ ∃𝑤 ∈ 𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈))
55	54	rspcva 3578	. . . . . . . . . . . . . . 15 ⊢ (((𝐴𝐺𝑦) ∈ 𝑋 ∧ ∀𝑥 ∈ 𝑋 ∃𝑤 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑈) → ∃𝑤 ∈ 𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈)
56	51, 55	sylan2b 603	. . . . . . . . . . . . . 14 ⊢ (((𝐴𝐺𝑦) ∈ 𝑋 ∧ 𝜓) → ∃𝑤 ∈ 𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈)
57		anass 472	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑤 ∈ 𝑋) ∧ (𝐴𝐺𝑦) ∈ 𝑋) ↔ (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
58	57	biimpi 218	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑤 ∈ 𝑋) ∧ (𝐴𝐺𝑦) ∈ 𝑋) → (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
59	58	an32s 662	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐺 ∈ GrpOp ∧ (𝐴𝐺𝑦) ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) → (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
60	59	ex 416	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴𝐺𝑦) ∈ 𝑋) → (𝑤 ∈ 𝑋 → (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋))))
61	45, 60	syldan 600	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑤 ∈ 𝑋 → (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋))))
62	61	ad2ant2rl 759	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) → (𝑤 ∈ 𝑋 → (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋))))
63	62	imp 410	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) ∧ 𝑤 ∈ 𝑋) → (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
64	14	grpoidinvlem1 30663	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)) ∧ ((𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 ∧ ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)
65	63, 64	sylan 589	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) ∧ 𝑤 ∈ 𝑋) ∧ ((𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 ∧ ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)
66	65	exp43 440	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) → (𝑤 ∈ 𝑋 → ((𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈))))
67	66	rexlimdv 3160	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) → (∃𝑤 ∈ 𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
68	56, 67	syl5 34	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) → (((𝐴𝐺𝑦) ∈ 𝑋 ∧ 𝜓) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
69	46, 68	mpand 705	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) → (𝜓 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
70	69	exp32 424	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) → (𝜑 → ((𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝜓 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))))
71	70	com34 91	. . . . . . . . . 10 ⊢ ((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) → (𝜑 → (𝜓 → ((𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))))
72	71	imp32 422	. . . . . . . . 9 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) → ((𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
73	72	impl 459	. . . . . . . 8 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈))
74	73	adantr 484	. . . . . . 7 ⊢ ((((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈))
75	44, 74	mpd 15	. . . . . 6 ⊢ ((((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)
76	28, 75	eqtr3d 2798	. . . . 5 ⊢ ((((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝐴𝐺𝑦) = 𝑈)
77	76	ex 416	. . . 4 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝑦𝐺𝐴) = 𝑈 → (𝐴𝐺𝑦) = 𝑈))
78	77	ancld 558	. . 3 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝑦𝐺𝐴) = 𝑈 → ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈)))
79	78	reximdva 3174	. 2 ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) → (∃𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈 → ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈)))
80	13, 79	mpd 15	1 ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1559   ∈ wcel 2141  ∀wral 3075  ∃wrex 3085  ran crn 5644  (class class class)co 7390  GrpOpcgr 30648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pr 5387  ax-un 7712

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-iota 6471  df-fun 6517  df-fn 6518  df-f 6519  df-fo 6521  df-fv 6523  df-ov 7393  df-grpo 30652

This theorem is referenced by:  grpoidinv  30667