isuspgrim0

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)$
Assertion	isuspgrim0	$⊢ (G \in USHGraph \land H \in USHGraph \land F \in X) \to (F \in (G GraphIso H) \leftrightarrow (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D))$

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		eqid	$⊢ iEdg (G) = iEdg (G)$
6		eqid	$⊢ iEdg (H) = iEdg (H)$
7	1 2 5 6	isgrim	$⊢ (G \in USHGraph \land H \in USHGraph \land F \in X) \to (F \in (G GraphIso H) \leftrightarrow (F : V \underset{1-1 onto}{⟶} W \land \exists j (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])))$
8	3	eleq2i	$⊢ e \in E \leftrightarrow e \in Edg (G)$
9		uspgruhgr	$⊢ G \in USHGraph \to G \in UHGraph$
10	5	uhgredgiedgb	$⊢ G \in UHGraph \to (e \in Edg (G) \leftrightarrow \exists k \in dom iEdg (G) e = iEdg (G) (k))$
11	9 10	syl	$⊢ G \in USHGraph \to (e \in Edg (G) \leftrightarrow \exists k \in dom iEdg (G) e = iEdg (G) (k))$
12	8 11	bitrid	$⊢ G \in USHGraph \to (e \in E \leftrightarrow \exists k \in dom iEdg (G) e = iEdg (G) (k))$
13	12	3ad2ant1	$⊢ (G \in USHGraph \land H \in USHGraph \land F \in X) \to (e \in E \leftrightarrow \exists k \in dom iEdg (G) e = iEdg (G) (k))$
14	13	ad2antrr	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \to (e \in E \leftrightarrow \exists k \in dom iEdg (G) e = iEdg (G) (k))$
15	14	biimpa	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land e \in E) \to \exists k \in dom iEdg (G) e = iEdg (G) (k)$
16		2fveq3	$⊢ i = k \to iEdg (H) (j (i)) = iEdg (H) (j (k))$
17		fveq2	$⊢ i = k \to iEdg (G) (i) = iEdg (G) (k)$
18	17	imaeq2d	$⊢ i = k \to F [iEdg (G) (i)] = F [iEdg (G) (k)]$
19	16 18	eqeq12d	$⊢ i = k \to (iEdg (H) (j (i)) = F [iEdg (G) (i)] \leftrightarrow iEdg (H) (j (k)) = F [iEdg (G) (k)])$
20	19	rspcv	$⊢ k \in dom iEdg (G) \to (\forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)] \to iEdg (H) (j (k)) = F [iEdg (G) (k)])$
21	20	adantl	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in dom iEdg (G)) \to (\forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)] \to iEdg (H) (j (k)) = F [iEdg (G) (k)])$
22		uspgruhgr	$⊢ H \in USHGraph \to H \in UHGraph$
23	6	uhgrfun	$⊢ H \in UHGraph \to Fun iEdg (H)$
24	22 23	syl	$⊢ H \in USHGraph \to Fun iEdg (H)$
25	24	3ad2ant2	$⊢ (G \in USHGraph \land H \in USHGraph \land F \in X) \to Fun iEdg (H)$
26	25	ad3antrrr	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in dom iEdg (G)) \to Fun iEdg (H)$
27		f1of	$⊢ j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \to j : dom iEdg (G) ⟶ dom iEdg (H)$
28	27	adantl	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \to j : dom iEdg (G) ⟶ dom iEdg (H)$
29	28	ffvelcdmda	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in dom iEdg (G)) \to j (k) \in dom iEdg (H)$
30	6	iedgedg	$⊢ (Fun iEdg (H) \land j (k) \in dom iEdg (H)) \to iEdg (H) (j (k)) \in Edg (H)$
31	26 29 30	syl2anc	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in dom iEdg (G)) \to iEdg (H) (j (k)) \in Edg (H)$
32	4	eleq2i	$⊢ iEdg (H) (j (k)) \in D \leftrightarrow iEdg (H) (j (k)) \in Edg (H)$
33	31 32	sylibr	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in dom iEdg (G)) \to iEdg (H) (j (k)) \in D$
34		eleq1	$⊢ iEdg (H) (j (k)) = F [iEdg (G) (k)] \to (iEdg (H) (j (k)) \in D \leftrightarrow F [iEdg (G) (k)] \in D)$
35	33 34	syl5ibcom	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in dom iEdg (G)) \to (iEdg (H) (j (k)) = F [iEdg (G) (k)] \to F [iEdg (G) (k)] \in D)$
36	21 35	syld	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in dom iEdg (G)) \to (\forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)] \to F [iEdg (G) (k)] \in D)$
37	36	ex	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \to (k \in dom iEdg (G) \to (\forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)] \to F [iEdg (G) (k)] \in D))$
38	37	com23	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \to (\forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)] \to (k \in dom iEdg (G) \to F [iEdg (G) (k)] \in D))$
39	38	impr	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \to (k \in dom iEdg (G) \to F [iEdg (G) (k)] \in D)$
40	39	adantr	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land e \in E) \to (k \in dom iEdg (G) \to F [iEdg (G) (k)] \in D)$
41	40	imp	$⊢ (((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land e \in E) \land k \in dom iEdg (G)) \to F [iEdg (G) (k)] \in D$
42		imaeq2	$⊢ e = iEdg (G) (k) \to F [e] = F [iEdg (G) (k)]$
43	42	eleq1d	$⊢ e = iEdg (G) (k) \to (F [e] \in D \leftrightarrow F [iEdg (G) (k)] \in D)$
44	41 43	syl5ibrcom	$⊢ (((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land e \in E) \land k \in dom iEdg (G)) \to (e = iEdg (G) (k) \to F [e] \in D)$
45	44	rexlimdva	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land e \in E) \to (\exists k \in dom iEdg (G) e = iEdg (G) (k) \to F [e] \in D)$
46	15 45	mpd	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land e \in E) \to F [e] \in D$
47	46	ralrimiva	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \to \forall e \in E F [e] \in D$
48	4	eleq2i	$⊢ d \in D \leftrightarrow d \in Edg (H)$
49	6	uhgredgiedgb	$⊢ H \in UHGraph \to (d \in Edg (H) \leftrightarrow \exists k \in dom iEdg (H) d = iEdg (H) (k))$
50	22 49	syl	$⊢ H \in USHGraph \to (d \in Edg (H) \leftrightarrow \exists k \in dom iEdg (H) d = iEdg (H) (k))$
51	48 50	bitrid	$⊢ H \in USHGraph \to (d \in D \leftrightarrow \exists k \in dom iEdg (H) d = iEdg (H) (k))$
52	51	3ad2ant2	$⊢ (G \in USHGraph \land H \in USHGraph \land F \in X) \to (d \in D \leftrightarrow \exists k \in dom iEdg (H) d = iEdg (H) (k))$
53	52	ad2antrr	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \to (d \in D \leftrightarrow \exists k \in dom iEdg (H) d = iEdg (H) (k))$
54		simprl	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \to j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)$
55		f1ocnvdm	$⊢ (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land k \in dom iEdg (H)) \to j^{-1} (k) \in dom iEdg (G)$
56	54 55	sylan	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land k \in dom iEdg (H)) \to j^{-1} (k) \in dom iEdg (G)$
57		2fveq3	$⊢ i = j^{-1} (k) \to iEdg (H) (j (i)) = iEdg (H) (j (j^{-1} (k)))$
58		fveq2	$⊢ i = j^{-1} (k) \to iEdg (G) (i) = iEdg (G) (j^{-1} (k))$
59	58	imaeq2d	$⊢ i = j^{-1} (k) \to F [iEdg (G) (i)] = F [iEdg (G) (j^{-1} (k))]$
60	57 59	eqeq12d	$⊢ i = j^{-1} (k) \to (iEdg (H) (j (i)) = F [iEdg (G) (i)] \leftrightarrow iEdg (H) (j (j^{-1} (k))) = F [iEdg (G) (j^{-1} (k))])$
61	60	rspccv	$⊢ \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)] \to (j^{-1} (k) \in dom iEdg (G) \to iEdg (H) (j (j^{-1} (k))) = F [iEdg (G) (j^{-1} (k))])$
62	61	adantl	$⊢ (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)]) \to (j^{-1} (k) \in dom iEdg (G) \to iEdg (H) (j (j^{-1} (k))) = F [iEdg (G) (j^{-1} (k))])$
63	62	adantl	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \to (j^{-1} (k) \in dom iEdg (G) \to iEdg (H) (j (j^{-1} (k))) = F [iEdg (G) (j^{-1} (k))])$
64	63	adantr	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land k \in dom iEdg (H)) \to (j^{-1} (k) \in dom iEdg (G) \to iEdg (H) (j (j^{-1} (k))) = F [iEdg (G) (j^{-1} (k))])$
65		f1ocnvfv2	$⊢ (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land k \in dom iEdg (H)) \to j (j^{-1} (k)) = k$
66	54 65	sylan	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land k \in dom iEdg (H)) \to j (j^{-1} (k)) = k$
67	66	fveqeq2d	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land k \in dom iEdg (H)) \to (iEdg (H) (j (j^{-1} (k))) = F [iEdg (G) (j^{-1} (k))] \leftrightarrow iEdg (H) (k) = F [iEdg (G) (j^{-1} (k))])$
68		eqeq2	$⊢ iEdg (H) (k) = F [iEdg (G) (j^{-1} (k))] \to (d = iEdg (H) (k) \leftrightarrow d = F [iEdg (G) (j^{-1} (k))])$
69	68	adantl	$⊢ (((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land k \in dom iEdg (H)) \land iEdg (H) (k) = F [iEdg (G) (j^{-1} (k))]) \to (d = iEdg (H) (k) \leftrightarrow d = F [iEdg (G) (j^{-1} (k))])$
70		simpll1	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \to G \in USHGraph$
71	3 5	uspgriedgedg	$⊢ (G \in USHGraph \land j^{-1} (k) \in dom iEdg (G)) \to \exists! e \in E e = iEdg (G) (j^{-1} (k))$
72	70 56 71	syl2an2r	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land k \in dom iEdg (H)) \to \exists! e \in E e = iEdg (G) (j^{-1} (k))$
73		eqcom	$⊢ iEdg (G) (j^{-1} (k)) = e \leftrightarrow e = iEdg (G) (j^{-1} (k))$
74	73	reubii	$⊢ \exists! e \in E iEdg (G) (j^{-1} (k)) = e \leftrightarrow \exists! e \in E e = iEdg (G) (j^{-1} (k))$
75	72 74	sylibr	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land k \in dom iEdg (H)) \to \exists! e \in E iEdg (G) (j^{-1} (k)) = e$
76		f1of1	$⊢ F : V \underset{1-1 onto}{⟶} W \to F : V \underset{1-1}{⟶} W$
77	76	ad4antlr	$⊢ (((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land k \in dom iEdg (H)) \land e \in E) \to F : V \underset{1-1}{⟶} W$
78		uspgrupgr	$⊢ G \in USHGraph \to G \in UPGraph$
79	78	3ad2ant1	$⊢ (G \in USHGraph \land H \in USHGraph \land F \in X) \to G \in UPGraph$
80	79	ad3antrrr	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land k \in dom iEdg (H)) \to G \in UPGraph$
81	80 56	jca	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land k \in dom iEdg (H)) \to (G \in UPGraph \land j^{-1} (k) \in dom iEdg (G))$
82	81	adantr	$⊢ (((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land k \in dom iEdg (H)) \land e \in E) \to (G \in UPGraph \land j^{-1} (k) \in dom iEdg (G))$
83	1 5	upgrss	$⊢ (G \in UPGraph \land j^{-1} (k) \in dom iEdg (G)) \to iEdg (G) (j^{-1} (k)) \subseteq V$
84	82 83	syl	$⊢ (((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land k \in dom iEdg (H)) \land e \in E) \to iEdg (G) (j^{-1} (k)) \subseteq V$
85	8	biimpi	$⊢ e \in E \to e \in Edg (G)$
86		edgupgr	$⊢ (G \in UPGraph \land e \in Edg (G)) \to (e \in 𝒫 Vtx (G) \land e \neq \emptyset \land \|e\| \leq 2)$
87	80 85 86	syl2an	$⊢ (((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land k \in dom iEdg (H)) \land e \in E) \to (e \in 𝒫 Vtx (G) \land e \neq \emptyset \land \|e\| \leq 2)$
88	87	simp1d	$⊢ (((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land k \in dom iEdg (H)) \land e \in E) \to e \in 𝒫 Vtx (G)$
89	88	elpwid	$⊢ (((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land k \in dom iEdg (H)) \land e \in E) \to e \subseteq Vtx (G)$
90	89 1	sseqtrrdi	$⊢ (((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land k \in dom iEdg (H)) \land e \in E) \to e \subseteq V$
91		f1imaeq	$⊢ (F : V \underset{1-1}{⟶} W \land (iEdg (G) (j^{-1} (k)) \subseteq V \land e \subseteq V)) \to (F [iEdg (G) (j^{-1} (k))] = F [e] \leftrightarrow iEdg (G) (j^{-1} (k)) = e)$
92	77 84 90 91	syl12anc	$⊢ (((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land k \in dom iEdg (H)) \land e \in E) \to (F [iEdg (G) (j^{-1} (k))] = F [e] \leftrightarrow iEdg (G) (j^{-1} (k)) = e)$
93	92	reubidva	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land k \in dom iEdg (H)) \to (\exists! e \in E F [iEdg (G) (j^{-1} (k))] = F [e] \leftrightarrow \exists! e \in E iEdg (G) (j^{-1} (k)) = e)$
94	75 93	mpbird	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land k \in dom iEdg (H)) \to \exists! e \in E F [iEdg (G) (j^{-1} (k))] = F [e]$
95	94	ad2antrr	$⊢ ((((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land k \in dom iEdg (H)) \land iEdg (H) (k) = F [iEdg (G) (j^{-1} (k))]) \land d = F [iEdg (G) (j^{-1} (k))]) \to \exists! e \in E F [iEdg (G) (j^{-1} (k))] = F [e]$
96		eqeq1	$⊢ d = F [iEdg (G) (j^{-1} (k))] \to (d = F [e] \leftrightarrow F [iEdg (G) (j^{-1} (k))] = F [e])$
97	96	reubidv	$⊢ d = F [iEdg (G) (j^{-1} (k))] \to (\exists! e \in E d = F [e] \leftrightarrow \exists! e \in E F [iEdg (G) (j^{-1} (k))] = F [e])$
98	97	adantl	$⊢ ((((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land k \in dom iEdg (H)) \land iEdg (H) (k) = F [iEdg (G) (j^{-1} (k))]) \land d = F [iEdg (G) (j^{-1} (k))]) \to (\exists! e \in E d = F [e] \leftrightarrow \exists! e \in E F [iEdg (G) (j^{-1} (k))] = F [e])$
99	95 98	mpbird	$⊢ ((((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land k \in dom iEdg (H)) \land iEdg (H) (k) = F [iEdg (G) (j^{-1} (k))]) \land d = F [iEdg (G) (j^{-1} (k))]) \to \exists! e \in E d = F [e]$
100	99	ex	$⊢ (((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land k \in dom iEdg (H)) \land iEdg (H) (k) = F [iEdg (G) (j^{-1} (k))]) \to (d = F [iEdg (G) (j^{-1} (k))] \to \exists! e \in E d = F [e])$
101	69 100	sylbid	$⊢ (((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land k \in dom iEdg (H)) \land iEdg (H) (k) = F [iEdg (G) (j^{-1} (k))]) \to (d = iEdg (H) (k) \to \exists! e \in E d = F [e])$
102	101	ex	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land k \in dom iEdg (H)) \to (iEdg (H) (k) = F [iEdg (G) (j^{-1} (k))] \to (d = iEdg (H) (k) \to \exists! e \in E d = F [e]))$
103	67 102	sylbid	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land k \in dom iEdg (H)) \to (iEdg (H) (j (j^{-1} (k))) = F [iEdg (G) (j^{-1} (k))] \to (d = iEdg (H) (k) \to \exists! e \in E d = F [e]))$
104	64 103	syld	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land k \in dom iEdg (H)) \to (j^{-1} (k) \in dom iEdg (G) \to (d = iEdg (H) (k) \to \exists! e \in E d = F [e]))$
105	56 104	mpd	$⊢ ((((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land k \in dom iEdg (H)) \to (d = iEdg (H) (k) \to \exists! e \in E d = F [e])$
106	105	rexlimdva	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \to (\exists k \in dom iEdg (H) d = iEdg (H) (k) \to \exists! e \in E d = F [e])$
107	53 106	sylbid	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \to (d \in D \to \exists! e \in E d = F [e])$
108	107	ralrimiv	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \to \forall d \in D \exists! e \in E d = F [e]$
109		imaeq2	$⊢ x = e \to F [x] = F [e]$
110	109	cbvmptv	$⊢ (x \in E ⟼ F [x]) = (e \in E ⟼ F [e])$
111	110	f1ompt	$⊢ (x \in E ⟼ F [x]) : E \underset{1-1 onto}{⟶} D \leftrightarrow (\forall e \in E F [e] \in D \land \forall d \in D \exists! e \in E d = F [e])$
112	47 108 111	sylanbrc	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \to (x \in E ⟼ F [x]) : E \underset{1-1 onto}{⟶} D$
113	112	ex	$⊢ ((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \to ((j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)]) \to (x \in E ⟼ F [x]) : E \underset{1-1 onto}{⟶} D)$
114	113	exlimdv	$⊢ ((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \to (\exists j (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)]) \to (x \in E ⟼ F [x]) : E \underset{1-1 onto}{⟶} D)$
115		fvex	$⊢ iEdg (G) \in V$
116	115	dmex	$⊢ dom iEdg (G) \in V$
117	116	mptex	$⊢ (e \in dom iEdg (G) ⟼ {iEdg (H)}^{-1} ((x \in E ⟼ F [x]) (iEdg (G) (e)))) \in V$
118	117	a1i	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (x \in E ⟼ F [x]) : E \underset{1-1 onto}{⟶} D) \to (e \in dom iEdg (G) ⟼ {iEdg (H)}^{-1} ((x \in E ⟼ F [x]) (iEdg (G) (e)))) \in V$
119		eqid	$⊢ (e \in dom iEdg (G) ⟼ {iEdg (H)}^{-1} ((x \in E ⟼ F [x]) (iEdg (G) (e)))) = (e \in dom iEdg (G) ⟼ {iEdg (H)}^{-1} ((x \in E ⟼ F [x]) (iEdg (G) (e))))$
120	1 2 3 4 5 6 110 119	isuspgrim0lem	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (x \in E ⟼ F [x]) : E \underset{1-1 onto}{⟶} D) \to ((e \in dom iEdg (G) ⟼ {iEdg (H)}^{-1} ((x \in E ⟼ F [x]) (iEdg (G) (e)))) : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) ((e \in dom iEdg (G) ⟼ {iEdg (H)}^{-1} ((x \in E ⟼ F [x]) (iEdg (G) (e)))) (i)) = F [iEdg (G) (i)])$
121		f1oeq1	$⊢ j = (e \in dom iEdg (G) ⟼ {iEdg (H)}^{-1} ((x \in E ⟼ F [x]) (iEdg (G) (e)))) \to (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \leftrightarrow (e \in dom iEdg (G) ⟼ {iEdg (H)}^{-1} ((x \in E ⟼ F [x]) (iEdg (G) (e)))) : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H))$
122		fveq1	$⊢ j = (e \in dom iEdg (G) ⟼ {iEdg (H)}^{-1} ((x \in E ⟼ F [x]) (iEdg (G) (e)))) \to j (i) = (e \in dom iEdg (G) ⟼ {iEdg (H)}^{-1} ((x \in E ⟼ F [x]) (iEdg (G) (e)))) (i)$
123	122	fveqeq2d	$⊢ j = (e \in dom iEdg (G) ⟼ {iEdg (H)}^{-1} ((x \in E ⟼ F [x]) (iEdg (G) (e)))) \to (iEdg (H) (j (i)) = F [iEdg (G) (i)] \leftrightarrow iEdg (H) ((e \in dom iEdg (G) ⟼ {iEdg (H)}^{-1} ((x \in E ⟼ F [x]) (iEdg (G) (e)))) (i)) = F [iEdg (G) (i)])$
124	123	ralbidv	$⊢ j = (e \in dom iEdg (G) ⟼ {iEdg (H)}^{-1} ((x \in E ⟼ F [x]) (iEdg (G) (e)))) \to (\forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)] \leftrightarrow \forall i \in dom iEdg (G) iEdg (H) ((e \in dom iEdg (G) ⟼ {iEdg (H)}^{-1} ((x \in E ⟼ F [x]) (iEdg (G) (e)))) (i)) = F [iEdg (G) (i)])$
125	121 124	anbi12d	$⊢ j = (e \in dom iEdg (G) ⟼ {iEdg (H)}^{-1} ((x \in E ⟼ F [x]) (iEdg (G) (e)))) \to ((j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)]) \leftrightarrow ((e \in dom iEdg (G) ⟼ {iEdg (H)}^{-1} ((x \in E ⟼ F [x]) (iEdg (G) (e)))) : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) ((e \in dom iEdg (G) ⟼ {iEdg (H)}^{-1} ((x \in E ⟼ F [x]) (iEdg (G) (e)))) (i)) = F [iEdg (G) (i)]))$
126	118 120 125	spcedv	$⊢ (((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \land (x \in E ⟼ F [x]) : E \underset{1-1 onto}{⟶} D) \to \exists j (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])$
127	126	ex	$⊢ ((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \to ((x \in E ⟼ F [x]) : E \underset{1-1 onto}{⟶} D \to \exists j (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)]))$
128	114 127	impbid	$⊢ ((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \to (\exists j (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)]) \leftrightarrow (x \in E ⟼ F [x]) : E \underset{1-1 onto}{⟶} D)$
129		f1oeq1	$⊢ (x \in E ⟼ F [x]) = (e \in E ⟼ F [e]) \to ((x \in E ⟼ F [x]) : E \underset{1-1 onto}{⟶} D \leftrightarrow (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)$
130	110 129	mp1i	$⊢ ((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \to ((x \in E ⟼ F [x]) : E \underset{1-1 onto}{⟶} D \leftrightarrow (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)$
131	128 130	bitrd	$⊢ ((G \in USHGraph \land H \in USHGraph \land F \in X) \land F : V \underset{1-1 onto}{⟶} W) \to (\exists j (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)]) \leftrightarrow (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)$
132	131	pm5.32da	$⊢ (G \in USHGraph \land H \in USHGraph \land F \in X) \to ((F : V \underset{1-1 onto}{⟶} W \land \exists j (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \leftrightarrow (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D))$
133	7 132	bitrd	$⊢ (G \in USHGraph \land H \in USHGraph \land F \in X) \to (F \in (G GraphIso H) \leftrightarrow (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D))$

Metamath Proof Explorer

Theorem isuspgrim0

Proof