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 )