# Metamath Proof Explorer

## Theorem grpoidinvlem3

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

Ref Expression
Hypotheses grpfo.1 ${⊢}{X}=\mathrm{ran}{G}$
grpidinvlem3.2 ${⊢}{\phi }↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{U}{G}{x}={x}$
grpidinvlem3.3 ${⊢}{\psi }↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {z}\in {X}\phantom{\rule{.4em}{0ex}}{z}{G}{x}={U}$
Assertion grpoidinvlem3 ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {U}\in {X}\right)\wedge \left({\phi }\wedge {\psi }\right)\right)\wedge {A}\in {X}\right)\to \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{A}={U}\wedge {A}{G}{y}={U}\right)$

### Proof

Step Hyp Ref Expression
1 grpfo.1 ${⊢}{X}=\mathrm{ran}{G}$
2 grpidinvlem3.2 ${⊢}{\phi }↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{U}{G}{x}={x}$
3 grpidinvlem3.3 ${⊢}{\psi }↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {z}\in {X}\phantom{\rule{.4em}{0ex}}{z}{G}{x}={U}$
4 oveq1 ${⊢}{z}={y}\to {z}{G}{x}={y}{G}{x}$
5 4 eqeq1d ${⊢}{z}={y}\to \left({z}{G}{x}={U}↔{y}{G}{x}={U}\right)$
6 5 cbvrexvw ${⊢}\exists {z}\in {X}\phantom{\rule{.4em}{0ex}}{z}{G}{x}={U}↔\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={U}$
7 6 ralbii ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {z}\in {X}\phantom{\rule{.4em}{0ex}}{z}{G}{x}={U}↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={U}$
8 3 7 bitri ${⊢}{\psi }↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={U}$
9 oveq2 ${⊢}{x}={A}\to {y}{G}{x}={y}{G}{A}$
10 9 eqeq1d ${⊢}{x}={A}\to \left({y}{G}{x}={U}↔{y}{G}{A}={U}\right)$
11 10 rexbidv ${⊢}{x}={A}\to \left(\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={U}↔\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{A}={U}\right)$
12 11 rspccva ${⊢}\left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={U}\wedge {A}\in {X}\right)\to \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{A}={U}$
13 8 12 sylanb ${⊢}\left({\psi }\wedge {A}\in {X}\right)\to \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{A}={U}$
14 13 adantll ${⊢}\left(\left({\phi }\wedge {\psi }\right)\wedge {A}\in {X}\right)\to \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{A}={U}$
15 14 adantll ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {U}\in {X}\right)\wedge \left({\phi }\wedge {\psi }\right)\right)\wedge {A}\in {X}\right)\to \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{A}={U}$
16 1 grpocl ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\wedge {y}\in {X}\right)\to {A}{G}{y}\in {X}$
17 16 3expa ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\wedge {y}\in {X}\right)\to {A}{G}{y}\in {X}$
18 17 adantllr ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {U}\in {X}\right)\wedge {A}\in {X}\right)\wedge {y}\in {X}\right)\to {A}{G}{y}\in {X}$
19 18 adantllr ${⊢}\left(\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {U}\in {X}\right)\wedge \left({\phi }\wedge {\psi }\right)\right)\wedge {A}\in {X}\right)\wedge {y}\in {X}\right)\to {A}{G}{y}\in {X}$
20 2 biimpi ${⊢}{\phi }\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{U}{G}{x}={x}$
21 20 ad2antrl ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {U}\in {X}\right)\wedge \left({\phi }\wedge {\psi }\right)\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{U}{G}{x}={x}$
22 21 ad2antrr ${⊢}\left(\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {U}\in {X}\right)\wedge \left({\phi }\wedge {\psi }\right)\right)\wedge {A}\in {X}\right)\wedge {y}\in {X}\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{U}{G}{x}={x}$
23 oveq2 ${⊢}{x}={A}{G}{y}\to {U}{G}{x}={U}{G}\left({A}{G}{y}\right)$
24 id ${⊢}{x}={A}{G}{y}\to {x}={A}{G}{y}$
25 23 24 eqeq12d ${⊢}{x}={A}{G}{y}\to \left({U}{G}{x}={x}↔{U}{G}\left({A}{G}{y}\right)={A}{G}{y}\right)$
26 25 rspcva ${⊢}\left({A}{G}{y}\in {X}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{U}{G}{x}={x}\right)\to {U}{G}\left({A}{G}{y}\right)={A}{G}{y}$
27 19 22 26 syl2anc ${⊢}\left(\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {U}\in {X}\right)\wedge \left({\phi }\wedge {\psi }\right)\right)\wedge {A}\in {X}\right)\wedge {y}\in {X}\right)\to {U}{G}\left({A}{G}{y}\right)={A}{G}{y}$
28 27 adantr ${⊢}\left(\left(\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {U}\in {X}\right)\wedge \left({\phi }\wedge {\psi }\right)\right)\wedge {A}\in {X}\right)\wedge {y}\in {X}\right)\wedge {y}{G}{A}={U}\right)\to {U}{G}\left({A}{G}{y}\right)={A}{G}{y}$
29 pm3.22 ${⊢}\left(\left({y}\in {X}\wedge {A}\in {X}\right)\wedge {G}\in \mathrm{GrpOp}\right)\to \left({G}\in \mathrm{GrpOp}\wedge \left({y}\in {X}\wedge {A}\in {X}\right)\right)$
30 29 an31s ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\wedge {y}\in {X}\right)\to \left({G}\in \mathrm{GrpOp}\wedge \left({y}\in {X}\wedge {A}\in {X}\right)\right)$
31 30 adantllr ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {U}\in {X}\right)\wedge {A}\in {X}\right)\wedge {y}\in {X}\right)\to \left({G}\in \mathrm{GrpOp}\wedge \left({y}\in {X}\wedge {A}\in {X}\right)\right)$
32 31 adantllr ${⊢}\left(\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {U}\in {X}\right)\wedge \left({\phi }\wedge {\psi }\right)\right)\wedge {A}\in {X}\right)\wedge {y}\in {X}\right)\to \left({G}\in \mathrm{GrpOp}\wedge \left({y}\in {X}\wedge {A}\in {X}\right)\right)$
33 32 adantr ${⊢}\left(\left(\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {U}\in {X}\right)\wedge \left({\phi }\wedge {\psi }\right)\right)\wedge {A}\in {X}\right)\wedge {y}\in {X}\right)\wedge {y}{G}{A}={U}\right)\to \left({G}\in \mathrm{GrpOp}\wedge \left({y}\in {X}\wedge {A}\in {X}\right)\right)$
34 oveq2 ${⊢}{x}={y}\to {U}{G}{x}={U}{G}{y}$
35 id ${⊢}{x}={y}\to {x}={y}$
36 34 35 eqeq12d ${⊢}{x}={y}\to \left({U}{G}{x}={x}↔{U}{G}{y}={y}\right)$
37 36 rspccva ${⊢}\left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{U}{G}{x}={x}\wedge {y}\in {X}\right)\to {U}{G}{y}={y}$
38 2 37 sylanb ${⊢}\left({\phi }\wedge {y}\in {X}\right)\to {U}{G}{y}={y}$
39 38 adantlr ${⊢}\left(\left({\phi }\wedge {\psi }\right)\wedge {y}\in {X}\right)\to {U}{G}{y}={y}$
40 39 adantlr ${⊢}\left(\left(\left({\phi }\wedge {\psi }\right)\wedge {A}\in {X}\right)\wedge {y}\in {X}\right)\to {U}{G}{y}={y}$
41 40 adantlll ${⊢}\left(\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {U}\in {X}\right)\wedge \left({\phi }\wedge {\psi }\right)\right)\wedge {A}\in {X}\right)\wedge {y}\in {X}\right)\to {U}{G}{y}={y}$
42 41 anim1i ${⊢}\left(\left(\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {U}\in {X}\right)\wedge \left({\phi }\wedge {\psi }\right)\right)\wedge {A}\in {X}\right)\wedge {y}\in {X}\right)\wedge {y}{G}{A}={U}\right)\to \left({U}{G}{y}={y}\wedge {y}{G}{A}={U}\right)$
43 1 grpoidinvlem2 ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge \left({y}\in {X}\wedge {A}\in {X}\right)\right)\wedge \left({U}{G}{y}={y}\wedge {y}{G}{A}={U}\right)\right)\to \left({A}{G}{y}\right){G}\left({A}{G}{y}\right)={A}{G}{y}$
44 33 42 43 syl2anc ${⊢}\left(\left(\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {U}\in {X}\right)\wedge \left({\phi }\wedge {\psi }\right)\right)\wedge {A}\in {X}\right)\wedge {y}\in {X}\right)\wedge {y}{G}{A}={U}\right)\to \left({A}{G}{y}\right){G}\left({A}{G}{y}\right)={A}{G}{y}$
45 16 3expb ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({A}\in {X}\wedge {y}\in {X}\right)\right)\to {A}{G}{y}\in {X}$
46 45 ad2ant2rl ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {U}\in {X}\right)\wedge \left({\phi }\wedge \left({A}\in {X}\wedge {y}\in {X}\right)\right)\right)\to {A}{G}{y}\in {X}$
47 oveq1 ${⊢}{z}={w}\to {z}{G}{x}={w}{G}{x}$
48 47 eqeq1d ${⊢}{z}={w}\to \left({z}{G}{x}={U}↔{w}{G}{x}={U}\right)$
49 48 cbvrexvw ${⊢}\exists {z}\in {X}\phantom{\rule{.4em}{0ex}}{z}{G}{x}={U}↔\exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{x}={U}$
50 49 ralbii ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {z}\in {X}\phantom{\rule{.4em}{0ex}}{z}{G}{x}={U}↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{x}={U}$
51 3 50 bitri ${⊢}{\psi }↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{x}={U}$
52 oveq2 ${⊢}{x}={A}{G}{y}\to {w}{G}{x}={w}{G}\left({A}{G}{y}\right)$
53 52 eqeq1d ${⊢}{x}={A}{G}{y}\to \left({w}{G}{x}={U}↔{w}{G}\left({A}{G}{y}\right)={U}\right)$
54 53 rexbidv ${⊢}{x}={A}{G}{y}\to \left(\exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{x}={U}↔\exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}\left({A}{G}{y}\right)={U}\right)$
55 54 rspcva ${⊢}\left({A}{G}{y}\in {X}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}{x}={U}\right)\to \exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}\left({A}{G}{y}\right)={U}$
56 51 55 sylan2b ${⊢}\left({A}{G}{y}\in {X}\wedge {\psi }\right)\to \exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}\left({A}{G}{y}\right)={U}$
57 anass ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {w}\in {X}\right)\wedge {A}{G}{y}\in {X}\right)↔\left({G}\in \mathrm{GrpOp}\wedge \left({w}\in {X}\wedge {A}{G}{y}\in {X}\right)\right)$
58 57 biimpi ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {w}\in {X}\right)\wedge {A}{G}{y}\in {X}\right)\to \left({G}\in \mathrm{GrpOp}\wedge \left({w}\in {X}\wedge {A}{G}{y}\in {X}\right)\right)$
59 58 an32s ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {A}{G}{y}\in {X}\right)\wedge {w}\in {X}\right)\to \left({G}\in \mathrm{GrpOp}\wedge \left({w}\in {X}\wedge {A}{G}{y}\in {X}\right)\right)$
60 59 ex ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {A}{G}{y}\in {X}\right)\to \left({w}\in {X}\to \left({G}\in \mathrm{GrpOp}\wedge \left({w}\in {X}\wedge {A}{G}{y}\in {X}\right)\right)\right)$
61 45 60 syldan ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({A}\in {X}\wedge {y}\in {X}\right)\right)\to \left({w}\in {X}\to \left({G}\in \mathrm{GrpOp}\wedge \left({w}\in {X}\wedge {A}{G}{y}\in {X}\right)\right)\right)$
62 61 ad2ant2rl ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {U}\in {X}\right)\wedge \left({\phi }\wedge \left({A}\in {X}\wedge {y}\in {X}\right)\right)\right)\to \left({w}\in {X}\to \left({G}\in \mathrm{GrpOp}\wedge \left({w}\in {X}\wedge {A}{G}{y}\in {X}\right)\right)\right)$
63 62 imp ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {U}\in {X}\right)\wedge \left({\phi }\wedge \left({A}\in {X}\wedge {y}\in {X}\right)\right)\right)\wedge {w}\in {X}\right)\to \left({G}\in \mathrm{GrpOp}\wedge \left({w}\in {X}\wedge {A}{G}{y}\in {X}\right)\right)$
64 1 grpoidinvlem1 ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge \left({w}\in {X}\wedge {A}{G}{y}\in {X}\right)\right)\wedge \left({w}{G}\left({A}{G}{y}\right)={U}\wedge \left({A}{G}{y}\right){G}\left({A}{G}{y}\right)={A}{G}{y}\right)\right)\to {U}{G}\left({A}{G}{y}\right)={U}$
65 63 64 sylan ${⊢}\left(\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {U}\in {X}\right)\wedge \left({\phi }\wedge \left({A}\in {X}\wedge {y}\in {X}\right)\right)\right)\wedge {w}\in {X}\right)\wedge \left({w}{G}\left({A}{G}{y}\right)={U}\wedge \left({A}{G}{y}\right){G}\left({A}{G}{y}\right)={A}{G}{y}\right)\right)\to {U}{G}\left({A}{G}{y}\right)={U}$
66 65 exp43 ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {U}\in {X}\right)\wedge \left({\phi }\wedge \left({A}\in {X}\wedge {y}\in {X}\right)\right)\right)\to \left({w}\in {X}\to \left({w}{G}\left({A}{G}{y}\right)={U}\to \left(\left({A}{G}{y}\right){G}\left({A}{G}{y}\right)={A}{G}{y}\to {U}{G}\left({A}{G}{y}\right)={U}\right)\right)\right)$
67 66 rexlimdv ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {U}\in {X}\right)\wedge \left({\phi }\wedge \left({A}\in {X}\wedge {y}\in {X}\right)\right)\right)\to \left(\exists {w}\in {X}\phantom{\rule{.4em}{0ex}}{w}{G}\left({A}{G}{y}\right)={U}\to \left(\left({A}{G}{y}\right){G}\left({A}{G}{y}\right)={A}{G}{y}\to {U}{G}\left({A}{G}{y}\right)={U}\right)\right)$
68 56 67 syl5 ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {U}\in {X}\right)\wedge \left({\phi }\wedge \left({A}\in {X}\wedge {y}\in {X}\right)\right)\right)\to \left(\left({A}{G}{y}\in {X}\wedge {\psi }\right)\to \left(\left({A}{G}{y}\right){G}\left({A}{G}{y}\right)={A}{G}{y}\to {U}{G}\left({A}{G}{y}\right)={U}\right)\right)$
69 46 68 mpand ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {U}\in {X}\right)\wedge \left({\phi }\wedge \left({A}\in {X}\wedge {y}\in {X}\right)\right)\right)\to \left({\psi }\to \left(\left({A}{G}{y}\right){G}\left({A}{G}{y}\right)={A}{G}{y}\to {U}{G}\left({A}{G}{y}\right)={U}\right)\right)$
70 69 exp32 ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {U}\in {X}\right)\to \left({\phi }\to \left(\left({A}\in {X}\wedge {y}\in {X}\right)\to \left({\psi }\to \left(\left({A}{G}{y}\right){G}\left({A}{G}{y}\right)={A}{G}{y}\to {U}{G}\left({A}{G}{y}\right)={U}\right)\right)\right)\right)$
71 70 com34 ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {U}\in {X}\right)\to \left({\phi }\to \left({\psi }\to \left(\left({A}\in {X}\wedge {y}\in {X}\right)\to \left(\left({A}{G}{y}\right){G}\left({A}{G}{y}\right)={A}{G}{y}\to {U}{G}\left({A}{G}{y}\right)={U}\right)\right)\right)\right)$
72 71 imp32 ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {U}\in {X}\right)\wedge \left({\phi }\wedge {\psi }\right)\right)\to \left(\left({A}\in {X}\wedge {y}\in {X}\right)\to \left(\left({A}{G}{y}\right){G}\left({A}{G}{y}\right)={A}{G}{y}\to {U}{G}\left({A}{G}{y}\right)={U}\right)\right)$
73 72 impl ${⊢}\left(\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {U}\in {X}\right)\wedge \left({\phi }\wedge {\psi }\right)\right)\wedge {A}\in {X}\right)\wedge {y}\in {X}\right)\to \left(\left({A}{G}{y}\right){G}\left({A}{G}{y}\right)={A}{G}{y}\to {U}{G}\left({A}{G}{y}\right)={U}\right)$
74 73 adantr ${⊢}\left(\left(\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {U}\in {X}\right)\wedge \left({\phi }\wedge {\psi }\right)\right)\wedge {A}\in {X}\right)\wedge {y}\in {X}\right)\wedge {y}{G}{A}={U}\right)\to \left(\left({A}{G}{y}\right){G}\left({A}{G}{y}\right)={A}{G}{y}\to {U}{G}\left({A}{G}{y}\right)={U}\right)$
75 44 74 mpd ${⊢}\left(\left(\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {U}\in {X}\right)\wedge \left({\phi }\wedge {\psi }\right)\right)\wedge {A}\in {X}\right)\wedge {y}\in {X}\right)\wedge {y}{G}{A}={U}\right)\to {U}{G}\left({A}{G}{y}\right)={U}$
76 28 75 eqtr3d ${⊢}\left(\left(\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {U}\in {X}\right)\wedge \left({\phi }\wedge {\psi }\right)\right)\wedge {A}\in {X}\right)\wedge {y}\in {X}\right)\wedge {y}{G}{A}={U}\right)\to {A}{G}{y}={U}$
77 76 ex ${⊢}\left(\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {U}\in {X}\right)\wedge \left({\phi }\wedge {\psi }\right)\right)\wedge {A}\in {X}\right)\wedge {y}\in {X}\right)\to \left({y}{G}{A}={U}\to {A}{G}{y}={U}\right)$
78 77 ancld ${⊢}\left(\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {U}\in {X}\right)\wedge \left({\phi }\wedge {\psi }\right)\right)\wedge {A}\in {X}\right)\wedge {y}\in {X}\right)\to \left({y}{G}{A}={U}\to \left({y}{G}{A}={U}\wedge {A}{G}{y}={U}\right)\right)$
79 78 reximdva ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {U}\in {X}\right)\wedge \left({\phi }\wedge {\psi }\right)\right)\wedge {A}\in {X}\right)\to \left(\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{A}={U}\to \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{A}={U}\wedge {A}{G}{y}={U}\right)\right)$
80 15 79 mpd ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {U}\in {X}\right)\wedge \left({\phi }\wedge {\psi }\right)\right)\wedge {A}\in {X}\right)\to \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{A}={U}\wedge {A}{G}{y}={U}\right)$