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

Theorem grpoidinvlem3 27206
Description: Lemma for grpoidinv 27208. (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 6611 . . . . . . . . 9 (𝑧 = 𝑦 → (𝑧𝐺𝑥) = (𝑦𝐺𝑥))
32eqeq1d 2623 . . . . . . . 8 (𝑧 = 𝑦 → ((𝑧𝐺𝑥) = 𝑈 ↔ (𝑦𝐺𝑥) = 𝑈))
43cbvrexv 3160 . . . . . . 7 (∃𝑧𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∃𝑦𝑋 (𝑦𝐺𝑥) = 𝑈)
54ralbii 2974 . . . . . 6 (∀𝑥𝑋𝑧𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∀𝑥𝑋𝑦𝑋 (𝑦𝐺𝑥) = 𝑈)
61, 5bitri 264 . . . . 5 (𝜓 ↔ ∀𝑥𝑋𝑦𝑋 (𝑦𝐺𝑥) = 𝑈)
7 oveq2 6612 . . . . . . . 8 (𝑥 = 𝐴 → (𝑦𝐺𝑥) = (𝑦𝐺𝐴))
87eqeq1d 2623 . . . . . . 7 (𝑥 = 𝐴 → ((𝑦𝐺𝑥) = 𝑈 ↔ (𝑦𝐺𝐴) = 𝑈))
98rexbidv 3045 . . . . . 6 (𝑥 = 𝐴 → (∃𝑦𝑋 (𝑦𝐺𝑥) = 𝑈 ↔ ∃𝑦𝑋 (𝑦𝐺𝐴) = 𝑈))
109rspccva 3294 . . . . 5 ((∀𝑥𝑋𝑦𝑋 (𝑦𝐺𝑥) = 𝑈𝐴𝑋) → ∃𝑦𝑋 (𝑦𝐺𝐴) = 𝑈)
116, 10sylanb 489 . . . 4 ((𝜓𝐴𝑋) → ∃𝑦𝑋 (𝑦𝐺𝐴) = 𝑈)
1211adantll 749 . . 3 (((𝜑𝜓) ∧ 𝐴𝑋) → ∃𝑦𝑋 (𝑦𝐺𝐴) = 𝑈)
1312adantll 749 . 2 ((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) → ∃𝑦𝑋 (𝑦𝐺𝐴) = 𝑈)
14 grpfo.1 . . . . . . . . . . . 12 𝑋 = ran 𝐺
1514grpocl 27200 . . . . . . . . . . 11 ((𝐺 ∈ GrpOp ∧ 𝐴𝑋𝑦𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
16153expa 1262 . . . . . . . . . 10 (((𝐺 ∈ GrpOp ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
1716adantllr 754 . . . . . . . . 9 ((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
1817adantllr 754 . . . . . . . 8 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝐴𝐺𝑦) ∈ 𝑋)
19 grpidinvlem3.2 . . . . . . . . . . 11 (𝜑 ↔ ∀𝑥𝑋 (𝑈𝐺𝑥) = 𝑥)
2019biimpi 206 . . . . . . . . . 10 (𝜑 → ∀𝑥𝑋 (𝑈𝐺𝑥) = 𝑥)
2120ad2antrl 763 . . . . . . . . 9 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) → ∀𝑥𝑋 (𝑈𝐺𝑥) = 𝑥)
2221ad2antrr 761 . . . . . . . 8 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → ∀𝑥𝑋 (𝑈𝐺𝑥) = 𝑥)
23 oveq2 6612 . . . . . . . . . 10 (𝑥 = (𝐴𝐺𝑦) → (𝑈𝐺𝑥) = (𝑈𝐺(𝐴𝐺𝑦)))
24 id 22 . . . . . . . . . 10 (𝑥 = (𝐴𝐺𝑦) → 𝑥 = (𝐴𝐺𝑦))
2523, 24eqeq12d 2636 . . . . . . . . 9 (𝑥 = (𝐴𝐺𝑦) → ((𝑈𝐺𝑥) = 𝑥 ↔ (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦)))
2625rspcva 3293 . . . . . . . 8 (((𝐴𝐺𝑦) ∈ 𝑋 ∧ ∀𝑥𝑋 (𝑈𝐺𝑥) = 𝑥) → (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
2718, 22, 26syl2anc 692 . . . . . . 7 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
2827adantr 481 . . . . . 6 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝑈𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
29 pm3.22 465 . . . . . . . . . . . 12 (((𝑦𝑋𝐴𝑋) ∧ 𝐺 ∈ GrpOp) → (𝐺 ∈ GrpOp ∧ (𝑦𝑋𝐴𝑋)))
3029an31s 847 . . . . . . . . . . 11 (((𝐺 ∈ GrpOp ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝐺 ∈ GrpOp ∧ (𝑦𝑋𝐴𝑋)))
3130adantllr 754 . . . . . . . . . 10 ((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝐺 ∈ GrpOp ∧ (𝑦𝑋𝐴𝑋)))
3231adantllr 754 . . . . . . . . 9 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝐺 ∈ GrpOp ∧ (𝑦𝑋𝐴𝑋)))
3332adantr 481 . . . . . . . 8 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝐺 ∈ GrpOp ∧ (𝑦𝑋𝐴𝑋)))
34 oveq2 6612 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑈𝐺𝑥) = (𝑈𝐺𝑦))
35 id 22 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦𝑥 = 𝑦)
3634, 35eqeq12d 2636 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → ((𝑈𝐺𝑥) = 𝑥 ↔ (𝑈𝐺𝑦) = 𝑦))
3736rspccva 3294 . . . . . . . . . . . . 13 ((∀𝑥𝑋 (𝑈𝐺𝑥) = 𝑥𝑦𝑋) → (𝑈𝐺𝑦) = 𝑦)
3819, 37sylanb 489 . . . . . . . . . . . 12 ((𝜑𝑦𝑋) → (𝑈𝐺𝑦) = 𝑦)
3938adantlr 750 . . . . . . . . . . 11 (((𝜑𝜓) ∧ 𝑦𝑋) → (𝑈𝐺𝑦) = 𝑦)
4039adantlr 750 . . . . . . . . . 10 ((((𝜑𝜓) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝑈𝐺𝑦) = 𝑦)
4140adantlll 753 . . . . . . . . 9 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (𝑈𝐺𝑦) = 𝑦)
4241anim1i 591 . . . . . . . 8 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → ((𝑈𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝐴) = 𝑈))
4314grpoidinvlem2 27205 . . . . . . . 8 (((𝐺 ∈ GrpOp ∧ (𝑦𝑋𝐴𝑋)) ∧ ((𝑈𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝐴) = 𝑈)) → ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
4433, 42, 43syl2anc 692 . . . . . . 7 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))
45153expb 1263 . . . . . . . . . . . . . 14 ((𝐺 ∈ GrpOp ∧ (𝐴𝑋𝑦𝑋)) → (𝐴𝐺𝑦) ∈ 𝑋)
4645ad2ant2rl 784 . . . . . . . . . . . . 13 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) → (𝐴𝐺𝑦) ∈ 𝑋)
47 oveq1 6611 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑤 → (𝑧𝐺𝑥) = (𝑤𝐺𝑥))
4847eqeq1d 2623 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑤 → ((𝑧𝐺𝑥) = 𝑈 ↔ (𝑤𝐺𝑥) = 𝑈))
4948cbvrexv 3160 . . . . . . . . . . . . . . . . 17 (∃𝑧𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∃𝑤𝑋 (𝑤𝐺𝑥) = 𝑈)
5049ralbii 2974 . . . . . . . . . . . . . . . 16 (∀𝑥𝑋𝑧𝑋 (𝑧𝐺𝑥) = 𝑈 ↔ ∀𝑥𝑋𝑤𝑋 (𝑤𝐺𝑥) = 𝑈)
511, 50bitri 264 . . . . . . . . . . . . . . 15 (𝜓 ↔ ∀𝑥𝑋𝑤𝑋 (𝑤𝐺𝑥) = 𝑈)
52 oveq2 6612 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝐴𝐺𝑦) → (𝑤𝐺𝑥) = (𝑤𝐺(𝐴𝐺𝑦)))
5352eqeq1d 2623 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝐴𝐺𝑦) → ((𝑤𝐺𝑥) = 𝑈 ↔ (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈))
5453rexbidv 3045 . . . . . . . . . . . . . . . 16 (𝑥 = (𝐴𝐺𝑦) → (∃𝑤𝑋 (𝑤𝐺𝑥) = 𝑈 ↔ ∃𝑤𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈))
5554rspcva 3293 . . . . . . . . . . . . . . 15 (((𝐴𝐺𝑦) ∈ 𝑋 ∧ ∀𝑥𝑋𝑤𝑋 (𝑤𝐺𝑥) = 𝑈) → ∃𝑤𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈)
5651, 55sylan2b 492 . . . . . . . . . . . . . 14 (((𝐴𝐺𝑦) ∈ 𝑋𝜓) → ∃𝑤𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈)
57 anass 680 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐺 ∈ GrpOp ∧ 𝑤𝑋) ∧ (𝐴𝐺𝑦) ∈ 𝑋) ↔ (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
5857biimpi 206 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐺 ∈ GrpOp ∧ 𝑤𝑋) ∧ (𝐴𝐺𝑦) ∈ 𝑋) → (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
5958an32s 845 . . . . . . . . . . . . . . . . . . . . 21 (((𝐺 ∈ GrpOp ∧ (𝐴𝐺𝑦) ∈ 𝑋) ∧ 𝑤𝑋) → (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
6059ex 450 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ GrpOp ∧ (𝐴𝐺𝑦) ∈ 𝑋) → (𝑤𝑋 → (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋))))
6145, 60syldan 487 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ GrpOp ∧ (𝐴𝑋𝑦𝑋)) → (𝑤𝑋 → (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋))))
6261ad2ant2rl 784 . . . . . . . . . . . . . . . . . 18 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) → (𝑤𝑋 → (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋))))
6362imp 445 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) ∧ 𝑤𝑋) → (𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)))
6414grpoidinvlem1 27204 . . . . . . . . . . . . . . . . 17 (((𝐺 ∈ GrpOp ∧ (𝑤𝑋 ∧ (𝐴𝐺𝑦) ∈ 𝑋)) ∧ ((𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 ∧ ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)
6563, 64sylan 488 . . . . . . . . . . . . . . . 16 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) ∧ 𝑤𝑋) ∧ ((𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 ∧ ((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦))) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)
6665exp43 639 . . . . . . . . . . . . . . 15 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) → (𝑤𝑋 → ((𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈))))
6766rexlimdv 3023 . . . . . . . . . . . . . 14 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) → (∃𝑤𝑋 (𝑤𝐺(𝐴𝐺𝑦)) = 𝑈 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
6856, 67syl5 34 . . . . . . . . . . . . 13 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) → (((𝐴𝐺𝑦) ∈ 𝑋𝜓) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
6946, 68mpand 710 . . . . . . . . . . . 12 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑 ∧ (𝐴𝑋𝑦𝑋))) → (𝜓 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
7069exp32 630 . . . . . . . . . . 11 ((𝐺 ∈ GrpOp ∧ 𝑈𝑋) → (𝜑 → ((𝐴𝑋𝑦𝑋) → (𝜓 → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))))
7170com34 91 . . . . . . . . . 10 ((𝐺 ∈ GrpOp ∧ 𝑈𝑋) → (𝜑 → (𝜓 → ((𝐴𝑋𝑦𝑋) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))))
7271imp32 449 . . . . . . . . 9 (((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) → ((𝐴𝑋𝑦𝑋) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)))
7372impl 649 . . . . . . . 8 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈))
7473adantr 481 . . . . . . 7 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (((𝐴𝐺𝑦)𝐺(𝐴𝐺𝑦)) = (𝐴𝐺𝑦) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈))
7544, 74mpd 15 . . . . . 6 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝑈𝐺(𝐴𝐺𝑦)) = 𝑈)
7628, 75eqtr3d 2657 . . . . 5 ((((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) ∧ (𝑦𝐺𝐴) = 𝑈) → (𝐴𝐺𝑦) = 𝑈)
7776ex 450 . . . 4 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → ((𝑦𝐺𝐴) = 𝑈 → (𝐴𝐺𝑦) = 𝑈))
7877ancld 575 . . 3 (((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) ∧ 𝑦𝑋) → ((𝑦𝐺𝐴) = 𝑈 → ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈)))
7978reximdva 3011 . 2 ((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) → (∃𝑦𝑋 (𝑦𝐺𝐴) = 𝑈 → ∃𝑦𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈)))
8013, 79mpd 15 1 ((((𝐺 ∈ GrpOp ∧ 𝑈𝑋) ∧ (𝜑𝜓)) ∧ 𝐴𝑋) → ∃𝑦𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  wral 2907  wrex 2908  ran crn 5075  (class class class)co 6604  GrpOpcgr 27189
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-fo 5853  df-fv 5855  df-ov 6607  df-grpo 27193
This theorem is referenced by:  grpoidinv  27208
  Copyright terms: Public domain W3C validator