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 )