Metamath Proof Explorer

Theorem isexid

Description: The predicate G has a left and right identity element. (Contributed by FL, 2-Nov-2009) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	isexid.1	$⊢ X = dom dom G$
	Assertion	isexid	$⊢ G \in A \to (G \in ExId \leftrightarrow \exists x \in X \forall y \in X (x G y = y \land y G x = y))$

Proof

Step	Hyp	Ref	Expression
1		isexid.1	$⊢ X = dom dom G$
2		dmeq	$⊢ g = G \to dom g = dom G$
3	2	dmeqd	$⊢ g = G \to dom dom g = dom dom G$
4	3 1	eqtr4di	$⊢ g = G \to dom dom g = X$
5		oveq	$⊢ g = G \to x g y = x G y$
6	5	eqeq1d	$⊢ g = G \to (x g y = y \leftrightarrow x G y = y)$
7		oveq	$⊢ g = G \to y g x = y G x$
8	7	eqeq1d	$⊢ g = G \to (y g x = y \leftrightarrow y G x = y)$
9	6 8	anbi12d	$⊢ g = G \to ((x g y = y \land y g x = y) \leftrightarrow (x G y = y \land y G x = y))$
10	4 9	raleqbidv	$⊢ g = G \to (\forall y \in dom dom g (x g y = y \land y g x = y) \leftrightarrow \forall y \in X (x G y = y \land y G x = y))$
11	4 10	rexeqbidv	$⊢ g = G \to (\exists x \in dom dom g \forall y \in dom dom g (x g y = y \land y g x = y) \leftrightarrow \exists x \in X \forall y \in X (x G y = y \land y G x = y))$
12		df-exid	$⊢ ExId = \{g \| \exists x \in dom dom g \forall y \in dom dom g (x g y = y \land y g x = y)\}$
13	11 12	elab2g	$⊢ G \in A \to (G \in ExId \leftrightarrow \exists x \in X \forall y \in X (x G y = y \land y G x = y))$