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 \mathrm{UHGraph}\to G{\simeq }_{𝑔𝑟}G$$

Proof

Step	Hyp	Ref	Expression
1		grimid	$$⊢G\in \mathrm{UHGraph}\to {\mathrm{I}\upharpoonright }_{\mathrm{Vtx}\left(G\right)}\in \left(G\mathrm{GraphIso}G\right)$$
2		brgrici	$$⊢{\mathrm{I}\upharpoonright }_{\mathrm{Vtx}\left(G\right)}\in \left(G\mathrm{GraphIso}G\right)\to G{\simeq }_{𝑔𝑟}G$$
3	1 2	syl	$$⊢G\in \mathrm{UHGraph}\to G{\simeq }_{𝑔𝑟}G$$