Metamath Proof Explorer

Theorem exidcl

Description: Obsolete theorem, use mgmcl instead. Closure of the binary operation of a magma with identity. (Contributed by Jeff Madsen, 16-Jun-2011) (New usage is discouraged.) (Proof modification is discouraged.)

		Ref	Expression
	Hypothesis	exidcl.1	$⊢ X = ran G$
	Assertion	exidcl	$⊢ (G \in (Magma \cap ExId) \land A \in X \land B \in X) \to A G B \in X$

Proof

Step	Hyp	Ref	Expression
1		exidcl.1	$⊢ X = ran G$
2		rngopidOLD	$⊢ G \in (Magma \cap ExId) \to ran G = dom dom G$
3	1 2	eqtrid	$⊢ G \in (Magma \cap ExId) \to X = dom dom G$
4	3	eleq2d	$⊢ G \in (Magma \cap ExId) \to (A \in X \leftrightarrow A \in dom dom G)$
5	3	eleq2d	$⊢ G \in (Magma \cap ExId) \to (B \in X \leftrightarrow B \in dom dom G)$
6	4 5	anbi12d	$⊢ G \in (Magma \cap ExId) \to ((A \in X \land B \in X) \leftrightarrow (A \in dom dom G \land B \in dom dom G))$
7	6	pm5.32i	$⊢ (G \in (Magma \cap ExId) \land (A \in X \land B \in X)) \leftrightarrow (G \in (Magma \cap ExId) \land (A \in dom dom G \land B \in dom dom G))$
8		inss1	$⊢ Magma \cap ExId \subseteq Magma$
9	8	sseli	$⊢ G \in (Magma \cap ExId) \to G \in Magma$
10		eqid	$⊢ dom dom G = dom dom G$
11	10	clmgmOLD	$⊢ (G \in Magma \land A \in dom dom G \land B \in dom dom G) \to A G B \in dom dom G$
12	9 11	syl3an1	$⊢ (G \in (Magma \cap ExId) \land A \in dom dom G \land B \in dom dom G) \to A G B \in dom dom G$
13	12	3expb	$⊢ (G \in (Magma \cap ExId) \land (A \in dom dom G \land B \in dom dom G)) \to A G B \in dom dom G$
14	7 13	sylbi	$⊢ (G \in (Magma \cap ExId) \land (A \in X \land B \in X)) \to A G B \in dom dom G$
15	14	3impb	$⊢ (G \in (Magma \cap ExId) \land A \in X \land B \in X) \to A G B \in dom dom G$
16	3	3ad2ant1	$⊢ (G \in (Magma \cap ExId) \land A \in X \land B \in X) \to X = dom dom G$
17	15 16	eleqtrrd	$⊢ (G \in (Magma \cap ExId) \land A \in X \land B \in X) \to A G B \in X$