exidreslem

	Ref	Expression
Hypotheses	exidres.1	$⊢ X = ran G$
	exidres.2	$⊢ U = GId (G)$
	exidres.3	$⊢ H = {G ↾}_{(Y \times Y)}$
Assertion	exidreslem	$⊢ (G \in (Magma \cap ExId) \land Y \subseteq X \land U \in Y) \to (U \in dom dom H \land \forall x \in dom dom H (U H x = x \land x H U = x))$

Proof

Step	Hyp	Ref	Expression
1		exidres.1	$⊢ X = ran G$
2		exidres.2	$⊢ U = GId (G)$
3		exidres.3	$⊢ H = {G ↾}_{(Y \times Y)}$
4	3	dmeqi	$⊢ dom H = dom ({G ↾}_{(Y \times Y)})$
5		xpss12	$⊢ (Y \subseteq X \land Y \subseteq X) \to Y \times Y \subseteq X \times X$
6	5	anidms	$⊢ Y \subseteq X \to Y \times Y \subseteq X \times X$
7	1	opidon2OLD	$⊢ G \in (Magma \cap ExId) \to G : X \times X \underset{onto}{⟶} X$
8		fof	$⊢ G : X \times X \underset{onto}{⟶} X \to G : X \times X ⟶ X$
9		fdm	$⊢ G : X \times X ⟶ X \to dom G = X \times X$
10	7 8 9	3syl	$⊢ G \in (Magma \cap ExId) \to dom G = X \times X$
11	10	sseq2d	$⊢ G \in (Magma \cap ExId) \to (Y \times Y \subseteq dom G \leftrightarrow Y \times Y \subseteq X \times X)$
12	6 11	syl5ibr	$⊢ G \in (Magma \cap ExId) \to (Y \subseteq X \to Y \times Y \subseteq dom G)$
13	12	imp	$⊢ (G \in (Magma \cap ExId) \land Y \subseteq X) \to Y \times Y \subseteq dom G$
14		ssdmres	$⊢ Y \times Y \subseteq dom G \leftrightarrow dom ({G ↾}_{(Y \times Y)}) = Y \times Y$
15	13 14	sylib	$⊢ (G \in (Magma \cap ExId) \land Y \subseteq X) \to dom ({G ↾}_{(Y \times Y)}) = Y \times Y$
16	4 15	eqtrid	$⊢ (G \in (Magma \cap ExId) \land Y \subseteq X) \to dom H = Y \times Y$
17	16	dmeqd	$⊢ (G \in (Magma \cap ExId) \land Y \subseteq X) \to dom dom H = dom (Y \times Y)$
18		dmxpid	$⊢ dom (Y \times Y) = Y$
19	17 18	eqtrdi	$⊢ (G \in (Magma \cap ExId) \land Y \subseteq X) \to dom dom H = Y$
20	19	eleq2d	$⊢ (G \in (Magma \cap ExId) \land Y \subseteq X) \to (U \in dom dom H \leftrightarrow U \in Y)$
21	20	biimp3ar	$⊢ (G \in (Magma \cap ExId) \land Y \subseteq X \land U \in Y) \to U \in dom dom H$
22		ssel2	$⊢ (Y \subseteq X \land x \in Y) \to x \in X$
23	1 2	cmpidelt	$⊢ (G \in (Magma \cap ExId) \land x \in X) \to (U G x = x \land x G U = x)$
24	22 23	sylan2	$⊢ (G \in (Magma \cap ExId) \land (Y \subseteq X \land x \in Y)) \to (U G x = x \land x G U = x)$
25	24	anassrs	$⊢ ((G \in (Magma \cap ExId) \land Y \subseteq X) \land x \in Y) \to (U G x = x \land x G U = x)$
26	25	adantrl	$⊢ ((G \in (Magma \cap ExId) \land Y \subseteq X) \land (U \in Y \land x \in Y)) \to (U G x = x \land x G U = x)$
27	3	oveqi	$⊢ U H x = U ({G ↾}_{(Y \times Y)}) x$
28		ovres	$⊢ (U \in Y \land x \in Y) \to U ({G ↾}_{(Y \times Y)}) x = U G x$
29	27 28	eqtrid	$⊢ (U \in Y \land x \in Y) \to U H x = U G x$
30	29	eqeq1d	$⊢ (U \in Y \land x \in Y) \to (U H x = x \leftrightarrow U G x = x)$
31	3	oveqi	$⊢ x H U = x ({G ↾}_{(Y \times Y)}) U$
32		ovres	$⊢ (x \in Y \land U \in Y) \to x ({G ↾}_{(Y \times Y)}) U = x G U$
33	31 32	eqtrid	$⊢ (x \in Y \land U \in Y) \to x H U = x G U$
34	33	ancoms	$⊢ (U \in Y \land x \in Y) \to x H U = x G U$
35	34	eqeq1d	$⊢ (U \in Y \land x \in Y) \to (x H U = x \leftrightarrow x G U = x)$
36	30 35	anbi12d	$⊢ (U \in Y \land x \in Y) \to ((U H x = x \land x H U = x) \leftrightarrow (U G x = x \land x G U = x))$
37	36	adantl	$⊢ ((G \in (Magma \cap ExId) \land Y \subseteq X) \land (U \in Y \land x \in Y)) \to ((U H x = x \land x H U = x) \leftrightarrow (U G x = x \land x G U = x))$
38	26 37	mpbird	$⊢ ((G \in (Magma \cap ExId) \land Y \subseteq X) \land (U \in Y \land x \in Y)) \to (U H x = x \land x H U = x)$
39	38	anassrs	$⊢ (((G \in (Magma \cap ExId) \land Y \subseteq X) \land U \in Y) \land x \in Y) \to (U H x = x \land x H U = x)$
40	39	ralrimiva	$⊢ ((G \in (Magma \cap ExId) \land Y \subseteq X) \land U \in Y) \to \forall x \in Y (U H x = x \land x H U = x)$
41	40	3impa	$⊢ (G \in (Magma \cap ExId) \land Y \subseteq X \land U \in Y) \to \forall x \in Y (U H x = x \land x H U = x)$
42	13	3adant3	$⊢ (G \in (Magma \cap ExId) \land Y \subseteq X \land U \in Y) \to Y \times Y \subseteq dom G$
43	42 14	sylib	$⊢ (G \in (Magma \cap ExId) \land Y \subseteq X \land U \in Y) \to dom ({G ↾}_{(Y \times Y)}) = Y \times Y$
44	4 43	eqtrid	$⊢ (G \in (Magma \cap ExId) \land Y \subseteq X \land U \in Y) \to dom H = Y \times Y$
45	44	dmeqd	$⊢ (G \in (Magma \cap ExId) \land Y \subseteq X \land U \in Y) \to dom dom H = dom (Y \times Y)$
46	45 18	eqtrdi	$⊢ (G \in (Magma \cap ExId) \land Y \subseteq X \land U \in Y) \to dom dom H = Y$
47	46	raleqdv	$⊢ (G \in (Magma \cap ExId) \land Y \subseteq X \land U \in Y) \to (\forall x \in dom dom H (U H x = x \land x H U = x) \leftrightarrow \forall x \in Y (U H x = x \land x H U = x))$
48	41 47	mpbird	$⊢ (G \in (Magma \cap ExId) \land Y \subseteq X \land U \in Y) \to \forall x \in dom dom H (U H x = x \land x H U = x)$
49	21 48	jca	$⊢ (G \in (Magma \cap ExId) \land Y \subseteq X \land U \in Y) \to (U \in dom dom H \land \forall x \in dom dom H (U H x = x \land x H U = x))$

Metamath Proof Explorer

Theorem exidreslem

Proof