Metamath Proof Explorer

Theorem uhgrimgrlim

Description: An isomorphism of hypergraphs is a local isomorphism between the two graphs. (Contributed by AV, 2-Jun-2025)

		Ref	Expression
	Assertion	uhgrimgrlim	$⊢ (G \in UHGraph \land H \in UHGraph \land F \in (G GraphIso H)) \to F \in (G GraphLocIso H)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ Vtx (G) = Vtx (G)$
2		eqid	$⊢ Vtx (H) = Vtx (H)$
3	1 2	grimf1o	$⊢ F \in (G GraphIso H) \to F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)$
4	3	3ad2ant3	$⊢ (G \in UHGraph \land H \in UHGraph \land F \in (G GraphIso H)) \to F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)$
5		simpl1	$⊢ ((G \in UHGraph \land H \in UHGraph \land F \in (G GraphIso H)) \land v \in Vtx (G)) \to G \in UHGraph$
6		simpl3	$⊢ ((G \in UHGraph \land H \in UHGraph \land F \in (G GraphIso H)) \land v \in Vtx (G)) \to F \in (G GraphIso H)$
7	1	clnbgrssvtx	$⊢ G ClNeighbVtx v \subseteq Vtx (G)$
8	7	a1i	$⊢ ((G \in UHGraph \land H \in UHGraph \land F \in (G GraphIso H)) \land v \in Vtx (G)) \to G ClNeighbVtx v \subseteq Vtx (G)$
9	1	uhgrimisgrgric	$⊢ (G \in UHGraph \land F \in (G GraphIso H) \land G ClNeighbVtx v \subseteq Vtx (G)) \to (G ISubGr (G ClNeighbVtx v)) ≃_{𝑔𝑟} (H ISubGr F [G ClNeighbVtx v])$
10	5 6 8 9	syl3anc	$⊢ ((G \in UHGraph \land H \in UHGraph \land F \in (G GraphIso H)) \land v \in Vtx (G)) \to (G ISubGr (G ClNeighbVtx v)) ≃_{𝑔𝑟} (H ISubGr F [G ClNeighbVtx v])$
11		df-3an	$⊢ (G \in UHGraph \land H \in UHGraph \land F \in (G GraphIso H)) \leftrightarrow ((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H))$
12	1	clnbgrgrim	$⊢ (((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H)) \land v \in Vtx (G)) \to H ClNeighbVtx F (v) = F [G ClNeighbVtx v]$
13	11 12	sylanb	$⊢ ((G \in UHGraph \land H \in UHGraph \land F \in (G GraphIso H)) \land v \in Vtx (G)) \to H ClNeighbVtx F (v) = F [G ClNeighbVtx v]$
14	13	oveq2d	$⊢ ((G \in UHGraph \land H \in UHGraph \land F \in (G GraphIso H)) \land v \in Vtx (G)) \to H ISubGr (H ClNeighbVtx F (v)) = H ISubGr F [G ClNeighbVtx v]$
15	10 14	breqtrrd	$⊢ ((G \in UHGraph \land H \in UHGraph \land F \in (G GraphIso H)) \land v \in Vtx (G)) \to (G ISubGr (G ClNeighbVtx v)) ≃_{𝑔𝑟} (H ISubGr (H ClNeighbVtx F (v)))$
16	15	ralrimiva	$⊢ (G \in UHGraph \land H \in UHGraph \land F \in (G GraphIso H)) \to \forall v \in Vtx (G) (G ISubGr (G ClNeighbVtx v)) ≃_{𝑔𝑟} (H ISubGr (H ClNeighbVtx F (v)))$
17	1 2	isgrlim	$⊢ (G \in UHGraph \land H \in UHGraph \land F \in (G GraphIso H)) \to (F \in (G GraphLocIso H) \leftrightarrow (F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H) \land \forall v \in Vtx (G) (G ISubGr (G ClNeighbVtx v)) ≃_{𝑔𝑟} (H ISubGr (H ClNeighbVtx F (v)))))$
18	4 16 17	mpbir2and	$⊢ (G \in UHGraph \land H \in UHGraph \land F \in (G GraphIso H)) \to F \in (G GraphLocIso H)$