MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  grpoidinvlem3 Structured version   Visualization version   GIF version

Theorem grpoidinvlem3 28075
Description: Lemma for grpoidinv 28077. (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.
StepHypRef Expression
1 grpidinvlem3.3 . . . . . 6 (𝜓 ↔ ∀𝑥𝑋𝑧𝑋 (𝑧𝐺𝑥) = 𝑈)
2 oveq1 6989 . . . . . . . . 9 (𝑧 = 𝑦 → (𝑧𝐺𝑥) = (𝑦𝐺𝑥))
32eqeq1d 2782 . . . . . . . 8 (𝑧 = 𝑦 → ((𝑧𝐺𝑥) = 𝑈 ↔ (𝑦𝐺𝑥) = 𝑈))
43cbvrexv 3386 . . . . . . 7 (∃𝑧𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∃𝑦𝑋 (𝑦𝐺𝑥) = 𝑈)
54ralbii 3117 . . . . . 6 (∀𝑥𝑋𝑧𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∀𝑥𝑋𝑦𝑋 (𝑦𝐺𝑥) = 𝑈)
61, 5bitri 267 . . . . 5 (𝜓 ↔ ∀𝑥𝑋𝑦𝑋 (𝑦𝐺𝑥) = 𝑈)
7 oveq2 6990 . . . . . . . 8 (𝑥 = 𝐴 → (𝑦𝐺𝑥) = (𝑦𝐺𝐴))
87eqeq1d 2782 . . . . . . 7 (𝑥 = 𝐴 → ((𝑦𝐺𝑥) = 𝑈 ↔ (𝑦𝐺𝐴) = 𝑈))
98rexbidv 3244 . . . . . 6 (𝑥 = 𝐴 → (∃𝑦𝑋 (𝑦𝐺𝑥) = 𝑈 ↔ ∃𝑦𝑋 (𝑦𝐺𝐴) = 𝑈))
109rspccva 3536 . . . . 5 ((∀𝑥𝑋𝑦𝑋 (𝑦𝐺𝑥) = 𝑈𝐴𝑋) → ∃𝑦𝑋 (𝑦𝐺𝐴) = 𝑈)
116, 10sylanb 573 . . . 4 ((𝜓𝐴𝑋) → ∃𝑦𝑋 (𝑦𝐺𝐴) = 𝑈)
1211adantll 702 . . 3 (((𝜑𝜓) ∧ 𝐴𝑋) → ∃𝑦𝑋 (𝑦𝐺𝐴) = 𝑈)
1312adantll 702 . 2 ((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) → ∃𝑦𝑋 (𝑦𝐺𝐴) = 𝑈)
14 grpfo.1 . . . . . . . . . . . 12 𝑋 = ran 𝐺
1514grpocl 28069 . . . . . . . . . . 11 ((𝐺 ∈ GrpOp ∧ 𝐴𝑋𝑦𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
16153expa 1099 . . . . . . . . . 10 (((𝐺 ∈ GrpOp ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
1716adantllr 707 . . . . . . . . 9 ((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
1817adantllr 707 . . . . . . . 8 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
19 grpidinvlem3.2 . . . . . . . . . . 11 (𝜑 ↔ ∀𝑥𝑋 (𝑈𝐺𝑥) = 𝑥)
2019biimpi 208 . . . . . . . . . 10 (𝜑 → ∀𝑥𝑋 (𝑈𝐺𝑥) = 𝑥)
2120ad2antrl 716 . . . . . . . . 9 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) → ∀𝑥𝑋 (𝑈𝐺𝑥) = 𝑥)
2221ad2antrr 714 . . . . . . . 8 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → ∀𝑥𝑋 (𝑈𝐺𝑥) = 𝑥)
23 oveq2 6990 . . . . . . . . . 10 (𝑥 = (𝐴𝐺𝑦) → (𝑈𝐺𝑥) = (𝑈𝐺(𝐴𝐺𝑦)))
24 id 22 . . . . . . . . . 10 (𝑥 = (𝐴𝐺𝑦) → 𝑥 = (𝐴𝐺𝑦))
2523, 24eqeq12d 2795 . . . . . . . . 9 (𝑥 = (𝐴𝐺𝑦) → ((𝑈𝐺𝑥) = 𝑥 ↔ (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦)))
2625rspcva 3535 . . . . . . . 8 (((𝐴𝐺𝑦) ∈ 𝑋 ∧ ∀𝑥𝑋 (𝑈𝐺𝑥) = 𝑥) → (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
2718, 22, 26syl2anc 576 . . . . . . 7 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
2827adantr 473 . . . . . 6 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
29 pm3.22 452 . . . . . . . . . . . 12 (((𝑦𝑋𝐴𝑋) ∧ 𝐺 ∈ GrpOp) → (𝐺 ∈ GrpOp ∧ (𝑦𝑋𝐴𝑋)))
3029an31s 642 . . . . . . . . . . 11 (((𝐺 ∈ GrpOp ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝐺 ∈ GrpOp ∧ (𝑦𝑋𝐴𝑋)))
3130adantllr 707 . . . . . . . . . 10 ((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝐺 ∈ GrpOp ∧ (𝑦𝑋𝐴𝑋)))
3231adantllr 707 . . . . . . . . 9 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝐺 ∈ GrpOp ∧ (𝑦𝑋𝐴𝑋)))
3332adantr 473 . . . . . . . 8 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝐺 ∈ GrpOp ∧ (𝑦𝑋𝐴𝑋)))
34 oveq2 6990 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑈𝐺𝑥) = (𝑈𝐺𝑦))
35 id 22 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦𝑥 = 𝑦)
3634, 35eqeq12d 2795 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → ((𝑈𝐺𝑥) = 𝑥 ↔ (𝑈𝐺𝑦) = 𝑦))
3736rspccva 3536 . . . . . . . . . . . . 13 ((∀𝑥𝑋 (𝑈𝐺𝑥) = 𝑥𝑦𝑋) → (𝑈𝐺𝑦) = 𝑦)
3819, 37sylanb 573 . . . . . . . . . . . 12 ((𝜑𝑦𝑋) → (𝑈𝐺𝑦) = 𝑦)
3938adantlr 703 . . . . . . . . . . 11 (((𝜑𝜓) ∧ 𝑦𝑋) → (𝑈𝐺𝑦) = 𝑦)
4039adantlr 703 . . . . . . . . . 10 ((((𝜑𝜓) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝑈𝐺𝑦) = 𝑦)
4140adantlll 706 . . . . . . . . 9 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝑈𝐺𝑦) = 𝑦)
4241anim1i 606 . . . . . . . 8 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → ((𝑈𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝐴) = 𝑈))
4314grpoidinvlem2 28074 . . . . . . . 8 (((𝐺 ∈ GrpOp ∧ (𝑦𝑋𝐴𝑋)) ∧ ((𝑈𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝐴) = 𝑈)) → ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
4433, 42, 43syl2anc 576 . . . . . . 7 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
45153expb 1101 . . . . . . . . . . . . . 14 ((𝐺 ∈ GrpOp ∧ (𝐴𝑋𝑦𝑋)) → (𝐴𝐺𝑦) ∈ 𝑋)
4645ad2ant2rl 737 . . . . . . . . . . . . 13 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) → (𝐴𝐺𝑦) ∈ 𝑋)
47 oveq1 6989 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑤 → (𝑧𝐺𝑥) = (𝑤𝐺𝑥))
4847eqeq1d 2782 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑤 → ((𝑧𝐺𝑥) = 𝑈 ↔ (𝑤𝐺𝑥) = 𝑈))
4948cbvrexv 3386 . . . . . . . . . . . . . . . . 17 (∃𝑧𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∃𝑤𝑋 (𝑤𝐺𝑥) = 𝑈)
5049ralbii 3117 . . . . . . . . . . . . . . . 16 (∀𝑥𝑋𝑧𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∀𝑥𝑋𝑤𝑋 (𝑤𝐺𝑥) = 𝑈)
511, 50bitri 267 . . . . . . . . . . . . . . 15 (𝜓 ↔ ∀𝑥𝑋𝑤𝑋 (𝑤𝐺𝑥) = 𝑈)
52 oveq2 6990 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝐴𝐺𝑦) → (𝑤𝐺𝑥) = (𝑤𝐺(𝐴𝐺𝑦)))
5352eqeq1d 2782 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝐴𝐺𝑦) → ((𝑤𝐺𝑥) = 𝑈 ↔ (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈))
5453rexbidv 3244 . . . . . . . . . . . . . . . 16 (𝑥 = (𝐴𝐺𝑦) → (∃𝑤𝑋 (𝑤𝐺𝑥) = 𝑈 ↔ ∃𝑤𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈))
5554rspcva 3535 . . . . . . . . . . . . . . 15 (((𝐴𝐺𝑦) ∈ 𝑋 ∧ ∀𝑥𝑋𝑤𝑋 (𝑤𝐺𝑥) = 𝑈) → ∃𝑤𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈)
5651, 55sylan2b 585 . . . . . . . . . . . . . 14 (((𝐴𝐺𝑦) ∈ 𝑋𝜓) → ∃𝑤𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈)
57 anass 461 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐺 ∈ GrpOp ∧ 𝑤𝑋) ∧ (𝐴𝐺𝑦) ∈ 𝑋) ↔ (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
5857biimpi 208 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐺 ∈ GrpOp ∧ 𝑤𝑋) ∧ (𝐴𝐺𝑦) ∈ 𝑋) → (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
5958an32s 640 . . . . . . . . . . . . . . . . . . . . 21 (((𝐺 ∈ GrpOp ∧ (𝐴𝐺𝑦) ∈ 𝑋) ∧ 𝑤𝑋) → (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
6059ex 405 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ GrpOp ∧ (𝐴𝐺𝑦) ∈ 𝑋) → (𝑤𝑋 → (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋))))
6145, 60syldan 583 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ GrpOp ∧ (𝐴𝑋𝑦𝑋)) → (𝑤𝑋 → (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋))))
6261ad2ant2rl 737 . . . . . . . . . . . . . . . . . 18 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) → (𝑤𝑋 → (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋))))
6362imp 398 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) ∧ 𝑤𝑋) → (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
6414grpoidinvlem1 28073 . . . . . . . . . . . . . . . . 17 (((𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)) ∧ ((𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 ∧ ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)
6563, 64sylan 572 . . . . . . . . . . . . . . . 16 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) ∧ 𝑤𝑋) ∧ ((𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 ∧ ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)
6665exp43 429 . . . . . . . . . . . . . . 15 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) → (𝑤𝑋 → ((𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈))))
6766rexlimdv 3230 . . . . . . . . . . . . . 14 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) → (∃𝑤𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
6856, 67syl5 34 . . . . . . . . . . . . 13 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) → (((𝐴𝐺𝑦) ∈ 𝑋𝜓) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
6946, 68mpand 683 . . . . . . . . . . . 12 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) → (𝜓 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
7069exp32 413 . . . . . . . . . . 11 ((𝐺 ∈ GrpOp ∧ 𝑈𝑋) → (𝜑 → ((𝐴𝑋𝑦𝑋) → (𝜓 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))))
7170com34 91 . . . . . . . . . 10 ((𝐺 ∈ GrpOp ∧ 𝑈𝑋) → (𝜑 → (𝜓 → ((𝐴𝑋𝑦𝑋) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))))
7271imp32 411 . . . . . . . . 9 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) → ((𝐴𝑋𝑦𝑋) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
7372impl 448 . . . . . . . 8 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈))
7473adantr 473 . . . . . . 7 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈))
7544, 74mpd 15 . . . . . 6 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)
7628, 75eqtr3d 2818 . . . . 5 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝐴𝐺𝑦) = 𝑈)
7776ex 405 . . . 4 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → ((𝑦𝐺𝐴) = 𝑈 → (𝐴𝐺𝑦) = 𝑈))
7877ancld 543 . . 3 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → ((𝑦𝐺𝐴) = 𝑈 → ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈)))
7978reximdva 3221 . 2 ((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) → (∃𝑦𝑋 (𝑦𝐺𝐴) = 𝑈 → ∃𝑦𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈)))
8013, 79mpd 15 1 ((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) → ∃𝑦𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387   = wceq 1508  wcel 2051  wral 3090  wrex 3091  ran crn 5412  (class class class)co 6982  GrpOpcgr 28058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2752  ax-sep 5064  ax-nul 5071  ax-pr 5190  ax-un 7285
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2551  df-eu 2589  df-clab 2761  df-cleq 2773  df-clel 2848  df-nfc 2920  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3419  df-sbc 3684  df-csb 3789  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-nul 4182  df-if 4354  df-sn 4445  df-pr 4447  df-op 4451  df-uni 4718  df-iun 4799  df-br 4935  df-opab 4997  df-mpt 5014  df-id 5316  df-xp 5417  df-rel 5418  df-cnv 5419  df-co 5420  df-dm 5421  df-rn 5422  df-iota 6157  df-fun 6195  df-fn 6196  df-f 6197  df-fo 6199  df-fv 6201  df-ov 6985  df-grpo 28062
This theorem is referenced by:  grpoidinv  28077
  Copyright terms: Public domain W3C validator