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

Theorem grpoidinvlem3 27687
Description: Lemma for grpoidinv 27689. (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 6879 . . . . . . . . 9 (𝑧 = 𝑦 → (𝑧𝐺𝑥) = (𝑦𝐺𝑥))
32eqeq1d 2806 . . . . . . . 8 (𝑧 = 𝑦 → ((𝑧𝐺𝑥) = 𝑈 ↔ (𝑦𝐺𝑥) = 𝑈))
43cbvrexv 3359 . . . . . . 7 (∃𝑧𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∃𝑦𝑋 (𝑦𝐺𝑥) = 𝑈)
54ralbii 3166 . . . . . 6 (∀𝑥𝑋𝑧𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∀𝑥𝑋𝑦𝑋 (𝑦𝐺𝑥) = 𝑈)
61, 5bitri 266 . . . . 5 (𝜓 ↔ ∀𝑥𝑋𝑦𝑋 (𝑦𝐺𝑥) = 𝑈)
7 oveq2 6880 . . . . . . . 8 (𝑥 = 𝐴 → (𝑦𝐺𝑥) = (𝑦𝐺𝐴))
87eqeq1d 2806 . . . . . . 7 (𝑥 = 𝐴 → ((𝑦𝐺𝑥) = 𝑈 ↔ (𝑦𝐺𝐴) = 𝑈))
98rexbidv 3238 . . . . . 6 (𝑥 = 𝐴 → (∃𝑦𝑋 (𝑦𝐺𝑥) = 𝑈 ↔ ∃𝑦𝑋 (𝑦𝐺𝐴) = 𝑈))
109rspccva 3499 . . . . 5 ((∀𝑥𝑋𝑦𝑋 (𝑦𝐺𝑥) = 𝑈𝐴𝑋) → ∃𝑦𝑋 (𝑦𝐺𝐴) = 𝑈)
116, 10sylanb 572 . . . 4 ((𝜓𝐴𝑋) → ∃𝑦𝑋 (𝑦𝐺𝐴) = 𝑈)
1211adantll 696 . . 3 (((𝜑𝜓) ∧ 𝐴𝑋) → ∃𝑦𝑋 (𝑦𝐺𝐴) = 𝑈)
1312adantll 696 . 2 ((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) → ∃𝑦𝑋 (𝑦𝐺𝐴) = 𝑈)
14 grpfo.1 . . . . . . . . . . . 12 𝑋 = ran 𝐺
1514grpocl 27681 . . . . . . . . . . 11 ((𝐺 ∈ GrpOp ∧ 𝐴𝑋𝑦𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
16153expa 1140 . . . . . . . . . 10 (((𝐺 ∈ GrpOp ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
1716adantllr 701 . . . . . . . . 9 ((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
1817adantllr 701 . . . . . . . 8 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
19 grpidinvlem3.2 . . . . . . . . . . 11 (𝜑 ↔ ∀𝑥𝑋 (𝑈𝐺𝑥) = 𝑥)
2019biimpi 207 . . . . . . . . . 10 (𝜑 → ∀𝑥𝑋 (𝑈𝐺𝑥) = 𝑥)
2120ad2antrl 710 . . . . . . . . 9 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) → ∀𝑥𝑋 (𝑈𝐺𝑥) = 𝑥)
2221ad2antrr 708 . . . . . . . 8 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → ∀𝑥𝑋 (𝑈𝐺𝑥) = 𝑥)
23 oveq2 6880 . . . . . . . . . 10 (𝑥 = (𝐴𝐺𝑦) → (𝑈𝐺𝑥) = (𝑈𝐺(𝐴𝐺𝑦)))
24 id 22 . . . . . . . . . 10 (𝑥 = (𝐴𝐺𝑦) → 𝑥 = (𝐴𝐺𝑦))
2523, 24eqeq12d 2819 . . . . . . . . 9 (𝑥 = (𝐴𝐺𝑦) → ((𝑈𝐺𝑥) = 𝑥 ↔ (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦)))
2625rspcva 3498 . . . . . . . 8 (((𝐴𝐺𝑦) ∈ 𝑋 ∧ ∀𝑥𝑋 (𝑈𝐺𝑥) = 𝑥) → (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
2718, 22, 26syl2anc 575 . . . . . . 7 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
2827adantr 468 . . . . . 6 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
29 pm3.22 449 . . . . . . . . . . . 12 (((𝑦𝑋𝐴𝑋) ∧ 𝐺 ∈ GrpOp) → (𝐺 ∈ GrpOp ∧ (𝑦𝑋𝐴𝑋)))
3029an31s 636 . . . . . . . . . . 11 (((𝐺 ∈ GrpOp ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝐺 ∈ GrpOp ∧ (𝑦𝑋𝐴𝑋)))
3130adantllr 701 . . . . . . . . . 10 ((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝐺 ∈ GrpOp ∧ (𝑦𝑋𝐴𝑋)))
3231adantllr 701 . . . . . . . . 9 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝐺 ∈ GrpOp ∧ (𝑦𝑋𝐴𝑋)))
3332adantr 468 . . . . . . . 8 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝐺 ∈ GrpOp ∧ (𝑦𝑋𝐴𝑋)))
34 oveq2 6880 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑈𝐺𝑥) = (𝑈𝐺𝑦))
35 id 22 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦𝑥 = 𝑦)
3634, 35eqeq12d 2819 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → ((𝑈𝐺𝑥) = 𝑥 ↔ (𝑈𝐺𝑦) = 𝑦))
3736rspccva 3499 . . . . . . . . . . . . 13 ((∀𝑥𝑋 (𝑈𝐺𝑥) = 𝑥𝑦𝑋) → (𝑈𝐺𝑦) = 𝑦)
3819, 37sylanb 572 . . . . . . . . . . . 12 ((𝜑𝑦𝑋) → (𝑈𝐺𝑦) = 𝑦)
3938adantlr 697 . . . . . . . . . . 11 (((𝜑𝜓) ∧ 𝑦𝑋) → (𝑈𝐺𝑦) = 𝑦)
4039adantlr 697 . . . . . . . . . 10 ((((𝜑𝜓) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝑈𝐺𝑦) = 𝑦)
4140adantlll 700 . . . . . . . . 9 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝑈𝐺𝑦) = 𝑦)
4241anim1i 604 . . . . . . . 8 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → ((𝑈𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝐴) = 𝑈))
4314grpoidinvlem2 27686 . . . . . . . 8 (((𝐺 ∈ GrpOp ∧ (𝑦𝑋𝐴𝑋)) ∧ ((𝑈𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝐴) = 𝑈)) → ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
4433, 42, 43syl2anc 575 . . . . . . 7 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
45153expb 1142 . . . . . . . . . . . . . 14 ((𝐺 ∈ GrpOp ∧ (𝐴𝑋𝑦𝑋)) → (𝐴𝐺𝑦) ∈ 𝑋)
4645ad2ant2rl 746 . . . . . . . . . . . . 13 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) → (𝐴𝐺𝑦) ∈ 𝑋)
47 oveq1 6879 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑤 → (𝑧𝐺𝑥) = (𝑤𝐺𝑥))
4847eqeq1d 2806 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑤 → ((𝑧𝐺𝑥) = 𝑈 ↔ (𝑤𝐺𝑥) = 𝑈))
4948cbvrexv 3359 . . . . . . . . . . . . . . . . 17 (∃𝑧𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∃𝑤𝑋 (𝑤𝐺𝑥) = 𝑈)
5049ralbii 3166 . . . . . . . . . . . . . . . 16 (∀𝑥𝑋𝑧𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∀𝑥𝑋𝑤𝑋 (𝑤𝐺𝑥) = 𝑈)
511, 50bitri 266 . . . . . . . . . . . . . . 15 (𝜓 ↔ ∀𝑥𝑋𝑤𝑋 (𝑤𝐺𝑥) = 𝑈)
52 oveq2 6880 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝐴𝐺𝑦) → (𝑤𝐺𝑥) = (𝑤𝐺(𝐴𝐺𝑦)))
5352eqeq1d 2806 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝐴𝐺𝑦) → ((𝑤𝐺𝑥) = 𝑈 ↔ (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈))
5453rexbidv 3238 . . . . . . . . . . . . . . . 16 (𝑥 = (𝐴𝐺𝑦) → (∃𝑤𝑋 (𝑤𝐺𝑥) = 𝑈 ↔ ∃𝑤𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈))
5554rspcva 3498 . . . . . . . . . . . . . . 15 (((𝐴𝐺𝑦) ∈ 𝑋 ∧ ∀𝑥𝑋𝑤𝑋 (𝑤𝐺𝑥) = 𝑈) → ∃𝑤𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈)
5651, 55sylan2b 583 . . . . . . . . . . . . . 14 (((𝐴𝐺𝑦) ∈ 𝑋𝜓) → ∃𝑤𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈)
57 anass 456 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐺 ∈ GrpOp ∧ 𝑤𝑋) ∧ (𝐴𝐺𝑦) ∈ 𝑋) ↔ (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
5857biimpi 207 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐺 ∈ GrpOp ∧ 𝑤𝑋) ∧ (𝐴𝐺𝑦) ∈ 𝑋) → (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
5958an32s 634 . . . . . . . . . . . . . . . . . . . . 21 (((𝐺 ∈ GrpOp ∧ (𝐴𝐺𝑦) ∈ 𝑋) ∧ 𝑤𝑋) → (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
6059ex 399 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ GrpOp ∧ (𝐴𝐺𝑦) ∈ 𝑋) → (𝑤𝑋 → (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋))))
6145, 60syldan 581 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ GrpOp ∧ (𝐴𝑋𝑦𝑋)) → (𝑤𝑋 → (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋))))
6261ad2ant2rl 746 . . . . . . . . . . . . . . . . . 18 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) → (𝑤𝑋 → (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋))))
6362imp 395 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) ∧ 𝑤𝑋) → (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
6414grpoidinvlem1 27685 . . . . . . . . . . . . . . . . 17 (((𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)) ∧ ((𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 ∧ ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)
6563, 64sylan 571 . . . . . . . . . . . . . . . 16 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) ∧ 𝑤𝑋) ∧ ((𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 ∧ ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)
6665exp43 425 . . . . . . . . . . . . . . 15 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) → (𝑤𝑋 → ((𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈))))
6766rexlimdv 3216 . . . . . . . . . . . . . 14 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) → (∃𝑤𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
6856, 67syl5 34 . . . . . . . . . . . . 13 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) → (((𝐴𝐺𝑦) ∈ 𝑋𝜓) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
6946, 68mpand 678 . . . . . . . . . . . 12 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) → (𝜓 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
7069exp32 409 . . . . . . . . . . 11 ((𝐺 ∈ GrpOp ∧ 𝑈𝑋) → (𝜑 → ((𝐴𝑋𝑦𝑋) → (𝜓 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))))
7170com34 91 . . . . . . . . . 10 ((𝐺 ∈ GrpOp ∧ 𝑈𝑋) → (𝜑 → (𝜓 → ((𝐴𝑋𝑦𝑋) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))))
7271imp32 407 . . . . . . . . 9 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) → ((𝐴𝑋𝑦𝑋) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
7372impl 445 . . . . . . . 8 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈))
7473adantr 468 . . . . . . 7 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈))
7544, 74mpd 15 . . . . . 6 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)
7628, 75eqtr3d 2840 . . . . 5 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝐴𝐺𝑦) = 𝑈)
7776ex 399 . . . 4 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → ((𝑦𝐺𝐴) = 𝑈 → (𝐴𝐺𝑦) = 𝑈))
7877ancld 542 . . 3 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → ((𝑦𝐺𝐴) = 𝑈 → ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈)))
7978reximdva 3202 . 2 ((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) → (∃𝑦𝑋 (𝑦𝐺𝐴) = 𝑈 → ∃𝑦𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈)))
8013, 79mpd 15 1 ((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) → ∃𝑦𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1637  wcel 2156  wral 3094  wrex 3095  ran crn 5310  (class class class)co 6872  GrpOpcgr 27670
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2782  ax-sep 4973  ax-nul 4981  ax-pr 5094  ax-un 7177
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2791  df-cleq 2797  df-clel 2800  df-nfc 2935  df-ral 3099  df-rex 3100  df-rab 3103  df-v 3391  df-sbc 3632  df-csb 3727  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-nul 4115  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375  df-uni 4629  df-iun 4712  df-br 4843  df-opab 4905  df-mpt 4922  df-id 5217  df-xp 5315  df-rel 5316  df-cnv 5317  df-co 5318  df-dm 5319  df-rn 5320  df-iota 6062  df-fun 6101  df-fn 6102  df-f 6103  df-fo 6105  df-fv 6107  df-ov 6875  df-grpo 27674
This theorem is referenced by:  grpoidinv  27689
  Copyright terms: Public domain W3C validator