Theorem grpoidinvlem3 28289

Description: Lemma for grpoidinv 28291. (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 7142	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧𝐺𝑥) = (𝑦𝐺𝑥))
3	2	eqeq1d 2800	. . . . . . . 8 ⊢ (𝑧 = 𝑦 → ((𝑧𝐺𝑥) = 𝑈 ↔ (𝑦𝐺𝑥) = 𝑈))
4	3	cbvrexvw 3397	. . . . . . 7 ⊢ (∃𝑧 ∈ 𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈)
5	4	ralbii 3133	. . . . . 6 ⊢ (∀𝑥 ∈ 𝑋 ∃𝑧 ∈ 𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈)
6	1, 5	bitri 278	. . . . 5 ⊢ (𝜓 ↔ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈)
7		oveq2 7143	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑦𝐺𝑥) = (𝑦𝐺𝐴))
8	7	eqeq1d 2800	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((𝑦𝐺𝑥) = 𝑈 ↔ (𝑦𝐺𝐴) = 𝑈))
9	8	rexbidv 3256	. . . . . 6 ⊢ (𝑥 = 𝐴 → (∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈 ↔ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈))
10	9	rspccva 3570	. . . . 5 ⊢ ((∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈 ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈)
11	6, 10	sylanb 584	. . . 4 ⊢ ((𝜓 ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈)
12	11	adantll 713	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈)
13	12	adantll 713	. 2 ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈)
14		grpfo.1	. . . . . . . . . . . 12 ⊢ 𝑋 = ran 𝐺
15	14	grpocl 28283	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
16	15	3expa 1115	. . . . . . . . . 10 ⊢ (((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
17	16	adantllr 718	. . . . . . . . 9 ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
18	17	adantllr 718	. . . . . . . 8 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
19		grpidinvlem3.2	. . . . . . . . . . 11 ⊢ (𝜑 ↔ ∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥)
20	19	biimpi 219	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥)
21	20	ad2antrl 727	. . . . . . . . 9 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) → ∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥)
22	21	ad2antrr 725	. . . . . . . 8 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥)
23		oveq2 7143	. . . . . . . . . 10 ⊢ (𝑥 = (𝐴𝐺𝑦) → (𝑈𝐺𝑥) = (𝑈𝐺(𝐴𝐺𝑦)))
24		id 22	. . . . . . . . . 10 ⊢ (𝑥 = (𝐴𝐺𝑦) → 𝑥 = (𝐴𝐺𝑦))
25	23, 24	eqeq12d 2814	. . . . . . . . 9 ⊢ (𝑥 = (𝐴𝐺𝑦) → ((𝑈𝐺𝑥) = 𝑥 ↔ (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦)))
26	25	rspcva 3569	. . . . . . . 8 ⊢ (((𝐴𝐺𝑦) ∈ 𝑋 ∧ ∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥) → (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
27	18, 22, 26	syl2anc 587	. . . . . . 7 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
28	27	adantr 484	. . . . . 6 ⊢ ((((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
29		pm3.22 463	. . . . . . . . . . . 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 484	. . . . . . . 8 ⊢ ((((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝐺 ∈ GrpOp ∧ (𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)))
34		oveq2 7143	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑈𝐺𝑥) = (𝑈𝐺𝑦))
35		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦)
36	34, 35	eqeq12d 2814	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((𝑈𝐺𝑥) = 𝑥 ↔ (𝑈𝐺𝑦) = 𝑦))
37	36	rspccva 3570	. . . . . . . . . . . . 13 ⊢ ((∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥 ∧ 𝑦 ∈ 𝑋) → (𝑈𝐺𝑦) = 𝑦)
38	19, 37	sylanb 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑈𝐺𝑦) = 𝑦)
39	38	adantlr 714	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑦 ∈ 𝑋) → (𝑈𝐺𝑦) = 𝑦)
40	39	adantlr 714	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑈𝐺𝑦) = 𝑦)
41	40	adantlll 717	. . . . . . . . 9 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑈𝐺𝑦) = 𝑦)
42	41	anim1i 617	. . . . . . . 8 ⊢ ((((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → ((𝑈𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝐴) = 𝑈))
43	14	grpoidinvlem2 28288	. . . . . . . 8 ⊢ (((𝐺 ∈ GrpOp ∧ (𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) ∧ ((𝑈𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝐴) = 𝑈)) → ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
44	33, 42, 43	syl2anc 587	. . . . . . 7 ⊢ ((((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
45	15	3expb 1117	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝐴𝐺𝑦) ∈ 𝑋)
46	45	ad2ant2rl 748	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) → (𝐴𝐺𝑦) ∈ 𝑋)
47		oveq1 7142	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑤 → (𝑧𝐺𝑥) = (𝑤𝐺𝑥))
48	47	eqeq1d 2800	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑤 → ((𝑧𝐺𝑥) = 𝑈 ↔ (𝑤𝐺𝑥) = 𝑈))
49	48	cbvrexvw 3397	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑧 ∈ 𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∃𝑤 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑈)
50	49	ralbii 3133	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑥 ∈ 𝑋 ∃𝑧 ∈ 𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∀𝑥 ∈ 𝑋 ∃𝑤 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑈)
51	1, 50	bitri 278	. . . . . . . . . . . . . . 15 ⊢ (𝜓 ↔ ∀𝑥 ∈ 𝑋 ∃𝑤 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑈)
52		oveq2 7143	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝐴𝐺𝑦) → (𝑤𝐺𝑥) = (𝑤𝐺(𝐴𝐺𝑦)))
53	52	eqeq1d 2800	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝐴𝐺𝑦) → ((𝑤𝐺𝑥) = 𝑈 ↔ (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈))
54	53	rexbidv 3256	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝐴𝐺𝑦) → (∃𝑤 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑈 ↔ ∃𝑤 ∈ 𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈))
55	54	rspcva 3569	. . . . . . . . . . . . . . 15 ⊢ (((𝐴𝐺𝑦) ∈ 𝑋 ∧ ∀𝑥 ∈ 𝑋 ∃𝑤 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑈) → ∃𝑤 ∈ 𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈)
56	51, 55	sylan2b 596	. . . . . . . . . . . . . 14 ⊢ (((𝐴𝐺𝑦) ∈ 𝑋 ∧ 𝜓) → ∃𝑤 ∈ 𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈)
57		anass 472	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑤 ∈ 𝑋) ∧ (𝐴𝐺𝑦) ∈ 𝑋) ↔ (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
58	57	biimpi 219	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑤 ∈ 𝑋) ∧ (𝐴𝐺𝑦) ∈ 𝑋) → (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
59	58	an32s 651	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐺 ∈ GrpOp ∧ (𝐴𝐺𝑦) ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) → (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
60	59	ex 416	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴𝐺𝑦) ∈ 𝑋) → (𝑤 ∈ 𝑋 → (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋))))
61	45, 60	syldan 594	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑤 ∈ 𝑋 → (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋))))
62	61	ad2ant2rl 748	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) → (𝑤 ∈ 𝑋 → (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋))))
63	62	imp 410	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) ∧ 𝑤 ∈ 𝑋) → (𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
64	14	grpoidinvlem1 28287	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐺 ∈ GrpOp ∧ (𝑤 ∈ 𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)) ∧ ((𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 ∧ ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)
65	63, 64	sylan 583	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) ∧ 𝑤 ∈ 𝑋) ∧ ((𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 ∧ ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)
66	65	exp43 440	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) → (𝑤 ∈ 𝑋 → ((𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈))))
67	66	rexlimdv 3242	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) → (∃𝑤 ∈ 𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
68	56, 67	syl5 34	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ (𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) → (((𝐴𝐺𝑦) ∈ 𝑋 ∧ 𝜓) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
69	46, 68	mpand 694	. . . . . . . . . . . 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 2835	. . . . 5 ⊢ ((((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝐴𝐺𝑦) = 𝑈)
77	76	ex 416	. . . 4 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝑦𝐺𝐴) = 𝑈 → (𝐴𝐺𝑦) = 𝑈))
78	77	ancld 554	. . 3 ⊢ (((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝑦𝐺𝐴) = 𝑈 → ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈)))
79	78	reximdva 3233	. 2 ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) → (∃𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈 → ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈)))
80	13, 79	mpd 15	1 ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3106  ∃wrex 3107  ran crn 5520  (class class class)co 7135  GrpOpcgr 28272

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-fo 6330  df-fv 6332  df-ov 7138  df-grpo 28276

This theorem is referenced by:  grpoidinv  28291