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
|- X = ran G
exidres.2
|- U = ( GId ` G )
exidres.3
|- H = ( G |` ( Y X. Y ) )
Assertion exidres
|- ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) -> H e. ExId )

Proof

Step Hyp Ref Expression
1 exidres.1
 |-  X = ran G
2 exidres.2
 |-  U = ( GId ` G )
3 exidres.3
 |-  H = ( G |` ( Y X. Y ) )
4 1 2 3 exidreslem
 |-  ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) -> ( U e. dom dom H /\ A. x e. dom dom H ( ( U H x ) = x /\ ( x H U ) = x ) ) )
5 oveq1
 |-  ( u = U -> ( u H x ) = ( U H x ) )
6 5 eqeq1d
 |-  ( u = U -> ( ( u H x ) = x <-> ( U H x ) = x ) )
7 6 ovanraleqv
 |-  ( u = U -> ( A. x e. dom dom H ( ( u H x ) = x /\ ( x H u ) = x ) <-> A. x e. dom dom H ( ( U H x ) = x /\ ( x H U ) = x ) ) )
8 7 rspcev
 |-  ( ( U e. dom dom H /\ A. x e. dom dom H ( ( U H x ) = x /\ ( x H U ) = x ) ) -> E. u e. dom dom H A. x e. dom dom H ( ( u H x ) = x /\ ( x H u ) = x ) )
9 4 8 syl
 |-  ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) -> E. u e. dom dom H A. x e. dom dom H ( ( u H x ) = x /\ ( x H u ) = x ) )
10 resexg
 |-  ( G e. ( Magma i^i ExId ) -> ( G |` ( Y X. Y ) ) e. _V )
11 3 10 eqeltrid
 |-  ( G e. ( Magma i^i ExId ) -> H e. _V )
12 eqid
 |-  dom dom H = dom dom H
13 12 isexid
 |-  ( H e. _V -> ( H e. ExId <-> E. u e. dom dom H A. x e. dom dom H ( ( u H x ) = x /\ ( x H u ) = x ) ) )
14 11 13 syl
 |-  ( G e. ( Magma i^i ExId ) -> ( H e. ExId <-> E. u e. dom dom H A. x e. dom dom H ( ( u H x ) = x /\ ( x H u ) = x ) ) )
15 14 3ad2ant1
 |-  ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) -> ( H e. ExId <-> E. u e. dom dom H A. x e. dom dom H ( ( u H x ) = x /\ ( x H u ) = x ) ) )
16 9 15 mpbird
 |-  ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) -> H e. ExId )