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 
|- 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 )