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 \times Y)}$
	Assertion	exidres	$⊢ (G \in (Magma \cap ExId) \land Y \subseteq X \land U \in Y) \to H \in ExId$

Proof

Step	Hyp	Ref	Expression
1		exidres.1	$⊢ X = ran G$
2		exidres.2	$⊢ U = GId (G)$
3		exidres.3	$⊢ H = {G ↾}_{(Y \times Y)}$
4	1 2 3	exidreslem	$⊢ (G \in (Magma \cap ExId) \land Y \subseteq X \land U \in Y) \to (U \in dom dom H \land \forall x \in dom dom H (U H x = x \land x H U = x))$
5		oveq1	$⊢ u = U \to u H x = U H x$
6	5	eqeq1d	$⊢ u = U \to (u H x = x \leftrightarrow U H x = x)$
7	6	ovanraleqv	$⊢ u = U \to (\forall x \in dom dom H (u H x = x \land x H u = x) \leftrightarrow \forall x \in dom dom H (U H x = x \land x H U = x))$
8	7	rspcev	$⊢ (U \in dom dom H \land \forall x \in dom dom H (U H x = x \land x H U = x)) \to \exists u \in dom dom H \forall x \in dom dom H (u H x = x \land x H u = x)$
9	4 8	syl	$⊢ (G \in (Magma \cap ExId) \land Y \subseteq X \land U \in Y) \to \exists u \in dom dom H \forall x \in dom dom H (u H x = x \land x H u = x)$
10		resexg	$⊢ G \in (Magma \cap ExId) \to {G ↾}_{(Y \times Y)} \in V$
11	3 10	eqeltrid	$⊢ G \in (Magma \cap ExId) \to H \in V$
12		eqid	$⊢ dom dom H = dom dom H$
13	12	isexid	$⊢ H \in V \to (H \in ExId \leftrightarrow \exists u \in dom dom H \forall x \in dom dom H (u H x = x \land x H u = x))$
14	11 13	syl	$⊢ G \in (Magma \cap ExId) \to (H \in ExId \leftrightarrow \exists u \in dom dom H \forall x \in dom dom H (u H x = x \land x H u = x))$
15	14	3ad2ant1	$⊢ (G \in (Magma \cap ExId) \land Y \subseteq X \land U \in Y) \to (H \in ExId \leftrightarrow \exists u \in dom dom H \forall x \in dom dom H (u H x = x \land x H u = x))$
16	9 15	mpbird	$⊢ (G \in (Magma \cap ExId) \land Y \subseteq X \land U \in Y) \to H \in ExId$