Metamath Proof Explorer

Theorem clmgmOLD

Description: Obsolete version of mgmcl as of 3-Feb-2020. Closure of a magma. (Contributed by FL, 14-Sep-2010) (New usage is discouraged.) (Proof modification is discouraged.)

		Ref	Expression
	Hypothesis	clmgmOLD.1	$⊢ X = dom dom G$
	Assertion	clmgmOLD	$⊢ (G \in Magma \land A \in X \land B \in X) \to A G B \in X$

Proof

Step	Hyp	Ref	Expression
1		clmgmOLD.1	$⊢ X = dom dom G$
2	1	ismgmOLD	$⊢ G \in Magma \to (G \in Magma \leftrightarrow G : X \times X ⟶ X)$
3		fovrn	$⊢ (G : X \times X ⟶ X \land A \in X \land B \in X) \to A G B \in X$
4	3	3exp	$⊢ G : X \times X ⟶ X \to (A \in X \to (B \in X \to A G B \in X))$
5	2 4	syl6bi	$⊢ G \in Magma \to (G \in Magma \to (A \in X \to (B \in X \to A G B \in X)))$
6	5	pm2.43i	$⊢ G \in Magma \to (A \in X \to (B \in X \to A G B \in X))$
7	6	3imp	$⊢ (G \in Magma \land A \in X \land B \in X) \to A G B \in X$