uhgrimedgi

Description: An isomorphism between graphs preserves edges, i.e. if there is an edge in one graph connecting vertices then there is an edge in the other graph connecting the corresponding vertices. (Contributed by AV, 25-Oct-2025)

	Ref	Expression
Hypotheses	uhgrimedgi.e	$⊢ E = Edg (G)$
	uhgrimedgi.d	$⊢ D = Edg (H)$
Assertion	uhgrimedgi	$⊢ ((G \in UHGraph \land H \in UHGraph) \land (F \in (G GraphIso H) \land K \in E)) \to F [K] \in D$

Proof

Step	Hyp	Ref	Expression
1		uhgrimedgi.e	$⊢ E = Edg (G)$
2		uhgrimedgi.d	$⊢ D = Edg (H)$
3		eqid	$⊢ Vtx (G) = Vtx (G)$
4		eqid	$⊢ Vtx (H) = Vtx (H)$
5		eqid	$⊢ iEdg (G) = iEdg (G)$
6		eqid	$⊢ iEdg (H) = iEdg (H)$
7	3 4 5 6	grimprop	$⊢ F \in (G GraphIso H) \to (F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H) \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	1	eleq2i	$⊢ K \in E \leftrightarrow K \in Edg (G)$
9	5	uhgrfun	$⊢ G \in UHGraph \to Fun iEdg (G)$
10	5	edgiedgb	$⊢ Fun iEdg (G) \to (K \in Edg (G) \leftrightarrow \exists k \in dom iEdg (G) K = iEdg (G) (k))$
11	9 10	syl	$⊢ G \in UHGraph \to (K \in Edg (G) \leftrightarrow \exists k \in dom iEdg (G) K = iEdg (G) (k))$
12	8 11	bitrid	$⊢ G \in UHGraph \to (K \in E \leftrightarrow \exists k \in dom iEdg (G) K = iEdg (G) (k))$
13	12	adantr	$⊢ (G \in UHGraph \land H \in UHGraph) \to (K \in E \leftrightarrow \exists k \in dom iEdg (G) K = iEdg (G) (k))$
14		simplr	$⊢ (((G \in UHGraph \land H \in UHGraph) \land k \in dom iEdg (G)) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \to k \in dom iEdg (G)$
15		2fveq3	$⊢ i = k \to iEdg (H) (j (i)) = iEdg (H) (j (k))$
16		fveq2	$⊢ i = k \to iEdg (G) (i) = iEdg (G) (k)$
17	16	imaeq2d	$⊢ i = k \to F [iEdg (G) (i)] = F [iEdg (G) (k)]$
18	15 17	eqeq12d	$⊢ i = k \to (iEdg (H) (j (i)) = F [iEdg (G) (i)] \leftrightarrow iEdg (H) (j (k)) = F [iEdg (G) (k)])$
19	18	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)])$
20	14 19	syl	$⊢ (((G \in UHGraph \land H \in UHGraph) \land k \in dom iEdg (G)) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \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	6	uhgrfun	$⊢ H \in UHGraph \to Fun iEdg (H)$
22	21	ad3antlr	$⊢ (((G \in UHGraph \land H \in UHGraph) \land k \in dom iEdg (G)) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \to Fun iEdg (H)$
23		f1of	$⊢ j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \to j : dom iEdg (G) ⟶ dom iEdg (H)$
24	23	adantl	$⊢ ((((G \in UHGraph \land H \in UHGraph) \land k \in dom iEdg (G)) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \to j : dom iEdg (G) ⟶ dom iEdg (H)$
25	14	adantr	$⊢ ((((G \in UHGraph \land H \in UHGraph) \land k \in dom iEdg (G)) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \to k \in dom iEdg (G)$
26	24 25	ffvelcdmd	$⊢ ((((G \in UHGraph \land H \in UHGraph) \land k \in dom iEdg (G)) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \to j (k) \in dom iEdg (H)$
27	6	iedgedg	$⊢ (Fun iEdg (H) \land j (k) \in dom iEdg (H)) \to iEdg (H) (j (k)) \in Edg (H)$
28	22 26 27	syl2an2r	$⊢ ((((G \in UHGraph \land H \in UHGraph) \land k \in dom iEdg (G)) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \to iEdg (H) (j (k)) \in Edg (H)$
29	28 2	eleqtrrdi	$⊢ ((((G \in UHGraph \land H \in UHGraph) \land k \in dom iEdg (G)) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \to iEdg (H) (j (k)) \in D$
30		eleq1	$⊢ F [iEdg (G) (k)] = iEdg (H) (j (k)) \to (F [iEdg (G) (k)] \in D \leftrightarrow iEdg (H) (j (k)) \in D)$
31	30	eqcoms	$⊢ iEdg (H) (j (k)) = F [iEdg (G) (k)] \to (F [iEdg (G) (k)] \in D \leftrightarrow iEdg (H) (j (k)) \in D)$
32	29 31	syl5ibrcom	$⊢ ((((G \in UHGraph \land H \in UHGraph) \land k \in dom iEdg (G)) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \to (iEdg (H) (j (k)) = F [iEdg (G) (k)] \to F [iEdg (G) (k)] \in D)$
33	32	ex	$⊢ (((G \in UHGraph \land H \in UHGraph) \land k \in dom iEdg (G)) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \to (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \to (iEdg (H) (j (k)) = F [iEdg (G) (k)] \to F [iEdg (G) (k)] \in D))$
34	20 33	syl5d	$⊢ (((G \in UHGraph \land H \in UHGraph) \land k \in dom iEdg (G)) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \to (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 F [iEdg (G) (k)] \in D))$
35	34	impd	$⊢ (((G \in UHGraph \land H \in UHGraph) \land k \in dom iEdg (G)) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \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 F [iEdg (G) (k)] \in D)$
36	35	ex	$⊢ ((G \in UHGraph \land H \in UHGraph) \land k \in dom iEdg (G)) \to (F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H) \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 F [iEdg (G) (k)] \in D))$
37	36	adantr	$⊢ (((G \in UHGraph \land H \in UHGraph) \land k \in dom iEdg (G)) \land K = iEdg (G) (k)) \to (F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H) \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 F [iEdg (G) (k)] \in D))$
38	37	3imp	$⊢ ((((G \in UHGraph \land H \in UHGraph) \land k \in dom iEdg (G)) \land K = iEdg (G) (k)) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H) \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 F [iEdg (G) (k)] \in D$
39		imaeq2	$⊢ K = iEdg (G) (k) \to F [K] = F [iEdg (G) (k)]$
40	39	eleq1d	$⊢ K = iEdg (G) (k) \to (F [K] \in D \leftrightarrow F [iEdg (G) (k)] \in D)$
41	40	adantl	$⊢ (((G \in UHGraph \land H \in UHGraph) \land k \in dom iEdg (G)) \land K = iEdg (G) (k)) \to (F [K] \in D \leftrightarrow F [iEdg (G) (k)] \in D)$
42	41	3ad2ant1	$⊢ ((((G \in UHGraph \land H \in UHGraph) \land k \in dom iEdg (G)) \land K = iEdg (G) (k)) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H) \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 (F [K] \in D \leftrightarrow F [iEdg (G) (k)] \in D)$
43	38 42	mpbird	$⊢ ((((G \in UHGraph \land H \in UHGraph) \land k \in dom iEdg (G)) \land K = iEdg (G) (k)) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H) \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 F [K] \in D$
44	43	3exp	$⊢ (((G \in UHGraph \land H \in UHGraph) \land k \in dom iEdg (G)) \land K = iEdg (G) (k)) \to (F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H) \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 F [K] \in D))$
45	44	ex	$⊢ ((G \in UHGraph \land H \in UHGraph) \land k \in dom iEdg (G)) \to (K = iEdg (G) (k) \to (F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H) \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 F [K] \in D)))$
46	45	rexlimdva	$⊢ (G \in UHGraph \land H \in UHGraph) \to (\exists k \in dom iEdg (G) K = iEdg (G) (k) \to (F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H) \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 F [K] \in D)))$
47	13 46	sylbid	$⊢ (G \in UHGraph \land H \in UHGraph) \to (K \in E \to (F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H) \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 F [K] \in D)))$
48	47	imp	$⊢ ((G \in UHGraph \land H \in UHGraph) \land K \in E) \to (F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H) \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 F [K] \in D))$
49	48	imp	$⊢ (((G \in UHGraph \land H \in UHGraph) \land K \in E) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \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 F [K] \in D)$
50	49	exlimdv	$⊢ (((G \in UHGraph \land H \in UHGraph) \land K \in E) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \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 F [K] \in D)$
51	50	expimpd	$⊢ ((G \in UHGraph \land H \in UHGraph) \land K \in E) \to ((F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H) \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)])) \to F [K] \in D)$
52	7 51	syl5	$⊢ ((G \in UHGraph \land H \in UHGraph) \land K \in E) \to (F \in (G GraphIso H) \to F [K] \in D)$
53	52	ex	$⊢ (G \in UHGraph \land H \in UHGraph) \to (K \in E \to (F \in (G GraphIso H) \to F [K] \in D))$
54	53	impcomd	$⊢ (G \in UHGraph \land H \in UHGraph) \to ((F \in (G GraphIso H) \land K \in E) \to F [K] \in D)$
55	54	imp	$⊢ ((G \in UHGraph \land H \in UHGraph) \land (F \in (G GraphIso H) \land K \in E)) \to F [K] \in D$

Metamath Proof Explorer

Theorem uhgrimedgi

Proof