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

Theorem grpoidinvlem3 29746
Description: Lemma for grpoidinv 29748. (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 7412 . . . . . . . . 9 (𝑧 = 𝑦 → (𝑧𝐺𝑥) = (𝑦𝐺𝑥))
32eqeq1d 2734 . . . . . . . 8 (𝑧 = 𝑦 → ((𝑧𝐺𝑥) = 𝑈 ↔ (𝑦𝐺𝑥) = 𝑈))
43cbvrexvw 3235 . . . . . . 7 (∃𝑧𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∃𝑦𝑋 (𝑦𝐺𝑥) = 𝑈)
54ralbii 3093 . . . . . 6 (∀𝑥𝑋𝑧𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∀𝑥𝑋𝑦𝑋 (𝑦𝐺𝑥) = 𝑈)
61, 5bitri 274 . . . . 5 (𝜓 ↔ ∀𝑥𝑋𝑦𝑋 (𝑦𝐺𝑥) = 𝑈)
7 oveq2 7413 . . . . . . . 8 (𝑥 = 𝐴 → (𝑦𝐺𝑥) = (𝑦𝐺𝐴))
87eqeq1d 2734 . . . . . . 7 (𝑥 = 𝐴 → ((𝑦𝐺𝑥) = 𝑈 ↔ (𝑦𝐺𝐴) = 𝑈))
98rexbidv 3178 . . . . . 6 (𝑥 = 𝐴 → (∃𝑦𝑋 (𝑦𝐺𝑥) = 𝑈 ↔ ∃𝑦𝑋 (𝑦𝐺𝐴) = 𝑈))
109rspccva 3611 . . . . 5 ((∀𝑥𝑋𝑦𝑋 (𝑦𝐺𝑥) = 𝑈𝐴𝑋) → ∃𝑦𝑋 (𝑦𝐺𝐴) = 𝑈)
116, 10sylanb 581 . . . 4 ((𝜓𝐴𝑋) → ∃𝑦𝑋 (𝑦𝐺𝐴) = 𝑈)
1211adantll 712 . . 3 (((𝜑𝜓) ∧ 𝐴𝑋) → ∃𝑦𝑋 (𝑦𝐺𝐴) = 𝑈)
1312adantll 712 . 2 ((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) → ∃𝑦𝑋 (𝑦𝐺𝐴) = 𝑈)
14 grpfo.1 . . . . . . . . . . . 12 𝑋 = ran 𝐺
1514grpocl 29740 . . . . . . . . . . 11 ((𝐺 ∈ GrpOp ∧ 𝐴𝑋𝑦𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
16153expa 1118 . . . . . . . . . 10 (((𝐺 ∈ GrpOp ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
1716adantllr 717 . . . . . . . . 9 ((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
1817adantllr 717 . . . . . . . 8 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
19 grpidinvlem3.2 . . . . . . . . . . 11 (𝜑 ↔ ∀𝑥𝑋 (𝑈𝐺𝑥) = 𝑥)
2019biimpi 215 . . . . . . . . . 10 (𝜑 → ∀𝑥𝑋 (𝑈𝐺𝑥) = 𝑥)
2120ad2antrl 726 . . . . . . . . 9 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) → ∀𝑥𝑋 (𝑈𝐺𝑥) = 𝑥)
2221ad2antrr 724 . . . . . . . 8 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → ∀𝑥𝑋 (𝑈𝐺𝑥) = 𝑥)
23 oveq2 7413 . . . . . . . . . 10 (𝑥 = (𝐴𝐺𝑦) → (𝑈𝐺𝑥) = (𝑈𝐺(𝐴𝐺𝑦)))
24 id 22 . . . . . . . . . 10 (𝑥 = (𝐴𝐺𝑦) → 𝑥 = (𝐴𝐺𝑦))
2523, 24eqeq12d 2748 . . . . . . . . 9 (𝑥 = (𝐴𝐺𝑦) → ((𝑈𝐺𝑥) = 𝑥 ↔ (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦)))
2625rspcva 3610 . . . . . . . 8 (((𝐴𝐺𝑦) ∈ 𝑋 ∧ ∀𝑥𝑋 (𝑈𝐺𝑥) = 𝑥) → (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
2718, 22, 26syl2anc 584 . . . . . . 7 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
2827adantr 481 . . . . . 6 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
29 pm3.22 460 . . . . . . . . . . . 12 (((𝑦𝑋𝐴𝑋) ∧ 𝐺 ∈ GrpOp) → (𝐺 ∈ GrpOp ∧ (𝑦𝑋𝐴𝑋)))
3029an31s 652 . . . . . . . . . . 11 (((𝐺 ∈ GrpOp ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝐺 ∈ GrpOp ∧ (𝑦𝑋𝐴𝑋)))
3130adantllr 717 . . . . . . . . . 10 ((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝐺 ∈ GrpOp ∧ (𝑦𝑋𝐴𝑋)))
3231adantllr 717 . . . . . . . . 9 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝐺 ∈ GrpOp ∧ (𝑦𝑋𝐴𝑋)))
3332adantr 481 . . . . . . . 8 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝐺 ∈ GrpOp ∧ (𝑦𝑋𝐴𝑋)))
34 oveq2 7413 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑈𝐺𝑥) = (𝑈𝐺𝑦))
35 id 22 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦𝑥 = 𝑦)
3634, 35eqeq12d 2748 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → ((𝑈𝐺𝑥) = 𝑥 ↔ (𝑈𝐺𝑦) = 𝑦))
3736rspccva 3611 . . . . . . . . . . . . 13 ((∀𝑥𝑋 (𝑈𝐺𝑥) = 𝑥𝑦𝑋) → (𝑈𝐺𝑦) = 𝑦)
3819, 37sylanb 581 . . . . . . . . . . . 12 ((𝜑𝑦𝑋) → (𝑈𝐺𝑦) = 𝑦)
3938adantlr 713 . . . . . . . . . . 11 (((𝜑𝜓) ∧ 𝑦𝑋) → (𝑈𝐺𝑦) = 𝑦)
4039adantlr 713 . . . . . . . . . 10 ((((𝜑𝜓) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝑈𝐺𝑦) = 𝑦)
4140adantlll 716 . . . . . . . . 9 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝑈𝐺𝑦) = 𝑦)
4241anim1i 615 . . . . . . . 8 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → ((𝑈𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝐴) = 𝑈))
4314grpoidinvlem2 29745 . . . . . . . 8 (((𝐺 ∈ GrpOp ∧ (𝑦𝑋𝐴𝑋)) ∧ ((𝑈𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝐴) = 𝑈)) → ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
4433, 42, 43syl2anc 584 . . . . . . 7 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
45153expb 1120 . . . . . . . . . . . . . 14 ((𝐺 ∈ GrpOp ∧ (𝐴𝑋𝑦𝑋)) → (𝐴𝐺𝑦) ∈ 𝑋)
4645ad2ant2rl 747 . . . . . . . . . . . . 13 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) → (𝐴𝐺𝑦) ∈ 𝑋)
47 oveq1 7412 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑤 → (𝑧𝐺𝑥) = (𝑤𝐺𝑥))
4847eqeq1d 2734 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑤 → ((𝑧𝐺𝑥) = 𝑈 ↔ (𝑤𝐺𝑥) = 𝑈))
4948cbvrexvw 3235 . . . . . . . . . . . . . . . . 17 (∃𝑧𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∃𝑤𝑋 (𝑤𝐺𝑥) = 𝑈)
5049ralbii 3093 . . . . . . . . . . . . . . . 16 (∀𝑥𝑋𝑧𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∀𝑥𝑋𝑤𝑋 (𝑤𝐺𝑥) = 𝑈)
511, 50bitri 274 . . . . . . . . . . . . . . 15 (𝜓 ↔ ∀𝑥𝑋𝑤𝑋 (𝑤𝐺𝑥) = 𝑈)
52 oveq2 7413 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝐴𝐺𝑦) → (𝑤𝐺𝑥) = (𝑤𝐺(𝐴𝐺𝑦)))
5352eqeq1d 2734 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝐴𝐺𝑦) → ((𝑤𝐺𝑥) = 𝑈 ↔ (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈))
5453rexbidv 3178 . . . . . . . . . . . . . . . 16 (𝑥 = (𝐴𝐺𝑦) → (∃𝑤𝑋 (𝑤𝐺𝑥) = 𝑈 ↔ ∃𝑤𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈))
5554rspcva 3610 . . . . . . . . . . . . . . 15 (((𝐴𝐺𝑦) ∈ 𝑋 ∧ ∀𝑥𝑋𝑤𝑋 (𝑤𝐺𝑥) = 𝑈) → ∃𝑤𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈)
5651, 55sylan2b 594 . . . . . . . . . . . . . 14 (((𝐴𝐺𝑦) ∈ 𝑋𝜓) → ∃𝑤𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈)
57 anass 469 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐺 ∈ GrpOp ∧ 𝑤𝑋) ∧ (𝐴𝐺𝑦) ∈ 𝑋) ↔ (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
5857biimpi 215 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐺 ∈ GrpOp ∧ 𝑤𝑋) ∧ (𝐴𝐺𝑦) ∈ 𝑋) → (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
5958an32s 650 . . . . . . . . . . . . . . . . . . . . 21 (((𝐺 ∈ GrpOp ∧ (𝐴𝐺𝑦) ∈ 𝑋) ∧ 𝑤𝑋) → (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
6059ex 413 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ GrpOp ∧ (𝐴𝐺𝑦) ∈ 𝑋) → (𝑤𝑋 → (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋))))
6145, 60syldan 591 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ GrpOp ∧ (𝐴𝑋𝑦𝑋)) → (𝑤𝑋 → (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋))))
6261ad2ant2rl 747 . . . . . . . . . . . . . . . . . 18 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) → (𝑤𝑋 → (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋))))
6362imp 407 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) ∧ 𝑤𝑋) → (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
6414grpoidinvlem1 29744 . . . . . . . . . . . . . . . . 17 (((𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)) ∧ ((𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 ∧ ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)
6563, 64sylan 580 . . . . . . . . . . . . . . . 16 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) ∧ 𝑤𝑋) ∧ ((𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 ∧ ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)
6665exp43 437 . . . . . . . . . . . . . . 15 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) → (𝑤𝑋 → ((𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈))))
6766rexlimdv 3153 . . . . . . . . . . . . . 14 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) → (∃𝑤𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
6856, 67syl5 34 . . . . . . . . . . . . 13 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) → (((𝐴𝐺𝑦) ∈ 𝑋𝜓) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
6946, 68mpand 693 . . . . . . . . . . . 12 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) → (𝜓 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
7069exp32 421 . . . . . . . . . . 11 ((𝐺 ∈ GrpOp ∧ 𝑈𝑋) → (𝜑 → ((𝐴𝑋𝑦𝑋) → (𝜓 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))))
7170com34 91 . . . . . . . . . 10 ((𝐺 ∈ GrpOp ∧ 𝑈𝑋) → (𝜑 → (𝜓 → ((𝐴𝑋𝑦𝑋) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))))
7271imp32 419 . . . . . . . . 9 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) → ((𝐴𝑋𝑦𝑋) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
7372impl 456 . . . . . . . 8 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈))
7473adantr 481 . . . . . . 7 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈))
7544, 74mpd 15 . . . . . 6 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)
7628, 75eqtr3d 2774 . . . . 5 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝐴𝐺𝑦) = 𝑈)
7776ex 413 . . . 4 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → ((𝑦𝐺𝐴) = 𝑈 → (𝐴𝐺𝑦) = 𝑈))
7877ancld 551 . . 3 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → ((𝑦𝐺𝐴) = 𝑈 → ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈)))
7978reximdva 3168 . 2 ((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) → (∃𝑦𝑋 (𝑦𝐺𝐴) = 𝑈 → ∃𝑦𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈)))
8013, 79mpd 15 1 ((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) → ∃𝑦𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wral 3061  wrex 3070  ran crn 5676  (class class class)co 7405  GrpOpcgr 29729
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7721
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-fo 6546  df-fv 6548  df-ov 7408  df-grpo 29733
This theorem is referenced by:  grpoidinv  29748
  Copyright terms: Public domain W3C validator