ismndo2

Description: The predicate "is a monoid". (Contributed by FL, 2-Nov-2009) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	ismndo2.1	$⊢ X = ran G$
	Assertion	ismndo2	$⊢ G \in A \to (G \in MndOp \leftrightarrow (G : X \times X ⟶ X \land \forall x \in X \forall y \in X \forall z \in X (x G y) G z = x G (y G z) \land \exists x \in X \forall y \in X (x G y = y \land y G x = y)))$

Proof

Step	Hyp	Ref	Expression
1		ismndo2.1	$⊢ X = ran G$
2		mndomgmid	$⊢ G \in MndOp \to G \in (Magma \cap ExId)$
3		rngopidOLD	$⊢ G \in (Magma \cap ExId) \to ran G = dom dom G$
4	2 3	syl	$⊢ G \in MndOp \to ran G = dom dom G$
5	1 4	syl5eq	$⊢ G \in MndOp \to X = dom dom G$
6	5	a1i	$⊢ G \in A \to (G \in MndOp \to X = dom dom G)$
7		fdm	$⊢ G : X \times X ⟶ X \to dom G = X \times X$
8	7	dmeqd	$⊢ G : X \times X ⟶ X \to dom dom G = dom (X \times X)$
9		dmxpid	$⊢ dom (X \times X) = X$
10	8 9	eqtr2di	$⊢ G : X \times X ⟶ X \to X = dom dom G$
11	10	3ad2ant1	$⊢ (G : X \times X ⟶ X \land \forall x \in X \forall y \in X \forall z \in X (x G y) G z = x G (y G z) \land \exists x \in X \forall y \in X (x G y = y \land y G x = y)) \to X = dom dom G$
12	11	a1i	$⊢ G \in A \to ((G : X \times X ⟶ X \land \forall x \in X \forall y \in X \forall z \in X (x G y) G z = x G (y G z) \land \exists x \in X \forall y \in X (x G y = y \land y G x = y)) \to X = dom dom G)$
13		eqid	$⊢ dom dom G = dom dom G$
14	13	ismndo1	$⊢ G \in A \to (G \in MndOp \leftrightarrow (G : dom dom G \times dom dom G ⟶ dom dom G \land \forall x \in dom dom G \forall y \in dom dom G \forall z \in dom dom G (x G y) G z = x G (y G z) \land \exists x \in dom dom G \forall y \in dom dom G (x G y = y \land y G x = y)))$
15		xpid11	$⊢ X \times X = dom dom G \times dom dom G \leftrightarrow X = dom dom G$
16	15	biimpri	$⊢ X = dom dom G \to X \times X = dom dom G \times dom dom G$
17		feq23	$⊢ (X \times X = dom dom G \times dom dom G \land X = dom dom G) \to (G : X \times X ⟶ X \leftrightarrow G : dom dom G \times dom dom G ⟶ dom dom G)$
18	16 17	mpancom	$⊢ X = dom dom G \to (G : X \times X ⟶ X \leftrightarrow G : dom dom G \times dom dom G ⟶ dom dom G)$
19		raleq	$⊢ X = dom dom G \to (\forall z \in X (x G y) G z = x G (y G z) \leftrightarrow \forall z \in dom dom G (x G y) G z = x G (y G z))$
20	19	raleqbi1dv	$⊢ X = dom dom G \to (\forall y \in X \forall z \in X (x G y) G z = x G (y G z) \leftrightarrow \forall y \in dom dom G \forall z \in dom dom G (x G y) G z = x G (y G z))$
21	20	raleqbi1dv	$⊢ X = dom dom G \to (\forall x \in X \forall y \in X \forall z \in X (x G y) G z = x G (y G z) \leftrightarrow \forall x \in dom dom G \forall y \in dom dom G \forall z \in dom dom G (x G y) G z = x G (y G z))$
22		raleq	$⊢ X = dom dom G \to (\forall y \in X (x G y = y \land y G x = y) \leftrightarrow \forall y \in dom dom G (x G y = y \land y G x = y))$
23	22	rexeqbi1dv	$⊢ X = dom dom G \to (\exists x \in X \forall y \in X (x G y = y \land y G x = y) \leftrightarrow \exists x \in dom dom G \forall y \in dom dom G (x G y = y \land y G x = y))$
24	18 21 23	3anbi123d	$⊢ X = dom dom G \to ((G : X \times X ⟶ X \land \forall x \in X \forall y \in X \forall z \in X (x G y) G z = x G (y G z) \land \exists x \in X \forall y \in X (x G y = y \land y G x = y)) \leftrightarrow (G : dom dom G \times dom dom G ⟶ dom dom G \land \forall x \in dom dom G \forall y \in dom dom G \forall z \in dom dom G (x G y) G z = x G (y G z) \land \exists x \in dom dom G \forall y \in dom dom G (x G y = y \land y G x = y)))$
25	24	bibi2d	$⊢ X = dom dom G \to ((G \in MndOp \leftrightarrow (G : X \times X ⟶ X \land \forall x \in X \forall y \in X \forall z \in X (x G y) G z = x G (y G z) \land \exists x \in X \forall y \in X (x G y = y \land y G x = y))) \leftrightarrow (G \in MndOp \leftrightarrow (G : dom dom G \times dom dom G ⟶ dom dom G \land \forall x \in dom dom G \forall y \in dom dom G \forall z \in dom dom G (x G y) G z = x G (y G z) \land \exists x \in dom dom G \forall y \in dom dom G (x G y = y \land y G x = y))))$
26	14 25	syl5ibrcom	$⊢ G \in A \to (X = dom dom G \to (G \in MndOp \leftrightarrow (G : X \times X ⟶ X \land \forall x \in X \forall y \in X \forall z \in X (x G y) G z = x G (y G z) \land \exists x \in X \forall y \in X (x G y = y \land y G x = y))))$
27	6 12 26	pm5.21ndd	$⊢ G \in A \to (G \in MndOp \leftrightarrow (G : X \times X ⟶ X \land \forall x \in X \forall y \in X \forall z \in X (x G y) G z = x G (y G z) \land \exists x \in X \forall y \in X (x G y = y \land y G x = y)))$

Metamath Proof Explorer

Theorem ismndo2

Proof