# Metamath Proof Explorer

## Theorem exidreslem

Description: Lemma for exidres and exidresid . (Contributed by Jeff Madsen, 8-Jun-2010) (Revised by Mario Carneiro, 23-Dec-2013)

Ref Expression
Hypotheses exidres.1 ${⊢}{X}=\mathrm{ran}{G}$
exidres.2 ${⊢}{U}=\mathrm{GId}\left({G}\right)$
exidres.3 ${⊢}{H}={{G}↾}_{\left({Y}×{Y}\right)}$
Assertion exidreslem ${⊢}\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge {Y}\subseteq {X}\wedge {U}\in {Y}\right)\to \left({U}\in \mathrm{dom}\mathrm{dom}{H}\wedge \forall {x}\in \mathrm{dom}\mathrm{dom}{H}\phantom{\rule{.4em}{0ex}}\left({U}{H}{x}={x}\wedge {x}{H}{U}={x}\right)\right)$

### Proof

Step Hyp Ref Expression
1 exidres.1 ${⊢}{X}=\mathrm{ran}{G}$
2 exidres.2 ${⊢}{U}=\mathrm{GId}\left({G}\right)$
3 exidres.3 ${⊢}{H}={{G}↾}_{\left({Y}×{Y}\right)}$
4 3 dmeqi ${⊢}\mathrm{dom}{H}=\mathrm{dom}\left({{G}↾}_{\left({Y}×{Y}\right)}\right)$
5 xpss12 ${⊢}\left({Y}\subseteq {X}\wedge {Y}\subseteq {X}\right)\to {Y}×{Y}\subseteq {X}×{X}$
6 5 anidms ${⊢}{Y}\subseteq {X}\to {Y}×{Y}\subseteq {X}×{X}$
7 1 opidon2OLD ${⊢}{G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\to {G}:{X}×{X}\underset{onto}{⟶}{X}$
8 fof ${⊢}{G}:{X}×{X}\underset{onto}{⟶}{X}\to {G}:{X}×{X}⟶{X}$
9 fdm ${⊢}{G}:{X}×{X}⟶{X}\to \mathrm{dom}{G}={X}×{X}$
10 7 8 9 3syl ${⊢}{G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\to \mathrm{dom}{G}={X}×{X}$
11 10 sseq2d ${⊢}{G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\to \left({Y}×{Y}\subseteq \mathrm{dom}{G}↔{Y}×{Y}\subseteq {X}×{X}\right)$
12 6 11 syl5ibr ${⊢}{G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\to \left({Y}\subseteq {X}\to {Y}×{Y}\subseteq \mathrm{dom}{G}\right)$
13 12 imp ${⊢}\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge {Y}\subseteq {X}\right)\to {Y}×{Y}\subseteq \mathrm{dom}{G}$
14 ssdmres ${⊢}{Y}×{Y}\subseteq \mathrm{dom}{G}↔\mathrm{dom}\left({{G}↾}_{\left({Y}×{Y}\right)}\right)={Y}×{Y}$
15 13 14 sylib ${⊢}\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge {Y}\subseteq {X}\right)\to \mathrm{dom}\left({{G}↾}_{\left({Y}×{Y}\right)}\right)={Y}×{Y}$
16 4 15 syl5eq ${⊢}\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge {Y}\subseteq {X}\right)\to \mathrm{dom}{H}={Y}×{Y}$
17 16 dmeqd ${⊢}\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge {Y}\subseteq {X}\right)\to \mathrm{dom}\mathrm{dom}{H}=\mathrm{dom}\left({Y}×{Y}\right)$
18 dmxpid ${⊢}\mathrm{dom}\left({Y}×{Y}\right)={Y}$
19 17 18 syl6eq ${⊢}\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge {Y}\subseteq {X}\right)\to \mathrm{dom}\mathrm{dom}{H}={Y}$
20 19 eleq2d ${⊢}\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge {Y}\subseteq {X}\right)\to \left({U}\in \mathrm{dom}\mathrm{dom}{H}↔{U}\in {Y}\right)$
21 20 biimp3ar ${⊢}\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge {Y}\subseteq {X}\wedge {U}\in {Y}\right)\to {U}\in \mathrm{dom}\mathrm{dom}{H}$
22 ssel2 ${⊢}\left({Y}\subseteq {X}\wedge {x}\in {Y}\right)\to {x}\in {X}$
23 1 2 cmpidelt ${⊢}\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge {x}\in {X}\right)\to \left({U}{G}{x}={x}\wedge {x}{G}{U}={x}\right)$
24 22 23 sylan2 ${⊢}\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge \left({Y}\subseteq {X}\wedge {x}\in {Y}\right)\right)\to \left({U}{G}{x}={x}\wedge {x}{G}{U}={x}\right)$
25 24 anassrs ${⊢}\left(\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge {Y}\subseteq {X}\right)\wedge {x}\in {Y}\right)\to \left({U}{G}{x}={x}\wedge {x}{G}{U}={x}\right)$
26 25 adantrl ${⊢}\left(\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({U}\in {Y}\wedge {x}\in {Y}\right)\right)\to \left({U}{G}{x}={x}\wedge {x}{G}{U}={x}\right)$
27 3 oveqi ${⊢}{U}{H}{x}={U}\left({{G}↾}_{\left({Y}×{Y}\right)}\right){x}$
28 ovres ${⊢}\left({U}\in {Y}\wedge {x}\in {Y}\right)\to {U}\left({{G}↾}_{\left({Y}×{Y}\right)}\right){x}={U}{G}{x}$
29 27 28 syl5eq ${⊢}\left({U}\in {Y}\wedge {x}\in {Y}\right)\to {U}{H}{x}={U}{G}{x}$
30 29 eqeq1d ${⊢}\left({U}\in {Y}\wedge {x}\in {Y}\right)\to \left({U}{H}{x}={x}↔{U}{G}{x}={x}\right)$
31 3 oveqi ${⊢}{x}{H}{U}={x}\left({{G}↾}_{\left({Y}×{Y}\right)}\right){U}$
32 ovres ${⊢}\left({x}\in {Y}\wedge {U}\in {Y}\right)\to {x}\left({{G}↾}_{\left({Y}×{Y}\right)}\right){U}={x}{G}{U}$
33 31 32 syl5eq ${⊢}\left({x}\in {Y}\wedge {U}\in {Y}\right)\to {x}{H}{U}={x}{G}{U}$
34 33 ancoms ${⊢}\left({U}\in {Y}\wedge {x}\in {Y}\right)\to {x}{H}{U}={x}{G}{U}$
35 34 eqeq1d ${⊢}\left({U}\in {Y}\wedge {x}\in {Y}\right)\to \left({x}{H}{U}={x}↔{x}{G}{U}={x}\right)$
36 30 35 anbi12d ${⊢}\left({U}\in {Y}\wedge {x}\in {Y}\right)\to \left(\left({U}{H}{x}={x}\wedge {x}{H}{U}={x}\right)↔\left({U}{G}{x}={x}\wedge {x}{G}{U}={x}\right)\right)$
37 36 adantl ${⊢}\left(\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({U}\in {Y}\wedge {x}\in {Y}\right)\right)\to \left(\left({U}{H}{x}={x}\wedge {x}{H}{U}={x}\right)↔\left({U}{G}{x}={x}\wedge {x}{G}{U}={x}\right)\right)$
38 26 37 mpbird ${⊢}\left(\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({U}\in {Y}\wedge {x}\in {Y}\right)\right)\to \left({U}{H}{x}={x}\wedge {x}{H}{U}={x}\right)$
39 38 anassrs ${⊢}\left(\left(\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge {Y}\subseteq {X}\right)\wedge {U}\in {Y}\right)\wedge {x}\in {Y}\right)\to \left({U}{H}{x}={x}\wedge {x}{H}{U}={x}\right)$
40 39 ralrimiva ${⊢}\left(\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge {Y}\subseteq {X}\right)\wedge {U}\in {Y}\right)\to \forall {x}\in {Y}\phantom{\rule{.4em}{0ex}}\left({U}{H}{x}={x}\wedge {x}{H}{U}={x}\right)$
41 40 3impa ${⊢}\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge {Y}\subseteq {X}\wedge {U}\in {Y}\right)\to \forall {x}\in {Y}\phantom{\rule{.4em}{0ex}}\left({U}{H}{x}={x}\wedge {x}{H}{U}={x}\right)$
42 13 3adant3 ${⊢}\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge {Y}\subseteq {X}\wedge {U}\in {Y}\right)\to {Y}×{Y}\subseteq \mathrm{dom}{G}$
43 42 14 sylib ${⊢}\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge {Y}\subseteq {X}\wedge {U}\in {Y}\right)\to \mathrm{dom}\left({{G}↾}_{\left({Y}×{Y}\right)}\right)={Y}×{Y}$
44 4 43 syl5eq ${⊢}\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge {Y}\subseteq {X}\wedge {U}\in {Y}\right)\to \mathrm{dom}{H}={Y}×{Y}$
45 44 dmeqd ${⊢}\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge {Y}\subseteq {X}\wedge {U}\in {Y}\right)\to \mathrm{dom}\mathrm{dom}{H}=\mathrm{dom}\left({Y}×{Y}\right)$
46 45 18 syl6eq ${⊢}\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge {Y}\subseteq {X}\wedge {U}\in {Y}\right)\to \mathrm{dom}\mathrm{dom}{H}={Y}$
47 46 raleqdv ${⊢}\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge {Y}\subseteq {X}\wedge {U}\in {Y}\right)\to \left(\forall {x}\in \mathrm{dom}\mathrm{dom}{H}\phantom{\rule{.4em}{0ex}}\left({U}{H}{x}={x}\wedge {x}{H}{U}={x}\right)↔\forall {x}\in {Y}\phantom{\rule{.4em}{0ex}}\left({U}{H}{x}={x}\wedge {x}{H}{U}={x}\right)\right)$
48 41 47 mpbird ${⊢}\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge {Y}\subseteq {X}\wedge {U}\in {Y}\right)\to \forall {x}\in \mathrm{dom}\mathrm{dom}{H}\phantom{\rule{.4em}{0ex}}\left({U}{H}{x}={x}\wedge {x}{H}{U}={x}\right)$
49 21 48 jca ${⊢}\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge {Y}\subseteq {X}\wedge {U}\in {Y}\right)\to \left({U}\in \mathrm{dom}\mathrm{dom}{H}\wedge \forall {x}\in \mathrm{dom}\mathrm{dom}{H}\phantom{\rule{.4em}{0ex}}\left({U}{H}{x}={x}\wedge {x}{H}{U}={x}\right)\right)$