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

Theorem grpoidinvlem3 28292
Description: Lemma for grpoidinv 28294. (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 7156 . . . . . . . . 9 (𝑧 = 𝑦 → (𝑧𝐺𝑥) = (𝑦𝐺𝑥))
32eqeq1d 2826 . . . . . . . 8 (𝑧 = 𝑦 → ((𝑧𝐺𝑥) = 𝑈 ↔ (𝑦𝐺𝑥) = 𝑈))
43cbvrexvw 3435 . . . . . . 7 (∃𝑧𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∃𝑦𝑋 (𝑦𝐺𝑥) = 𝑈)
54ralbii 3160 . . . . . 6 (∀𝑥𝑋𝑧𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∀𝑥𝑋𝑦𝑋 (𝑦𝐺𝑥) = 𝑈)
61, 5bitri 278 . . . . 5 (𝜓 ↔ ∀𝑥𝑋𝑦𝑋 (𝑦𝐺𝑥) = 𝑈)
7 oveq2 7157 . . . . . . . 8 (𝑥 = 𝐴 → (𝑦𝐺𝑥) = (𝑦𝐺𝐴))
87eqeq1d 2826 . . . . . . 7 (𝑥 = 𝐴 → ((𝑦𝐺𝑥) = 𝑈 ↔ (𝑦𝐺𝐴) = 𝑈))
98rexbidv 3289 . . . . . 6 (𝑥 = 𝐴 → (∃𝑦𝑋 (𝑦𝐺𝑥) = 𝑈 ↔ ∃𝑦𝑋 (𝑦𝐺𝐴) = 𝑈))
109rspccva 3608 . . . . 5 ((∀𝑥𝑋𝑦𝑋 (𝑦𝐺𝑥) = 𝑈𝐴𝑋) → ∃𝑦𝑋 (𝑦𝐺𝐴) = 𝑈)
116, 10sylanb 584 . . . 4 ((𝜓𝐴𝑋) → ∃𝑦𝑋 (𝑦𝐺𝐴) = 𝑈)
1211adantll 713 . . 3 (((𝜑𝜓) ∧ 𝐴𝑋) → ∃𝑦𝑋 (𝑦𝐺𝐴) = 𝑈)
1312adantll 713 . 2 ((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) → ∃𝑦𝑋 (𝑦𝐺𝐴) = 𝑈)
14 grpfo.1 . . . . . . . . . . . 12 𝑋 = ran 𝐺
1514grpocl 28286 . . . . . . . . . . 11 ((𝐺 ∈ GrpOp ∧ 𝐴𝑋𝑦𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
16153expa 1115 . . . . . . . . . 10 (((𝐺 ∈ GrpOp ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
1716adantllr 718 . . . . . . . . 9 ((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
1817adantllr 718 . . . . . . . 8 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
19 grpidinvlem3.2 . . . . . . . . . . 11 (𝜑 ↔ ∀𝑥𝑋 (𝑈𝐺𝑥) = 𝑥)
2019biimpi 219 . . . . . . . . . 10 (𝜑 → ∀𝑥𝑋 (𝑈𝐺𝑥) = 𝑥)
2120ad2antrl 727 . . . . . . . . 9 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) → ∀𝑥𝑋 (𝑈𝐺𝑥) = 𝑥)
2221ad2antrr 725 . . . . . . . 8 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → ∀𝑥𝑋 (𝑈𝐺𝑥) = 𝑥)
23 oveq2 7157 . . . . . . . . . 10 (𝑥 = (𝐴𝐺𝑦) → (𝑈𝐺𝑥) = (𝑈𝐺(𝐴𝐺𝑦)))
24 id 22 . . . . . . . . . 10 (𝑥 = (𝐴𝐺𝑦) → 𝑥 = (𝐴𝐺𝑦))
2523, 24eqeq12d 2840 . . . . . . . . 9 (𝑥 = (𝐴𝐺𝑦) → ((𝑈𝐺𝑥) = 𝑥 ↔ (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦)))
2625rspcva 3607 . . . . . . . 8 (((𝐴𝐺𝑦) ∈ 𝑋 ∧ ∀𝑥𝑋 (𝑈𝐺𝑥) = 𝑥) → (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
2718, 22, 26syl2anc 587 . . . . . . 7 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
2827adantr 484 . . . . . 6 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
29 pm3.22 463 . . . . . . . . . . . 12 (((𝑦𝑋𝐴𝑋) ∧ 𝐺 ∈ GrpOp) → (𝐺 ∈ GrpOp ∧ (𝑦𝑋𝐴𝑋)))
3029an31s 653 . . . . . . . . . . 11 (((𝐺 ∈ GrpOp ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝐺 ∈ GrpOp ∧ (𝑦𝑋𝐴𝑋)))
3130adantllr 718 . . . . . . . . . 10 ((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝐺 ∈ GrpOp ∧ (𝑦𝑋𝐴𝑋)))
3231adantllr 718 . . . . . . . . 9 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝐺 ∈ GrpOp ∧ (𝑦𝑋𝐴𝑋)))
3332adantr 484 . . . . . . . 8 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝐺 ∈ GrpOp ∧ (𝑦𝑋𝐴𝑋)))
34 oveq2 7157 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑈𝐺𝑥) = (𝑈𝐺𝑦))
35 id 22 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦𝑥 = 𝑦)
3634, 35eqeq12d 2840 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → ((𝑈𝐺𝑥) = 𝑥 ↔ (𝑈𝐺𝑦) = 𝑦))
3736rspccva 3608 . . . . . . . . . . . . 13 ((∀𝑥𝑋 (𝑈𝐺𝑥) = 𝑥𝑦𝑋) → (𝑈𝐺𝑦) = 𝑦)
3819, 37sylanb 584 . . . . . . . . . . . 12 ((𝜑𝑦𝑋) → (𝑈𝐺𝑦) = 𝑦)
3938adantlr 714 . . . . . . . . . . 11 (((𝜑𝜓) ∧ 𝑦𝑋) → (𝑈𝐺𝑦) = 𝑦)
4039adantlr 714 . . . . . . . . . 10 ((((𝜑𝜓) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝑈𝐺𝑦) = 𝑦)
4140adantlll 717 . . . . . . . . 9 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝑈𝐺𝑦) = 𝑦)
4241anim1i 617 . . . . . . . 8 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → ((𝑈𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝐴) = 𝑈))
4314grpoidinvlem2 28291 . . . . . . . 8 (((𝐺 ∈ GrpOp ∧ (𝑦𝑋𝐴𝑋)) ∧ ((𝑈𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝐴) = 𝑈)) → ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
4433, 42, 43syl2anc 587 . . . . . . 7 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
45153expb 1117 . . . . . . . . . . . . . 14 ((𝐺 ∈ GrpOp ∧ (𝐴𝑋𝑦𝑋)) → (𝐴𝐺𝑦) ∈ 𝑋)
4645ad2ant2rl 748 . . . . . . . . . . . . 13 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) → (𝐴𝐺𝑦) ∈ 𝑋)
47 oveq1 7156 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑤 → (𝑧𝐺𝑥) = (𝑤𝐺𝑥))
4847eqeq1d 2826 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑤 → ((𝑧𝐺𝑥) = 𝑈 ↔ (𝑤𝐺𝑥) = 𝑈))
4948cbvrexvw 3435 . . . . . . . . . . . . . . . . 17 (∃𝑧𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∃𝑤𝑋 (𝑤𝐺𝑥) = 𝑈)
5049ralbii 3160 . . . . . . . . . . . . . . . 16 (∀𝑥𝑋𝑧𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∀𝑥𝑋𝑤𝑋 (𝑤𝐺𝑥) = 𝑈)
511, 50bitri 278 . . . . . . . . . . . . . . 15 (𝜓 ↔ ∀𝑥𝑋𝑤𝑋 (𝑤𝐺𝑥) = 𝑈)
52 oveq2 7157 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝐴𝐺𝑦) → (𝑤𝐺𝑥) = (𝑤𝐺(𝐴𝐺𝑦)))
5352eqeq1d 2826 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝐴𝐺𝑦) → ((𝑤𝐺𝑥) = 𝑈 ↔ (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈))
5453rexbidv 3289 . . . . . . . . . . . . . . . 16 (𝑥 = (𝐴𝐺𝑦) → (∃𝑤𝑋 (𝑤𝐺𝑥) = 𝑈 ↔ ∃𝑤𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈))
5554rspcva 3607 . . . . . . . . . . . . . . 15 (((𝐴𝐺𝑦) ∈ 𝑋 ∧ ∀𝑥𝑋𝑤𝑋 (𝑤𝐺𝑥) = 𝑈) → ∃𝑤𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈)
5651, 55sylan2b 596 . . . . . . . . . . . . . 14 (((𝐴𝐺𝑦) ∈ 𝑋𝜓) → ∃𝑤𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈)
57 anass 472 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐺 ∈ GrpOp ∧ 𝑤𝑋) ∧ (𝐴𝐺𝑦) ∈ 𝑋) ↔ (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
5857biimpi 219 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐺 ∈ GrpOp ∧ 𝑤𝑋) ∧ (𝐴𝐺𝑦) ∈ 𝑋) → (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
5958an32s 651 . . . . . . . . . . . . . . . . . . . . 21 (((𝐺 ∈ GrpOp ∧ (𝐴𝐺𝑦) ∈ 𝑋) ∧ 𝑤𝑋) → (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
6059ex 416 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ GrpOp ∧ (𝐴𝐺𝑦) ∈ 𝑋) → (𝑤𝑋 → (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋))))
6145, 60syldan 594 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ GrpOp ∧ (𝐴𝑋𝑦𝑋)) → (𝑤𝑋 → (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋))))
6261ad2ant2rl 748 . . . . . . . . . . . . . . . . . 18 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) → (𝑤𝑋 → (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋))))
6362imp 410 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) ∧ 𝑤𝑋) → (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
6414grpoidinvlem1 28290 . . . . . . . . . . . . . . . . 17 (((𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)) ∧ ((𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 ∧ ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)
6563, 64sylan 583 . . . . . . . . . . . . . . . 16 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) ∧ 𝑤𝑋) ∧ ((𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 ∧ ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)
6665exp43 440 . . . . . . . . . . . . . . 15 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) → (𝑤𝑋 → ((𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈))))
6766rexlimdv 3275 . . . . . . . . . . . . . 14 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) → (∃𝑤𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
6856, 67syl5 34 . . . . . . . . . . . . 13 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) → (((𝐴𝐺𝑦) ∈ 𝑋𝜓) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
6946, 68mpand 694 . . . . . . . . . . . 12 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) → (𝜓 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
7069exp32 424 . . . . . . . . . . 11 ((𝐺 ∈ GrpOp ∧ 𝑈𝑋) → (𝜑 → ((𝐴𝑋𝑦𝑋) → (𝜓 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))))
7170com34 91 . . . . . . . . . 10 ((𝐺 ∈ GrpOp ∧ 𝑈𝑋) → (𝜑 → (𝜓 → ((𝐴𝑋𝑦𝑋) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))))
7271imp32 422 . . . . . . . . 9 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) → ((𝐴𝑋𝑦𝑋) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
7372impl 459 . . . . . . . 8 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈))
7473adantr 484 . . . . . . 7 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈))
7544, 74mpd 15 . . . . . 6 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)
7628, 75eqtr3d 2861 . . . . 5 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝐴𝐺𝑦) = 𝑈)
7776ex 416 . . . 4 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → ((𝑦𝐺𝐴) = 𝑈 → (𝐴𝐺𝑦) = 𝑈))
7877ancld 554 . . 3 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → ((𝑦𝐺𝐴) = 𝑈 → ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈)))
7978reximdva 3266 . 2 ((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) → (∃𝑦𝑋 (𝑦𝐺𝐴) = 𝑈 → ∃𝑦𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈)))
8013, 79mpd 15 1 ((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) → ∃𝑦𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wcel 2115  wral 3133  wrex 3134  ran crn 5543  (class class class)co 7149  GrpOpcgr 28275
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 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5189  ax-nul 5196  ax-pr 5317  ax-un 7455
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 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5447  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-fo 6349  df-fv 6351  df-ov 7152  df-grpo 28279
This theorem is referenced by:  grpoidinv  28294
  Copyright terms: Public domain W3C validator