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	bilani	$⊢ (((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$
43		f1oeq3	$⊢ D = Edg (H) \to (J : dom J \underset{1-1 onto}{⟶} D \leftrightarrow J : dom J \underset{1-1 onto}{⟶} Edg (H))$
44	4 43	ax-mp	$⊢ J : dom J \underset{1-1 onto}{⟶} D \leftrightarrow J : dom J \underset{1-1 onto}{⟶} Edg (H)$
45	11 44	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$
46		f1of	$⊢ J : dom J \underset{1-1 onto}{⟶} D \to J : dom J ⟶ D$
47	45 46	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$
48	47	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$
49		f1ocnvdm	$⊢ (M : Edg (G) \underset{1-1 onto}{⟶} D \land J (i) \in D) \to M^{-1} (J (i)) \in Edg (G)$
50	42 48 49	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)$
51		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$
52	39 50 51	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$
53		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$
54	53 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)$
55		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$
56		f1ocnvdm	$⊢ (M : E \underset{1-1 onto}{⟶} D \land J (i) \in D) \to M^{-1} (J (i)) \in E$
57	55 48 56	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$
58	57 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)$
59		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))$
60	54 58 59	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))$
61	60	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)))$
62		f1ocnvfv2	$⊢ (M : E \underset{1-1 onto}{⟶} D \land J (i) \in D) \to M (M^{-1} (J (i))) = J (i)$
63	55 48 62	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)$
64	61 63	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)))))$
65	36 52 64	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))$
66		eqtr2	$⊢ (J (i) = M (I (x)) \land J (i) = M (I (y))) \to M (I (x)) = M (I (y))$
67		f1of1	$⊢ M : E \underset{1-1 onto}{⟶} D \to M : E \underset{1-1}{⟶} D$
68	67	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$
69	68	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$
70	5	iedgedg	$⊢ (Fun I \land x \in dom I) \to I (x) \in Edg (G)$
71	17 70	sylan	$⊢ (G \in USHGraph \land x \in dom I) \to I (x) \in Edg (G)$
72	71 3	eleqtrrdi	$⊢ (G \in USHGraph \land x \in dom I) \to I (x) \in E$
73	72	ex	$⊢ G \in USHGraph \to (x \in dom I \to I (x) \in E)$
74	5	iedgedg	$⊢ (Fun I \land y \in dom I) \to I (y) \in Edg (G)$
75	17 74	sylan	$⊢ (G \in USHGraph \land y \in dom I) \to I (y) \in Edg (G)$
76	75 3	eleqtrrdi	$⊢ (G \in USHGraph \land y \in dom I) \to I (y) \in E$
77	76	ex	$⊢ G \in USHGraph \to (y \in dom I \to I (y) \in E)$
78	73 77	anim12d	$⊢ G \in USHGraph \to ((x \in dom I \land y \in dom I) \to (I (x) \in E \land I (y) \in E))$
79	78	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))$
80	79	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))$
81	80	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)$
82		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))$
83	69 81 82	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))$
84		f1of1	$⊢ I : dom I \underset{1-1 onto}{⟶} Edg (G) \to I : dom I \underset{1-1}{⟶} Edg (G)$
85	37 84	syl	$⊢ G \in USHGraph \to I : dom I \underset{1-1}{⟶} Edg (G)$
86	85	3ad2ant1	$⊢ (G \in USHGraph \land H \in USHGraph \land F \in X) \to I : dom I \underset{1-1}{⟶} Edg (G)$
87	86	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)$
88		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)$
89	87 88	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)$
90	83 89	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)$
91	66 90	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)$
92	91	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)$
93		2fveq3	$⊢ x = y \to M (I (x)) = M (I (y))$
94	93	eqeq2d	$⊢ x = y \to (J (i) = M (I (x)) \leftrightarrow J (i) = M (I (y)))$
95	94	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))$
96	65 92 95	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))$
97	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)$
98	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$
99	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$
100	99	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$
101	98 100	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$
102	101 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)$
103		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))$
104	97 102 103	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))$
105	104	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)))$
106	105	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)))$
107	96 106	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))))$
108	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)$
109		f1of1	$⊢ J : dom J \underset{1-1 onto}{⟶} Edg (H) \to J : dom J \underset{1-1}{⟶} Edg (H)$
110	108 109	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)$
111		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$
112	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$
113		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))))$
114	113	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)))))$
115	110 111 112 114	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)))))$
116	115	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)))))$
117	107 116	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)))$
118	117	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)))$
119	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))))$
120	34 118 119	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$
121		2fveq3	$⊢ x = i \to M (I (x)) = M (I (i))$
122	121	fveq2d	$⊢ x = i \to J^{-1} (M (I (x))) = J^{-1} (M (I (i)))$
123	122	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)))$
124		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$
125		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$
126	8 123 124 125	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)))$
127	126	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))))$
128	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$
129	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$
130	128 129	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$
131	130 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)$
132		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))$
133	11 131 132	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))$
134		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)$
135	134	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)]$
136		simp3	$⊢ (G \in USHGraph \land H \in USHGraph \land F \in X) \to F \in X$
137	136	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$
138	137	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$
139	7 135 129 138	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)]$
140	127 133 139	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)]$
141	140	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)]$
142	120 141	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