Metamath Proof Explorer

Theorem grpoidinvlem3

Description: Lemma for grpoidinv . (Contributed by NM, 11-Oct-2006) (New usage is discouraged.)

Ref Expression
Hypotheses grpfo.1 ⊢ 𝑋 = ran 𝐺
grpidinvlem3.2 ⊢ ( 𝜑 ↔ ∀ 𝑥 ∈ 𝑋 ( 𝑈 𝐺 𝑥 ) = 𝑥 )
grpidinvlem3.3 ⊢ ( 𝜓 ↔ ∀ 𝑥 ∈ 𝑋 ∃ 𝑧 ∈ 𝑋 ( 𝑧 𝐺 𝑥 ) = 𝑈 )
Assertion grpoidinvlem3 ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ∧ 𝐴 ∈ 𝑋 ) → ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) )

Proof

Step Hyp Ref Expression
1 grpfo.1 ⊢ 𝑋 = ran 𝐺
2 grpidinvlem3.2 ⊢ ( 𝜑 ↔ ∀ 𝑥 ∈ 𝑋 ( 𝑈 𝐺 𝑥 ) = 𝑥 )
3 grpidinvlem3.3 ⊢ ( 𝜓 ↔ ∀ 𝑥 ∈ 𝑋 ∃ 𝑧 ∈ 𝑋 ( 𝑧 𝐺 𝑥 ) = 𝑈 )
4 oveq1 ⊢ ( 𝑧 = 𝑦 → ( 𝑧 𝐺 𝑥 ) = ( 𝑦 𝐺 𝑥 ) )
5 4 eqeq1d ⊢ ( 𝑧 = 𝑦 → ( ( 𝑧 𝐺 𝑥 ) = 𝑈 ↔ ( 𝑦 𝐺 𝑥 ) = 𝑈 ) )
6 5 cbvrexvw ⊢ ( ∃ 𝑧 ∈ 𝑋 ( 𝑧 𝐺 𝑥 ) = 𝑈 ↔ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 )
7 6 ralbii ⊢ ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑧 ∈ 𝑋 ( 𝑧 𝐺 𝑥 ) = 𝑈 ↔ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 )
8 3 7 bitri ⊢ ( 𝜓 ↔ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 )
9 oveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑦 𝐺 𝑥 ) = ( 𝑦 𝐺 𝐴 ) )
10 9 eqeq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑦 𝐺 𝑥 ) = 𝑈 ↔ ( 𝑦 𝐺 𝐴 ) = 𝑈 ) )
11 10 rexbidv ⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ↔ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝐴 ) = 𝑈 ) )
12 11 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ∧ 𝐴 ∈ 𝑋 ) → ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝐴 ) = 𝑈 )
13 8 12 sylanb ⊢ ( ( 𝜓 ∧ 𝐴 ∈ 𝑋 ) → ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝐴 ) = 𝑈 )
14 13 adantll ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝐴 ∈ 𝑋 ) → ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝐴 ) = 𝑈 )
15 14 adantll ⊢ ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ∧ 𝐴 ∈ 𝑋 ) → ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝐴 ) = 𝑈 )
16 1 grpocl ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐴 𝐺 𝑦 ) ∈ 𝑋 )
17 16 3expa ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝐴 𝐺 𝑦 ) ∈ 𝑋 )
18 17 adantllr ⊢ ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝐴 𝐺 𝑦 ) ∈ 𝑋 )
19 18 adantllr ⊢ ( ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝐴 𝐺 𝑦 ) ∈ 𝑋 )
20 2 biimpi ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ( 𝑈 𝐺 𝑥 ) = 𝑥 )
21 20 ad2antrl ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝜑 ∧ 𝜓 ) ) → ∀ 𝑥 ∈ 𝑋 ( 𝑈 𝐺 𝑥 ) = 𝑥 )
22 21 ad2antrr ⊢ ( ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ∀ 𝑥 ∈ 𝑋 ( 𝑈 𝐺 𝑥 ) = 𝑥 )
23 oveq2 ⊢ ( 𝑥 = ( 𝐴 𝐺 𝑦 ) → ( 𝑈 𝐺 𝑥 ) = ( 𝑈 𝐺 ( 𝐴 𝐺 𝑦 ) ) )
24 id ⊢ ( 𝑥 = ( 𝐴 𝐺 𝑦 ) → 𝑥 = ( 𝐴 𝐺 𝑦 ) )
25 23 24 eqeq12d ⊢ ( 𝑥 = ( 𝐴 𝐺 𝑦 ) → ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ↔ ( 𝑈 𝐺 ( 𝐴 𝐺 𝑦 ) ) = ( 𝐴 𝐺 𝑦 ) ) )
26 25 rspcva ⊢ ( ( ( 𝐴 𝐺 𝑦 ) ∈ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑈 𝐺 𝑥 ) = 𝑥 ) → ( 𝑈 𝐺 ( 𝐴 𝐺 𝑦 ) ) = ( 𝐴 𝐺 𝑦 ) )
27 19 22 26 syl2anc ⊢ ( ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑈 𝐺 ( 𝐴 𝐺 𝑦 ) ) = ( 𝐴 𝐺 𝑦 ) )
28 27 adantr ⊢ ( ( ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑦 𝐺 𝐴 ) = 𝑈 ) → ( 𝑈 𝐺 ( 𝐴 𝐺 𝑦 ) ) = ( 𝐴 𝐺 𝑦 ) )
29 pm3.22 ⊢ ( ( ( 𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐺 ∈ GrpOp ) → ( 𝐺 ∈ GrpOp ∧ ( 𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) )
30 29 an31s ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝐺 ∈ GrpOp ∧ ( 𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) )
31 30 adantllr ⊢ ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝐺 ∈ GrpOp ∧ ( 𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) )
32 31 adantllr ⊢ ( ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝐺 ∈ GrpOp ∧ ( 𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) )
33 32 adantr ⊢ ( ( ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑦 𝐺 𝐴 ) = 𝑈 ) → ( 𝐺 ∈ GrpOp ∧ ( 𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) )
34 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑈 𝐺 𝑥 ) = ( 𝑈 𝐺 𝑦 ) )
35 id ⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
36 34 35 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ↔ ( 𝑈 𝐺 𝑦 ) = 𝑦 ) )
37 36 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝑋 ( 𝑈 𝐺 𝑥 ) = 𝑥 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑈 𝐺 𝑦 ) = 𝑦 )
38 2 37 sylanb ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑈 𝐺 𝑦 ) = 𝑦 )
39 38 adantlr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑈 𝐺 𝑦 ) = 𝑦 )
40 39 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑈 𝐺 𝑦 ) = 𝑦 )
41 40 adantlll ⊢ ( ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑈 𝐺 𝑦 ) = 𝑦 )
42 41 anim1i ⊢ ( ( ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑦 𝐺 𝐴 ) = 𝑈 ) → ( ( 𝑈 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝐴 ) = 𝑈 ) )
43 1 grpoidinvlem2 ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ ( 𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( ( 𝑈 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝐴 ) = 𝑈 ) ) → ( ( 𝐴 𝐺 𝑦 ) 𝐺 ( 𝐴 𝐺 𝑦 ) ) = ( 𝐴 𝐺 𝑦 ) )
44 33 42 43 syl2anc ⊢ ( ( ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑦 𝐺 𝐴 ) = 𝑈 ) → ( ( 𝐴 𝐺 𝑦 ) 𝐺 ( 𝐴 𝐺 𝑦 ) ) = ( 𝐴 𝐺 𝑦 ) )
45 16 3expb ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝐴 𝐺 𝑦 ) ∈ 𝑋 )
46 45 ad2ant2rl ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ) → ( 𝐴 𝐺 𝑦 ) ∈ 𝑋 )
47 oveq1 ⊢ ( 𝑧 = 𝑤 → ( 𝑧 𝐺 𝑥 ) = ( 𝑤 𝐺 𝑥 ) )
48 47 eqeq1d ⊢ ( 𝑧 = 𝑤 → ( ( 𝑧 𝐺 𝑥 ) = 𝑈 ↔ ( 𝑤 𝐺 𝑥 ) = 𝑈 ) )
49 48 cbvrexvw ⊢ ( ∃ 𝑧 ∈ 𝑋 ( 𝑧 𝐺 𝑥 ) = 𝑈 ↔ ∃ 𝑤 ∈ 𝑋 ( 𝑤 𝐺 𝑥 ) = 𝑈 )
50 49 ralbii ⊢ ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑧 ∈ 𝑋 ( 𝑧 𝐺 𝑥 ) = 𝑈 ↔ ∀ 𝑥 ∈ 𝑋 ∃ 𝑤 ∈ 𝑋 ( 𝑤 𝐺 𝑥 ) = 𝑈 )
51 3 50 bitri ⊢ ( 𝜓 ↔ ∀ 𝑥 ∈ 𝑋 ∃ 𝑤 ∈ 𝑋 ( 𝑤 𝐺 𝑥 ) = 𝑈 )
52 oveq2 ⊢ ( 𝑥 = ( 𝐴 𝐺 𝑦 ) → ( 𝑤 𝐺 𝑥 ) = ( 𝑤 𝐺 ( 𝐴 𝐺 𝑦 ) ) )
53 52 eqeq1d ⊢ ( 𝑥 = ( 𝐴 𝐺 𝑦 ) → ( ( 𝑤 𝐺 𝑥 ) = 𝑈 ↔ ( 𝑤 𝐺 ( 𝐴 𝐺 𝑦 ) ) = 𝑈 ) )
54 53 rexbidv ⊢ ( 𝑥 = ( 𝐴 𝐺 𝑦 ) → ( ∃ 𝑤 ∈ 𝑋 ( 𝑤 𝐺 𝑥 ) = 𝑈 ↔ ∃ 𝑤 ∈ 𝑋 ( 𝑤 𝐺 ( 𝐴 𝐺 𝑦 ) ) = 𝑈 ) )
55 54 rspcva ⊢ ( ( ( 𝐴 𝐺 𝑦 ) ∈ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑤 ∈ 𝑋 ( 𝑤 𝐺 𝑥 ) = 𝑈 ) → ∃ 𝑤 ∈ 𝑋 ( 𝑤 𝐺 ( 𝐴 𝐺 𝑦 ) ) = 𝑈 )
56 51 55 sylan2b ⊢ ( ( ( 𝐴 𝐺 𝑦 ) ∈ 𝑋 ∧ 𝜓 ) → ∃ 𝑤 ∈ 𝑋 ( 𝑤 𝐺 ( 𝐴 𝐺 𝑦 ) ) = 𝑈 )
57 anass ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝑤 ∈ 𝑋 ) ∧ ( 𝐴 𝐺 𝑦 ) ∈ 𝑋 ) ↔ ( 𝐺 ∈ GrpOp ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝐴 𝐺 𝑦 ) ∈ 𝑋 ) ) )
58 57 biimpi ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝑤 ∈ 𝑋 ) ∧ ( 𝐴 𝐺 𝑦 ) ∈ 𝑋 ) → ( 𝐺 ∈ GrpOp ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝐴 𝐺 𝑦 ) ∈ 𝑋 ) ) )
59 58 an32s ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 𝐺 𝑦 ) ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) → ( 𝐺 ∈ GrpOp ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝐴 𝐺 𝑦 ) ∈ 𝑋 ) ) )
60 59 ex ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 𝐺 𝑦 ) ∈ 𝑋 ) → ( 𝑤 ∈ 𝑋 → ( 𝐺 ∈ GrpOp ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝐴 𝐺 𝑦 ) ∈ 𝑋 ) ) ) )
61 45 60 syldan ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑤 ∈ 𝑋 → ( 𝐺 ∈ GrpOp ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝐴 𝐺 𝑦 ) ∈ 𝑋 ) ) ) )
62 61 ad2ant2rl ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ) → ( 𝑤 ∈ 𝑋 → ( 𝐺 ∈ GrpOp ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝐴 𝐺 𝑦 ) ∈ 𝑋 ) ) ) )
63 62 imp ⊢ ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ) ∧ 𝑤 ∈ 𝑋 ) → ( 𝐺 ∈ GrpOp ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝐴 𝐺 𝑦 ) ∈ 𝑋 ) ) )
64 1 grpoidinvlem1 ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝐴 𝐺 𝑦 ) ∈ 𝑋 ) ) ∧ ( ( 𝑤 𝐺 ( 𝐴 𝐺 𝑦 ) ) = 𝑈 ∧ ( ( 𝐴 𝐺 𝑦 ) 𝐺 ( 𝐴 𝐺 𝑦 ) ) = ( 𝐴 𝐺 𝑦 ) ) ) → ( 𝑈 𝐺 ( 𝐴 𝐺 𝑦 ) ) = 𝑈 )
65 63 64 sylan ⊢ ( ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ) ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑤 𝐺 ( 𝐴 𝐺 𝑦 ) ) = 𝑈 ∧ ( ( 𝐴 𝐺 𝑦 ) 𝐺 ( 𝐴 𝐺 𝑦 ) ) = ( 𝐴 𝐺 𝑦 ) ) ) → ( 𝑈 𝐺 ( 𝐴 𝐺 𝑦 ) ) = 𝑈 )
66 65 exp43 ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ) → ( 𝑤 ∈ 𝑋 → ( ( 𝑤 𝐺 ( 𝐴 𝐺 𝑦 ) ) = 𝑈 → ( ( ( 𝐴 𝐺 𝑦 ) 𝐺 ( 𝐴 𝐺 𝑦 ) ) = ( 𝐴 𝐺 𝑦 ) → ( 𝑈 𝐺 ( 𝐴 𝐺 𝑦 ) ) = 𝑈 ) ) ) )
67 66 rexlimdv ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ) → ( ∃ 𝑤 ∈ 𝑋 ( 𝑤 𝐺 ( 𝐴 𝐺 𝑦 ) ) = 𝑈 → ( ( ( 𝐴 𝐺 𝑦 ) 𝐺 ( 𝐴 𝐺 𝑦 ) ) = ( 𝐴 𝐺 𝑦 ) → ( 𝑈 𝐺 ( 𝐴 𝐺 𝑦 ) ) = 𝑈 ) ) )
68 56 67 syl5 ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ) → ( ( ( 𝐴 𝐺 𝑦 ) ∈ 𝑋 ∧ 𝜓 ) → ( ( ( 𝐴 𝐺 𝑦 ) 𝐺 ( 𝐴 𝐺 𝑦 ) ) = ( 𝐴 𝐺 𝑦 ) → ( 𝑈 𝐺 ( 𝐴 𝐺 𝑦 ) ) = 𝑈 ) ) )
69 46 68 mpand ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ) → ( 𝜓 → ( ( ( 𝐴 𝐺 𝑦 ) 𝐺 ( 𝐴 𝐺 𝑦 ) ) = ( 𝐴 𝐺 𝑦 ) → ( 𝑈 𝐺 ( 𝐴 𝐺 𝑦 ) ) = 𝑈 ) ) )
70 69 exp32 ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋 ) → ( 𝜑 → ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝜓 → ( ( ( 𝐴 𝐺 𝑦 ) 𝐺 ( 𝐴 𝐺 𝑦 ) ) = ( 𝐴 𝐺 𝑦 ) → ( 𝑈 𝐺 ( 𝐴 𝐺 𝑦 ) ) = 𝑈 ) ) ) ) )
71 70 com34 ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋 ) → ( 𝜑 → ( 𝜓 → ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝐴 𝐺 𝑦 ) 𝐺 ( 𝐴 𝐺 𝑦 ) ) = ( 𝐴 𝐺 𝑦 ) → ( 𝑈 𝐺 ( 𝐴 𝐺 𝑦 ) ) = 𝑈 ) ) ) ) )
72 71 imp32 ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝜑 ∧ 𝜓 ) ) → ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝐴 𝐺 𝑦 ) 𝐺 ( 𝐴 𝐺 𝑦 ) ) = ( 𝐴 𝐺 𝑦 ) → ( 𝑈 𝐺 ( 𝐴 𝐺 𝑦 ) ) = 𝑈 ) ) )
73 72 impl ⊢ ( ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝐴 𝐺 𝑦 ) 𝐺 ( 𝐴 𝐺 𝑦 ) ) = ( 𝐴 𝐺 𝑦 ) → ( 𝑈 𝐺 ( 𝐴 𝐺 𝑦 ) ) = 𝑈 ) )
74 73 adantr ⊢ ( ( ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑦 𝐺 𝐴 ) = 𝑈 ) → ( ( ( 𝐴 𝐺 𝑦 ) 𝐺 ( 𝐴 𝐺 𝑦 ) ) = ( 𝐴 𝐺 𝑦 ) → ( 𝑈 𝐺 ( 𝐴 𝐺 𝑦 ) ) = 𝑈 ) )
75 44 74 mpd ⊢ ( ( ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑦 𝐺 𝐴 ) = 𝑈 ) → ( 𝑈 𝐺 ( 𝐴 𝐺 𝑦 ) ) = 𝑈 )
76 28 75 eqtr3d ⊢ ( ( ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑦 𝐺 𝐴 ) = 𝑈 ) → ( 𝐴 𝐺 𝑦 ) = 𝑈 )
77 76 ex ⊢ ( ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑦 𝐺 𝐴 ) = 𝑈 → ( 𝐴 𝐺 𝑦 ) = 𝑈 ) )
78 77 ancld ⊢ ( ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑦 𝐺 𝐴 ) = 𝑈 → ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) ) )
79 78 reximdva ⊢ ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ∧ 𝐴 ∈ 𝑋 ) → ( ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝐴 ) = 𝑈 → ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) ) )
80 15 79 mpd ⊢ ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ∧ 𝐴 ∈ 𝑋 ) → ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) )