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	⊢ ( 𝐺 ∈ UHGraph → 𝐺 ≃𝑔𝑟 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		grimid	⊢ ( 𝐺 ∈ UHGraph → ( I ↾ ( Vtx ‘ 𝐺 ) ) ∈ ( 𝐺 GraphIso 𝐺 ) )
2		brgrici	⊢ ( ( I ↾ ( Vtx ‘ 𝐺 ) ) ∈ ( 𝐺 GraphIso 𝐺 ) → 𝐺 ≃𝑔𝑟 𝐺 )
3	1 2	syl	⊢ ( 𝐺 ∈ UHGraph → 𝐺 ≃𝑔𝑟 𝐺 )