This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem exidres

Description: The restriction of a binary operation with identity to a subset containing the identity has an identity element. (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 exidres ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌 ) → 𝐻 ∈ ExId )

Proof

Step Hyp Ref Expression
1 exidres.1 ⊢ 𝑋 = ran 𝐺
2 exidres.2 ⊢ 𝑈 = ( GId ‘ 𝐺 )
3 exidres.3 ⊢ 𝐻 = ( 𝐺 ↾ ( 𝑌 × 𝑌 ) )
4 1 2 3 exidreslem ⊢ ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌 ) → ( 𝑈 ∈ dom dom 𝐻 ∧ ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) ) )
5 oveq1 ⊢ ( 𝑢 = 𝑈 → ( 𝑢 𝐻 𝑥 ) = ( 𝑈 𝐻 𝑥 ) )
6 5 eqeq1d ⊢ ( 𝑢 = 𝑈 → ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ↔ ( 𝑈 𝐻 𝑥 ) = 𝑥 ) )
7 6 ovanraleqv ⊢ ( 𝑢 = 𝑈 → ( ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) ) )
8 7 rspcev ⊢ ( ( 𝑈 ∈ dom dom 𝐻 ∧ ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) ) → ∃ 𝑢 ∈ dom dom 𝐻 ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) )
9 4 8 syl ⊢ ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌 ) → ∃ 𝑢 ∈ dom dom 𝐻 ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) )
10 resexg ⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) ∈ V )
11 3 10 eqeltrid ⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → 𝐻 ∈ V )
12 eqid ⊢ dom dom 𝐻 = dom dom 𝐻
13 12 isexid ⊢ ( 𝐻 ∈ V → ( 𝐻 ∈ ExId ↔ ∃ 𝑢 ∈ dom dom 𝐻 ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ) )
14 11 13 syl ⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → ( 𝐻 ∈ ExId ↔ ∃ 𝑢 ∈ dom dom 𝐻 ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ) )
15 14 3ad2ant1 ⊢ ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌 ) → ( 𝐻 ∈ ExId ↔ ∃ 𝑢 ∈ dom dom 𝐻 ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ) )
16 9 15 mpbird ⊢ ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌 ) → 𝐻 ∈ ExId )