Metamath Proof Explorer

Theorem grpoidval

Description: Lemma for grpoidcl and others. (Contributed by NM, 5-Feb-2010) (Proof shortened by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	grpoidval.1	$⊢ X = ran G$
		grpoidval.2	$⊢ U = GId (G)$
	Assertion	grpoidval	$⊢ G \in GrpOp \to U = (ι u \in X \| \forall x \in X u G x = x)$

Proof

Step	Hyp	Ref	Expression
1		grpoidval.1	$⊢ X = ran G$
2		grpoidval.2	$⊢ U = GId (G)$
3	1	gidval	$⊢ G \in GrpOp \to GId (G) = (ι u \in X \| \forall x \in X (u G x = x \land x G u = x))$
4		simpl	$⊢ (u G x = x \land x G u = x) \to u G x = x$
5	4	ralimi	$⊢ \forall x \in X (u G x = x \land x G u = x) \to \forall x \in X u G x = x$
6	5	rgenw	$⊢ \forall u \in X (\forall x \in X (u G x = x \land x G u = x) \to \forall x \in X u G x = x)$
7	6	a1i	$⊢ G \in GrpOp \to \forall u \in X (\forall x \in X (u G x = x \land x G u = x) \to \forall x \in X u G x = x)$
8	1	grpoidinv	$⊢ G \in GrpOp \to \exists u \in X \forall x \in X ((u G x = x \land x G u = x) \land \exists y \in X (y G x = u \land x G y = u))$
9		simpl	$⊢ ((u G x = x \land x G u = x) \land \exists y \in X (y G x = u \land x G y = u)) \to (u G x = x \land x G u = x)$
10	9	ralimi	$⊢ \forall x \in X ((u G x = x \land x G u = x) \land \exists y \in X (y G x = u \land x G y = u)) \to \forall x \in X (u G x = x \land x G u = x)$
11	10	reximi	$⊢ \exists u \in X \forall x \in X ((u G x = x \land x G u = x) \land \exists y \in X (y G x = u \land x G y = u)) \to \exists u \in X \forall x \in X (u G x = x \land x G u = x)$
12	8 11	syl	$⊢ G \in GrpOp \to \exists u \in X \forall x \in X (u G x = x \land x G u = x)$
13	1	grpoideu	$⊢ G \in GrpOp \to \exists! u \in X \forall x \in X u G x = x$
14	7 12 13	3jca	$⊢ G \in GrpOp \to (\forall u \in X (\forall x \in X (u G x = x \land x G u = x) \to \forall x \in X u G x = x) \land \exists u \in X \forall x \in X (u G x = x \land x G u = x) \land \exists! u \in X \forall x \in X u G x = x)$
15		reupick2	$⊢ ((\forall u \in X (\forall x \in X (u G x = x \land x G u = x) \to \forall x \in X u G x = x) \land \exists u \in X \forall x \in X (u G x = x \land x G u = x) \land \exists! u \in X \forall x \in X u G x = x) \land u \in X) \to (\forall x \in X u G x = x \leftrightarrow \forall x \in X (u G x = x \land x G u = x))$
16	14 15	sylan	$⊢ (G \in GrpOp \land u \in X) \to (\forall x \in X u G x = x \leftrightarrow \forall x \in X (u G x = x \land x G u = x))$
17	16	riotabidva	$⊢ G \in GrpOp \to (ι u \in X \| \forall x \in X u G x = x) = (ι u \in X \| \forall x \in X (u G x = x \land x G u = x))$
18	3 17	eqtr4d	$⊢ G \in GrpOp \to GId (G) = (ι u \in X \| \forall x \in X u G x = x)$
19	2 18	eqtrid	$⊢ G \in GrpOp \to U = (ι u \in X \| \forall x \in X u G x = x)$