isuspgrim0lem

Description: An isomorphism of simple pseudographs is a bijection between their vertices which induces a bijection between their edges. (Contributed by AV, 21-Apr-2025)

	Ref	Expression
Hypotheses	isusgrim.v	$⊢ V = Vtx (G)$
	isusgrim.w	$⊢ W = Vtx (H)$
	isusgrim.e	$⊢ E = Edg (G)$
	isusgrim.d	$⊢ D = Edg (H)$
	isuspgrim0lem.i	$⊢ I = iEdg (G)$
	isuspgrim0lem.j	$⊢ J = iEdg (H)$
	isuspgrim0lem.m	$⊢ M = (x \in E ⟼ F [x])$
	isuspgrim0lem.n	$⊢ N = (x \in dom I ⟼ J^{-1} (M (I (x))))$
Assertion	isuspgrim0lem	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \to (N : dom I \underset{1-1 onto}{⟶} dom J \land \forall i \in dom I J (N (i)) = F [I (i)])$

Proof

Step	Hyp	Ref	Expression
1		isusgrim.v	$⊢ V = Vtx (G)$
2		isusgrim.w	$⊢ W = Vtx (H)$
3		isusgrim.e	$⊢ E = Edg (G)$
4		isusgrim.d	$⊢ D = Edg (H)$
5		isuspgrim0lem.i	$⊢ I = iEdg (G)$
6		isuspgrim0lem.j	$⊢ J = iEdg (H)$
7		isuspgrim0lem.m	$⊢ M = (x \in E ⟼ F [x])$
8		isuspgrim0lem.n	$⊢ N = (x \in dom I ⟼ J^{-1} (M (I (x))))$
9	6	uspgrf1oedg	$⊢ H \in USHGraph \to J : dom J \underset{1-1 onto}{⟶} Edg (H)$
10	9	3ad2ant2	$⊢ (G \in USHGraph \land H \in USHGraph \land F \in X) \to J : dom J \underset{1-1 onto}{⟶} Edg (H)$
11	10	ad2antrr	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \to J : dom J \underset{1-1 onto}{⟶} Edg (H)$
12		f1of	$⊢ M : E \underset{1-1 onto}{⟶} D \to M : E ⟶ D$
13	12	adantl	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \to M : E ⟶ D$
14	13	adantr	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land x \in dom I) \to M : E ⟶ D$
15		uspgruhgr	$⊢ G \in USHGraph \to G \in UHGraph$
16	5	uhgrfun	$⊢ G \in UHGraph \to Fun I$
17	15 16	syl	$⊢ G \in USHGraph \to Fun I$
18		edgval	$⊢ Edg (G) = ran iEdg (G)$
19	5	eqcomi	$⊢ iEdg (G) = I$
20	19	rneqi	$⊢ ran iEdg (G) = ran I$
21	3 18 20	3eqtri	$⊢ E = ran I$
22		feq3	$⊢ E = ran I \to (I : dom I ⟶ E \leftrightarrow I : dom I ⟶ ran I)$
23	21 22	ax-mp	$⊢ I : dom I ⟶ E \leftrightarrow I : dom I ⟶ ran I$
24		fdmrn	$⊢ Fun I \leftrightarrow I : dom I ⟶ ran I$
25	23 24	bitr4i	$⊢ I : dom I ⟶ E \leftrightarrow Fun I$
26	17 25	sylibr	$⊢ G \in USHGraph \to I : dom I ⟶ E$
27	26	3ad2ant1	$⊢ (G \in USHGraph \land H \in USHGraph \land F \in X) \to I : dom I ⟶ E$
28	27	ad2antrr	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \to I : dom I ⟶ E$
29	28	ffvelcdmda	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land x \in dom I) \to I (x) \in E$
30	14 29	ffvelcdmd	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land x \in dom I) \to M (I (x)) \in D$
31	30 4	eleqtrdi	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land x \in dom I) \to M (I (x)) \in Edg (H)$
32		f1ocnvdm	$⊢ (J : dom J \underset{1-1 onto}{⟶} Edg (H) \land M (I (x)) \in Edg (H)) \to J^{-1} (M (I (x))) \in dom J$
33	11 31 32	syl2an2r	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land x \in dom I) \to J^{-1} (M (I (x))) \in dom J$
34	33	ralrimiva	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \to \forall x \in dom I J^{-1} (M (I (x))) \in dom J$
35		2fveq3	$⊢ x = I^{-1} (M^{-1} (J (i))) \to M (I (x)) = M (I (I^{-1} (M^{-1} (J (i)))))$
36	35	eqeq2d	$⊢ x = I^{-1} (M^{-1} (J (i))) \to (J (i) = M (I (x)) \leftrightarrow J (i) = M (I (I^{-1} (M^{-1} (J (i))))))$
37	5	uspgrf1oedg	$⊢ G \in USHGraph \to I : dom I \underset{1-1 onto}{⟶} Edg (G)$
38	37	3ad2ant1	$⊢ (G \in USHGraph \land H \in USHGraph \land F \in X) \to I : dom I \underset{1-1 onto}{⟶} Edg (G)$
39	38	ad2antrr	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \to I : dom I \underset{1-1 onto}{⟶} Edg (G)$
40		f1oeq2	$⊢ E = Edg (G) \to (M : E \underset{1-1 onto}{⟶} D \leftrightarrow M : Edg (G) \underset{1-1 onto}{⟶} D)$
41	3 40	ax-mp	$⊢ M : E \underset{1-1 onto}{⟶} D \leftrightarrow M : Edg (G) \underset{1-1 onto}{⟶} D$
42	41	biimpi	$⊢ M : E \underset{1-1 onto}{⟶} D \to M : Edg (G) \underset{1-1 onto}{⟶} D$
43	42	adantl	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \to M : Edg (G) \underset{1-1 onto}{⟶} D$
44		f1oeq3	$⊢ D = Edg (H) \to (J : dom J \underset{1-1 onto}{⟶} D \leftrightarrow J : dom J \underset{1-1 onto}{⟶} Edg (H))$
45	4 44	ax-mp	$⊢ J : dom J \underset{1-1 onto}{⟶} D \leftrightarrow J : dom J \underset{1-1 onto}{⟶} Edg (H)$
46	11 45	sylibr	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \to J : dom J \underset{1-1 onto}{⟶} D$
47		f1of	$⊢ J : dom J \underset{1-1 onto}{⟶} D \to J : dom J ⟶ D$
48	46 47	syl	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \to J : dom J ⟶ D$
49	48	ffvelcdmda	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \to J (i) \in D$
50		f1ocnvdm	$⊢ (M : Edg (G) \underset{1-1 onto}{⟶} D \land J (i) \in D) \to M^{-1} (J (i)) \in Edg (G)$
51	43 49 50	syl2an2r	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \to M^{-1} (J (i)) \in Edg (G)$
52		f1ocnvdm	$⊢ (I : dom I \underset{1-1 onto}{⟶} Edg (G) \land M^{-1} (J (i)) \in Edg (G)) \to I^{-1} (M^{-1} (J (i))) \in dom I$
53	39 51 52	syl2an2r	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \to I^{-1} (M^{-1} (J (i))) \in dom I$
54		simpll1	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \to G \in USHGraph$
55	54 37	syl	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \to I : dom I \underset{1-1 onto}{⟶} Edg (G)$
56		simpr	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \to M : E \underset{1-1 onto}{⟶} D$
57		f1ocnvdm	$⊢ (M : E \underset{1-1 onto}{⟶} D \land J (i) \in D) \to M^{-1} (J (i)) \in E$
58	56 49 57	syl2an2r	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \to M^{-1} (J (i)) \in E$
59	58 3	eleqtrdi	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \to M^{-1} (J (i)) \in Edg (G)$
60		f1ocnvfv2	$⊢ (I : dom I \underset{1-1 onto}{⟶} Edg (G) \land M^{-1} (J (i)) \in Edg (G)) \to I (I^{-1} (M^{-1} (J (i)))) = M^{-1} (J (i))$
61	55 59 60	syl2an2r	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \to I (I^{-1} (M^{-1} (J (i)))) = M^{-1} (J (i))$
62	61	fveq2d	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \to M (I (I^{-1} (M^{-1} (J (i))))) = M (M^{-1} (J (i)))$
63		f1ocnvfv2	$⊢ (M : E \underset{1-1 onto}{⟶} D \land J (i) \in D) \to M (M^{-1} (J (i))) = J (i)$
64	56 49 63	syl2an2r	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \to M (M^{-1} (J (i))) = J (i)$
65	62 64	eqtr2d	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \to J (i) = M (I (I^{-1} (M^{-1} (J (i)))))$
66	36 53 65	rspcedvdw	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \to \exists x \in dom I J (i) = M (I (x))$
67		eqtr2	$⊢ (J (i) = M (I (x)) \land J (i) = M (I (y))) \to M (I (x)) = M (I (y))$
68		f1of1	$⊢ M : E \underset{1-1 onto}{⟶} D \to M : E \underset{1-1}{⟶} D$
69	68	adantl	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \to M : E \underset{1-1}{⟶} D$
70	69	adantr	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \to M : E \underset{1-1}{⟶} D$
71	5	iedgedg	$⊢ (Fun I \land x \in dom I) \to I (x) \in Edg (G)$
72	17 71	sylan	$⊢ (G \in USHGraph \land x \in dom I) \to I (x) \in Edg (G)$
73	72 3	eleqtrrdi	$⊢ (G \in USHGraph \land x \in dom I) \to I (x) \in E$
74	73	ex	$⊢ G \in USHGraph \to (x \in dom I \to I (x) \in E)$
75	5	iedgedg	$⊢ (Fun I \land y \in dom I) \to I (y) \in Edg (G)$
76	17 75	sylan	$⊢ (G \in USHGraph \land y \in dom I) \to I (y) \in Edg (G)$
77	76 3	eleqtrrdi	$⊢ (G \in USHGraph \land y \in dom I) \to I (y) \in E$
78	77	ex	$⊢ G \in USHGraph \to (y \in dom I \to I (y) \in E)$
79	74 78	anim12d	$⊢ G \in USHGraph \to ((x \in dom I \land y \in dom I) \to (I (x) \in E \land I (y) \in E))$
80	79	3ad2ant1	$⊢ (G \in USHGraph \land H \in USHGraph \land F \in X) \to ((x \in dom I \land y \in dom I) \to (I (x) \in E \land I (y) \in E))$
81	80	ad3antrrr	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \to ((x \in dom I \land y \in dom I) \to (I (x) \in E \land I (y) \in E))$
82	81	imp	$⊢ (((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \land (x \in dom I \land y \in dom I)) \to (I (x) \in E \land I (y) \in E)$
83		f1fveq	$⊢ (M : E \underset{1-1}{⟶} D \land (I (x) \in E \land I (y) \in E)) \to (M (I (x)) = M (I (y)) \leftrightarrow I (x) = I (y))$
84	70 82 83	syl2an2r	$⊢ (((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \land (x \in dom I \land y \in dom I)) \to (M (I (x)) = M (I (y)) \leftrightarrow I (x) = I (y))$
85		f1of1	$⊢ I : dom I \underset{1-1 onto}{⟶} Edg (G) \to I : dom I \underset{1-1}{⟶} Edg (G)$
86	37 85	syl	$⊢ G \in USHGraph \to I : dom I \underset{1-1}{⟶} Edg (G)$
87	86	3ad2ant1	$⊢ (G \in USHGraph \land H \in USHGraph \land F \in X) \to I : dom I \underset{1-1}{⟶} Edg (G)$
88	87	ad3antrrr	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \to I : dom I \underset{1-1}{⟶} Edg (G)$
89		f1veqaeq	$⊢ (I : dom I \underset{1-1}{⟶} Edg (G) \land (x \in dom I \land y \in dom I)) \to (I (x) = I (y) \to x = y)$
90	88 89	sylan	$⊢ (((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \land (x \in dom I \land y \in dom I)) \to (I (x) = I (y) \to x = y)$
91	84 90	sylbid	$⊢ (((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \land (x \in dom I \land y \in dom I)) \to (M (I (x)) = M (I (y)) \to x = y)$
92	67 91	syl5	$⊢ (((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \land (x \in dom I \land y \in dom I)) \to ((J (i) = M (I (x)) \land J (i) = M (I (y))) \to x = y)$
93	92	ralrimivva	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \to \forall x \in dom I \forall y \in dom I ((J (i) = M (I (x)) \land J (i) = M (I (y))) \to x = y)$
94		2fveq3	$⊢ x = y \to M (I (x)) = M (I (y))$
95	94	eqeq2d	$⊢ x = y \to (J (i) = M (I (x)) \leftrightarrow J (i) = M (I (y)))$
96	95	reu4	$⊢ \exists! x \in dom I J (i) = M (I (x)) \leftrightarrow (\exists x \in dom I J (i) = M (I (x)) \land \forall x \in dom I \forall y \in dom I ((J (i) = M (I (x)) \land J (i) = M (I (y))) \to x = y))$
97	66 93 96	sylanbrc	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \to \exists! x \in dom I J (i) = M (I (x))$
98	10	ad3antrrr	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \to J : dom J \underset{1-1 onto}{⟶} Edg (H)$
99	13	ad2antrr	$⊢ (((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \land x \in dom I) \to M : E ⟶ D$
100	27	ad3antrrr	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \to I : dom I ⟶ E$
101	100	ffvelcdmda	$⊢ (((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \land x \in dom I) \to I (x) \in E$
102	99 101	ffvelcdmd	$⊢ (((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \land x \in dom I) \to M (I (x)) \in D$
103	102 4	eleqtrdi	$⊢ (((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \land x \in dom I) \to M (I (x)) \in Edg (H)$
104		f1ocnvfv2	$⊢ (J : dom J \underset{1-1 onto}{⟶} Edg (H) \land M (I (x)) \in Edg (H)) \to J (J^{-1} (M (I (x)))) = M (I (x))$
105	98 103 104	syl2an2r	$⊢ (((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \land x \in dom I) \to J (J^{-1} (M (I (x)))) = M (I (x))$
106	105	eqeq2d	$⊢ (((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \land x \in dom I) \to (J (i) = J (J^{-1} (M (I (x)))) \leftrightarrow J (i) = M (I (x)))$
107	106	reubidva	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \to (\exists! x \in dom I J (i) = J (J^{-1} (M (I (x)))) \leftrightarrow \exists! x \in dom I J (i) = M (I (x)))$
108	97 107	mpbird	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \to \exists! x \in dom I J (i) = J (J^{-1} (M (I (x))))$
109	11	ad2antrr	$⊢ (((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \land x \in dom I) \to J : dom J \underset{1-1 onto}{⟶} Edg (H)$
110		f1of1	$⊢ J : dom J \underset{1-1 onto}{⟶} Edg (H) \to J : dom J \underset{1-1}{⟶} Edg (H)$
111	109 110	syl	$⊢ (((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \land x \in dom I) \to J : dom J \underset{1-1}{⟶} Edg (H)$
112		simplr	$⊢ (((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \land x \in dom I) \to i \in dom J$
113	33	adantlr	$⊢ (((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \land x \in dom I) \to J^{-1} (M (I (x))) \in dom J$
114		f1fveq	$⊢ (J : dom J \underset{1-1}{⟶} Edg (H) \land (i \in dom J \land J^{-1} (M (I (x))) \in dom J)) \to (J (i) = J (J^{-1} (M (I (x)))) \leftrightarrow i = J^{-1} (M (I (x))))$
115	114	bicomd	$⊢ (J : dom J \underset{1-1}{⟶} Edg (H) \land (i \in dom J \land J^{-1} (M (I (x))) \in dom J)) \to (i = J^{-1} (M (I (x))) \leftrightarrow J (i) = J (J^{-1} (M (I (x)))))$
116	111 112 113 115	syl12anc	$⊢ (((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \land x \in dom I) \to (i = J^{-1} (M (I (x))) \leftrightarrow J (i) = J (J^{-1} (M (I (x)))))$
117	116	reubidva	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \to (\exists! x \in dom I i = J^{-1} (M (I (x))) \leftrightarrow \exists! x \in dom I J (i) = J (J^{-1} (M (I (x)))))$
118	108 117	mpbird	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom J) \to \exists! x \in dom I i = J^{-1} (M (I (x)))$
119	118	ralrimiva	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \to \forall i \in dom J \exists! x \in dom I i = J^{-1} (M (I (x)))$
120	8	f1ompt	$⊢ N : dom I \underset{1-1 onto}{⟶} dom J \leftrightarrow (\forall x \in dom I J^{-1} (M (I (x))) \in dom J \land \forall i \in dom J \exists! x \in dom I i = J^{-1} (M (I (x))))$
121	34 119 120	sylanbrc	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \to N : dom I \underset{1-1 onto}{⟶} dom J$
122		2fveq3	$⊢ x = i \to M (I (x)) = M (I (i))$
123	122	fveq2d	$⊢ x = i \to J^{-1} (M (I (x))) = J^{-1} (M (I (i)))$
124	123	adantl	$⊢ (((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom I) \land x = i) \to J^{-1} (M (I (x))) = J^{-1} (M (I (i)))$
125		simpr	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom I) \to i \in dom I$
126		fvexd	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom I) \to J^{-1} (M (I (i))) \in V$
127	8 124 125 126	fvmptd2	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom I) \to N (i) = J^{-1} (M (I (i)))$
128	127	fveq2d	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom I) \to J (N (i)) = J (J^{-1} (M (I (i))))$
129	13	adantr	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom I) \to M : E ⟶ D$
130	28	ffvelcdmda	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom I) \to I (i) \in E$
131	129 130	ffvelcdmd	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom I) \to M (I (i)) \in D$
132	131 4	eleqtrdi	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom I) \to M (I (i)) \in Edg (H)$
133		f1ocnvfv2	$⊢ (J : dom J \underset{1-1 onto}{⟶} Edg (H) \land M (I (i)) \in Edg (H)) \to J (J^{-1} (M (I (i)))) = M (I (i))$
134	11 132 133	syl2an2r	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom I) \to J (J^{-1} (M (I (i)))) = M (I (i))$
135		simpr	$⊢ (((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom I) \land x = I (i)) \to x = I (i)$
136	135	imaeq2d	$⊢ (((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom I) \land x = I (i)) \to F [x] = F [I (i)]$
137		simp3	$⊢ (G \in USHGraph \land H \in USHGraph \land F \in X) \to F \in X$
138	137	ad3antrrr	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom I) \to F \in X$
139	138	imaexd	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom I) \to F [I (i)] \in V$
140	7 136 130 139	fvmptd2	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom I) \to M (I (i)) = F [I (i)]$
141	128 134 140	3eqtrd	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \land i \in dom I) \to J (N (i)) = F [I (i)]$
142	141	ralrimiva	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \to \forall i \in dom I J (N (i)) = F [I (i)]$
143	121 142	jca	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land M : E \underset{1-1 onto}{⟶} D) \to (N : dom I \underset{1-1 onto}{⟶} dom J \land \forall i \in dom I J (N (i)) = F [I (i)])$

Metamath Proof Explorer

Theorem isuspgrim0lem

Proof