Theorem gricer

Description: Isomorphism is an equivalence relation on hypergraphs. (Contributed by AV, 3-May-2025) (Proof shortened by AV, 11-Jul-2025)

	Ref	Expression
Assertion	gricer	⊢ ( ≃𝑔𝑟 ∩ ( UHGraph × UHGraph ) ) Er UHGraph

Proof

Step	Hyp	Ref	Expression
1		gricref	⊢ ( 𝑔 ∈ UHGraph → 𝑔 ≃𝑔𝑟 𝑔 )
2		gricsym	⊢ ( 𝑔 ∈ UHGraph → ( 𝑔 ≃𝑔𝑟 ℎ → ℎ ≃𝑔𝑟 𝑔 ) )
3		grictr	⊢ ( ( 𝑔 ≃𝑔𝑟 ℎ ∧ ℎ ≃𝑔𝑟 𝑘 ) → 𝑔 ≃𝑔𝑟 𝑘 )
4	3	a1i	⊢ ( 𝑔 ∈ UHGraph → ( ( 𝑔 ≃𝑔𝑟 ℎ ∧ ℎ ≃𝑔𝑟 𝑘 ) → 𝑔 ≃𝑔𝑟 𝑘 ) )
5	1 2 4	brinxper	⊢ ( ≃𝑔𝑟 ∩ ( UHGraph × UHGraph ) ) Er UHGraph