uhgrimprop

Description: An isomorphism between hypergraphs is a bijection between their vertices that preserves adjacency for simple edges, i.e. there is a simple edge in one graph connecting one or two vertices iff there is a simple edge in the other graph connecting the vertices which are the images of the vertices. (Contributed by AV, 27-Apr-2025) (Revised by AV, 25-Oct-2025)

	Ref	Expression
Hypotheses	uhgrimedgi.e	$⊢ E = Edg (G)$
	uhgrimedgi.d	$⊢ D = Edg (H)$
	uhgrimprop.v	$⊢ V = Vtx (G)$
	uhgrimprop.w	$⊢ W = Vtx (H)$
Assertion	uhgrimprop	$⊢ (G \in UHGraph \land H \in UHGraph \land F \in (G GraphIso H)) \to (F : V \underset{1-1 onto}{⟶} W \land \forall x \in V \forall y \in V (\{x, y\} \in E \leftrightarrow \{F (x), F (y)\} \in D))$

Proof

Step	Hyp	Ref	Expression
1		uhgrimedgi.e	$⊢ E = Edg (G)$
2		uhgrimedgi.d	$⊢ D = Edg (H)$
3		uhgrimprop.v	$⊢ V = Vtx (G)$
4		uhgrimprop.w	$⊢ W = Vtx (H)$
5	3 4	grimf1o	$⊢ F \in (G GraphIso H) \to F : V \underset{1-1 onto}{⟶} W$
6	5	3ad2ant3	$⊢ (G \in UHGraph \land H \in UHGraph \land F \in (G GraphIso H)) \to F : V \underset{1-1 onto}{⟶} W$
7		3simpa	$⊢ (G \in UHGraph \land H \in UHGraph \land F \in (G GraphIso H)) \to (G \in UHGraph \land H \in UHGraph)$
8		simp3	$⊢ (G \in UHGraph \land H \in UHGraph \land F \in (G GraphIso H)) \to F \in (G GraphIso H)$
9		prssi	$⊢ (x \in V \land y \in V) \to \{x, y\} \subseteq V$
10	9 3	sseqtrdi	$⊢ (x \in V \land y \in V) \to \{x, y\} \subseteq Vtx (G)$
11	1 2	uhgrimedg	$⊢ ((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H) \land \{x, y\} \subseteq Vtx (G)) \to (\{x, y\} \in E \leftrightarrow F [\{x, y\}] \in D)$
12	7 8 10 11	syl2an3an	$⊢ ((G \in UHGraph \land H \in UHGraph \land F \in (G GraphIso H)) \land (x \in V \land y \in V)) \to (\{x, y\} \in E \leftrightarrow F [\{x, y\}] \in D)$
13		f1ofn	$⊢ F : V \underset{1-1 onto}{⟶} W \to F Fn V$
14	5 13	syl	$⊢ F \in (G GraphIso H) \to F Fn V$
15	14	3ad2ant3	$⊢ (G \in UHGraph \land H \in UHGraph \land F \in (G GraphIso H)) \to F Fn V$
16	15	anim1i	$⊢ ((G \in UHGraph \land H \in UHGraph \land F \in (G GraphIso H)) \land (x \in V \land y \in V)) \to (F Fn V \land (x \in V \land y \in V))$
17		3anass	$⊢ (F Fn V \land x \in V \land y \in V) \leftrightarrow (F Fn V \land (x \in V \land y \in V))$
18	16 17	sylibr	$⊢ ((G \in UHGraph \land H \in UHGraph \land F \in (G GraphIso H)) \land (x \in V \land y \in V)) \to (F Fn V \land x \in V \land y \in V)$
19		fnimapr	$⊢ (F Fn V \land x \in V \land y \in V) \to F [\{x, y\}] = \{F (x), F (y)\}$
20	18 19	syl	$⊢ ((G \in UHGraph \land H \in UHGraph \land F \in (G GraphIso H)) \land (x \in V \land y \in V)) \to F [\{x, y\}] = \{F (x), F (y)\}$
21	20	eleq1d	$⊢ ((G \in UHGraph \land H \in UHGraph \land F \in (G GraphIso H)) \land (x \in V \land y \in V)) \to (F [\{x, y\}] \in D \leftrightarrow \{F (x), F (y)\} \in D)$
22	12 21	bitrd	$⊢ ((G \in UHGraph \land H \in UHGraph \land F \in (G GraphIso H)) \land (x \in V \land y \in V)) \to (\{x, y\} \in E \leftrightarrow \{F (x), F (y)\} \in D)$
23	22	ralrimivva	$⊢ (G \in UHGraph \land H \in UHGraph \land F \in (G GraphIso H)) \to \forall x \in V \forall y \in V (\{x, y\} \in E \leftrightarrow \{F (x), F (y)\} \in D)$
24	6 23	jca	$⊢ (G \in UHGraph \land H \in UHGraph \land F \in (G GraphIso H)) \to (F : V \underset{1-1 onto}{⟶} W \land \forall x \in V \forall y \in V (\{x, y\} \in E \leftrightarrow \{F (x), F (y)\} \in D))$

Metamath Proof Explorer

Theorem uhgrimprop

Proof