# 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 𝑋 = ran 𝐺
exidres.2 𝑈 = ( GId ‘ 𝐺 )
exidres.3 𝐻 = ( 𝐺 ↾ ( 𝑌 × 𝑌 ) )
Assertion exidreslem ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋𝑈𝑌 ) → ( 𝑈 ∈ dom dom 𝐻 ∧ ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) ) )

### Proof

Step Hyp Ref Expression
1 exidres.1 𝑋 = ran 𝐺
2 exidres.2 𝑈 = ( GId ‘ 𝐺 )
3 exidres.3 𝐻 = ( 𝐺 ↾ ( 𝑌 × 𝑌 ) )
4 3 dmeqi dom 𝐻 = dom ( 𝐺 ↾ ( 𝑌 × 𝑌 ) )
5 xpss12 ( ( 𝑌𝑋𝑌𝑋 ) → ( 𝑌 × 𝑌 ) ⊆ ( 𝑋 × 𝑋 ) )
6 5 anidms ( 𝑌𝑋 → ( 𝑌 × 𝑌 ) ⊆ ( 𝑋 × 𝑋 ) )
7 1 opidon2OLD ( 𝐺 ∈ ( Magma ∩ ExId ) → 𝐺 : ( 𝑋 × 𝑋 ) –onto𝑋 )
8 fof ( 𝐺 : ( 𝑋 × 𝑋 ) –onto𝑋𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
9 fdm ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 → dom 𝐺 = ( 𝑋 × 𝑋 ) )
10 7 8 9 3syl ( 𝐺 ∈ ( Magma ∩ ExId ) → dom 𝐺 = ( 𝑋 × 𝑋 ) )
11 10 sseq2d ( 𝐺 ∈ ( Magma ∩ ExId ) → ( ( 𝑌 × 𝑌 ) ⊆ dom 𝐺 ↔ ( 𝑌 × 𝑌 ) ⊆ ( 𝑋 × 𝑋 ) ) )
12 6 11 syl5ibr ( 𝐺 ∈ ( Magma ∩ ExId ) → ( 𝑌𝑋 → ( 𝑌 × 𝑌 ) ⊆ dom 𝐺 ) )
13 12 imp ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋 ) → ( 𝑌 × 𝑌 ) ⊆ dom 𝐺 )
14 ssdmres ( ( 𝑌 × 𝑌 ) ⊆ dom 𝐺 ↔ dom ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) = ( 𝑌 × 𝑌 ) )
15 13 14 sylib ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋 ) → dom ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) = ( 𝑌 × 𝑌 ) )
16 4 15 syl5eq ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋 ) → dom 𝐻 = ( 𝑌 × 𝑌 ) )
17 16 dmeqd ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋 ) → dom dom 𝐻 = dom ( 𝑌 × 𝑌 ) )
18 dmxpid dom ( 𝑌 × 𝑌 ) = 𝑌
19 17 18 eqtrdi ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋 ) → dom dom 𝐻 = 𝑌 )
20 19 eleq2d ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋 ) → ( 𝑈 ∈ dom dom 𝐻𝑈𝑌 ) )
21 20 biimp3ar ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋𝑈𝑌 ) → 𝑈 ∈ dom dom 𝐻 )
22 ssel2 ( ( 𝑌𝑋𝑥𝑌 ) → 𝑥𝑋 )
23 1 2 cmpidelt ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑥𝑋 ) → ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑈 ) = 𝑥 ) )
24 22 23 sylan2 ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ ( 𝑌𝑋𝑥𝑌 ) ) → ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑈 ) = 𝑥 ) )
25 24 anassrs ( ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋 ) ∧ 𝑥𝑌 ) → ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑈 ) = 𝑥 ) )
26 25 adantrl ( ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋 ) ∧ ( 𝑈𝑌𝑥𝑌 ) ) → ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑈 ) = 𝑥 ) )
27 3 oveqi ( 𝑈 𝐻 𝑥 ) = ( 𝑈 ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) 𝑥 )
28 ovres ( ( 𝑈𝑌𝑥𝑌 ) → ( 𝑈 ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) 𝑥 ) = ( 𝑈 𝐺 𝑥 ) )
29 27 28 syl5eq ( ( 𝑈𝑌𝑥𝑌 ) → ( 𝑈 𝐻 𝑥 ) = ( 𝑈 𝐺 𝑥 ) )
30 29 eqeq1d ( ( 𝑈𝑌𝑥𝑌 ) → ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ↔ ( 𝑈 𝐺 𝑥 ) = 𝑥 ) )
31 3 oveqi ( 𝑥 𝐻 𝑈 ) = ( 𝑥 ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) 𝑈 )
32 ovres ( ( 𝑥𝑌𝑈𝑌 ) → ( 𝑥 ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) 𝑈 ) = ( 𝑥 𝐺 𝑈 ) )
33 31 32 syl5eq ( ( 𝑥𝑌𝑈𝑌 ) → ( 𝑥 𝐻 𝑈 ) = ( 𝑥 𝐺 𝑈 ) )
34 33 ancoms ( ( 𝑈𝑌𝑥𝑌 ) → ( 𝑥 𝐻 𝑈 ) = ( 𝑥 𝐺 𝑈 ) )
35 34 eqeq1d ( ( 𝑈𝑌𝑥𝑌 ) → ( ( 𝑥 𝐻 𝑈 ) = 𝑥 ↔ ( 𝑥 𝐺 𝑈 ) = 𝑥 ) )
36 30 35 anbi12d ( ( 𝑈𝑌𝑥𝑌 ) → ( ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) ↔ ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑈 ) = 𝑥 ) ) )
37 36 adantl ( ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋 ) ∧ ( 𝑈𝑌𝑥𝑌 ) ) → ( ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) ↔ ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑈 ) = 𝑥 ) ) )
38 26 37 mpbird ( ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋 ) ∧ ( 𝑈𝑌𝑥𝑌 ) ) → ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) )
39 38 anassrs ( ( ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋 ) ∧ 𝑈𝑌 ) ∧ 𝑥𝑌 ) → ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) )
40 39 ralrimiva ( ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋 ) ∧ 𝑈𝑌 ) → ∀ 𝑥𝑌 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) )
41 40 3impa ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋𝑈𝑌 ) → ∀ 𝑥𝑌 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) )
42 13 3adant3 ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋𝑈𝑌 ) → ( 𝑌 × 𝑌 ) ⊆ dom 𝐺 )
43 42 14 sylib ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋𝑈𝑌 ) → dom ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) = ( 𝑌 × 𝑌 ) )
44 4 43 syl5eq ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋𝑈𝑌 ) → dom 𝐻 = ( 𝑌 × 𝑌 ) )
45 44 dmeqd ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋𝑈𝑌 ) → dom dom 𝐻 = dom ( 𝑌 × 𝑌 ) )
46 45 18 eqtrdi ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋𝑈𝑌 ) → dom dom 𝐻 = 𝑌 )
47 46 raleqdv ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋𝑈𝑌 ) → ( ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) ↔ ∀ 𝑥𝑌 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) ) )
48 41 47 mpbird ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋𝑈𝑌 ) → ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) )
49 21 48 jca ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌𝑋𝑈𝑌 ) → ( 𝑈 ∈ dom dom 𝐻 ∧ ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) ) )