This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gricref

Description: Graph isomorphism is reflexive for hypergraphs. (Contributed by AV, 11-Nov-2022) (Revised by AV, 29-Apr-2025)

		Ref	Expression
	Assertion	gricref	$⊢ G \in UHGraph \to G ≃_{𝑔𝑟} G$

Step	Hyp	Ref	Expression
1		grimid	$⊢ G \in UHGraph \to {I ↾}_{Vtx (G)} \in (G GraphIso G)$
2		brgrici	$⊢ {I ↾}_{Vtx (G)} \in (G GraphIso G) \to G ≃_{𝑔𝑟} G$
3	1 2	syl	$⊢ G \in UHGraph \to G ≃_{𝑔𝑟} G$