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 𝐻 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) ) )