isexid2

Description: If G e. ( Magma i^i ExId ) , then it has a left and right identity element that belongs to the range of the operation. (Contributed by FL, 12-Dec-2009) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	isexid2.1	$⊢ X = ran G$
	Assertion	isexid2	$⊢ G \in (Magma \cap ExId) \to \exists u \in X \forall x \in X (u G x = x \land x G u = x)$

Proof

Step	Hyp	Ref	Expression
1		isexid2.1	$⊢ X = ran G$
2		rngopidOLD	$⊢ G \in (Magma \cap ExId) \to ran G = dom dom G$
3		elin	$⊢ G \in (Magma \cap ExId) \leftrightarrow (G \in Magma \land G \in ExId)$
4		eqid	$⊢ dom dom G = dom dom G$
5	4	isexid	$⊢ G \in ExId \to (G \in ExId \leftrightarrow \exists u \in dom dom G \forall x \in dom dom G (u G x = x \land x G u = x))$
6	5	ibi	$⊢ G \in ExId \to \exists u \in dom dom G \forall x \in dom dom G (u G x = x \land x G u = x)$
7	6	a1d	$⊢ G \in ExId \to (X = dom dom G \to \exists u \in dom dom G \forall x \in dom dom G (u G x = x \land x G u = x))$
8	7	adantl	$⊢ (G \in Magma \land G \in ExId) \to (X = dom dom G \to \exists u \in dom dom G \forall x \in dom dom G (u G x = x \land x G u = x))$
9	3 8	sylbi	$⊢ G \in (Magma \cap ExId) \to (X = dom dom G \to \exists u \in dom dom G \forall x \in dom dom G (u G x = x \land x G u = x))$
10		eqeq2	$⊢ ran G = dom dom G \to (X = ran G \leftrightarrow X = dom dom G)$
11		raleq	$⊢ ran G = dom dom G \to (\forall x \in ran G (u G x = x \land x G u = x) \leftrightarrow \forall x \in dom dom G (u G x = x \land x G u = x))$
12	11	rexeqbi1dv	$⊢ ran G = dom dom G \to (\exists u \in ran G \forall x \in ran G (u G x = x \land x G u = x) \leftrightarrow \exists u \in dom dom G \forall x \in dom dom G (u G x = x \land x G u = x))$
13	10 12	imbi12d	$⊢ ran G = dom dom G \to ((X = ran G \to \exists u \in ran G \forall x \in ran G (u G x = x \land x G u = x)) \leftrightarrow (X = dom dom G \to \exists u \in dom dom G \forall x \in dom dom G (u G x = x \land x G u = x)))$
14	9 13	imbitrrid	$⊢ ran G = dom dom G \to (G \in (Magma \cap ExId) \to (X = ran G \to \exists u \in ran G \forall x \in ran G (u G x = x \land x G u = x)))$
15	2 14	mpcom	$⊢ G \in (Magma \cap ExId) \to (X = ran G \to \exists u \in ran G \forall x \in ran G (u G x = x \land x G u = x))$
16	15	com12	$⊢ X = ran G \to (G \in (Magma \cap ExId) \to \exists u \in ran G \forall x \in ran G (u G x = x \land x G u = x))$
17		raleq	$⊢ X = ran G \to (\forall x \in X (u G x = x \land x G u = x) \leftrightarrow \forall x \in ran G (u G x = x \land x G u = x))$
18	17	rexeqbi1dv	$⊢ X = ran G \to (\exists u \in X \forall x \in X (u G x = x \land x G u = x) \leftrightarrow \exists u \in ran G \forall x \in ran G (u G x = x \land x G u = x))$
19	16 18	sylibrd	$⊢ X = ran G \to (G \in (Magma \cap ExId) \to \exists u \in X \forall x \in X (u G x = x \land x G u = x))$
20	1 19	ax-mp	$⊢ G \in (Magma \cap ExId) \to \exists u \in X \forall x \in X (u G x = x \land x G u = x)$

Metamath Proof Explorer

Theorem isexid2

Proof