uhgrimedg

Description: An isomorphism between graphs preserves edges, i.e. there is an edge in one graph connecting vertices iff 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	uhgrimedg	$⊢ ((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H) \land K \subseteq Vtx (G)) \to (K \in E \leftrightarrow F [K] \in D)$

Proof

Step	Hyp	Ref	Expression
1		uhgrimedgi.e	$⊢ E = Edg (G)$
2		uhgrimedgi.d	$⊢ D = Edg (H)$
3		simp1	$⊢ ((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H) \land K \subseteq Vtx (G)) \to (G \in UHGraph \land H \in UHGraph)$
4		simp2	$⊢ ((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H) \land K \subseteq Vtx (G)) \to F \in (G GraphIso H)$
5	4	anim1i	$⊢ (((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H) \land K \subseteq Vtx (G)) \land K \in E) \to (F \in (G GraphIso H) \land K \in E)$
6	1 2	uhgrimedgi	$⊢ ((G \in UHGraph \land H \in UHGraph) \land (F \in (G GraphIso H) \land K \in E)) \to F [K] \in D$
7	3 5 6	syl2an2r	$⊢ (((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H) \land K \subseteq Vtx (G)) \land K \in E) \to F [K] \in D$
8		eqid	$⊢ Vtx (G) = Vtx (G)$
9		eqid	$⊢ Vtx (H) = Vtx (H)$
10	8 9	grimf1o	$⊢ F \in (G GraphIso H) \to F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)$
11		f1of1	$⊢ F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H) \to F : Vtx (G) \underset{1-1}{⟶} Vtx (H)$
12	10 11	syl	$⊢ F \in (G GraphIso H) \to F : Vtx (G) \underset{1-1}{⟶} Vtx (H)$
13	12	3ad2ant2	$⊢ ((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H) \land K \subseteq Vtx (G)) \to F : Vtx (G) \underset{1-1}{⟶} Vtx (H)$
14		simp3	$⊢ ((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H) \land K \subseteq Vtx (G)) \to K \subseteq Vtx (G)$
15	13 14	jca	$⊢ ((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H) \land K \subseteq Vtx (G)) \to (F : Vtx (G) \underset{1-1}{⟶} Vtx (H) \land K \subseteq Vtx (G))$
16	15	adantr	$⊢ (((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H) \land K \subseteq Vtx (G)) \land F [K] \in D) \to (F : Vtx (G) \underset{1-1}{⟶} Vtx (H) \land K \subseteq Vtx (G))$
17		f1imacnv	$⊢ (F : Vtx (G) \underset{1-1}{⟶} Vtx (H) \land K \subseteq Vtx (G)) \to F^{-1} [F [K]] = K$
18	16 17	syl	$⊢ (((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H) \land K \subseteq Vtx (G)) \land F [K] \in D) \to F^{-1} [F [K]] = K$
19		pm3.22	$⊢ (G \in UHGraph \land H \in UHGraph) \to (H \in UHGraph \land G \in UHGraph)$
20	19	3ad2ant1	$⊢ ((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H) \land K \subseteq Vtx (G)) \to (H \in UHGraph \land G \in UHGraph)$
21		simpl	$⊢ (G \in UHGraph \land H \in UHGraph) \to G \in UHGraph$
22	21	anim1i	$⊢ ((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H)) \to (G \in UHGraph \land F \in (G GraphIso H))$
23	22	3adant3	$⊢ ((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H) \land K \subseteq Vtx (G)) \to (G \in UHGraph \land F \in (G GraphIso H))$
24		grimcnv	$⊢ G \in UHGraph \to (F \in (G GraphIso H) \to F^{-1} \in (H GraphIso G))$
25	24	imp	$⊢ (G \in UHGraph \land F \in (G GraphIso H)) \to F^{-1} \in (H GraphIso G)$
26	23 25	syl	$⊢ ((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H) \land K \subseteq Vtx (G)) \to F^{-1} \in (H GraphIso G)$
27	26	anim1i	$⊢ (((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H) \land K \subseteq Vtx (G)) \land F [K] \in D) \to (F^{-1} \in (H GraphIso G) \land F [K] \in D)$
28	2 1	uhgrimedgi	$⊢ ((H \in UHGraph \land G \in UHGraph) \land (F^{-1} \in (H GraphIso G) \land F [K] \in D)) \to F^{-1} [F [K]] \in E$
29	20 27 28	syl2an2r	$⊢ (((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H) \land K \subseteq Vtx (G)) \land F [K] \in D) \to F^{-1} [F [K]] \in E$
30	18 29	eqeltrrd	$⊢ (((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H) \land K \subseteq Vtx (G)) \land F [K] \in D) \to K \in E$
31	7 30	impbida	$⊢ ((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H) \land K \subseteq Vtx (G)) \to (K \in E \leftrightarrow F [K] \in D)$

Metamath Proof Explorer

Theorem uhgrimedg

Proof