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

Metamath Proof Explorer

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	$⊢ (≃_{𝑔𝑟} \cap (UHGraph \times UHGraph)) Er UHGraph$

Step	Hyp	Ref	Expression
1		gricref	$⊢ g \in UHGraph \to g ≃_{𝑔𝑟} g$
2		gricsym	$⊢ g \in UHGraph \to (g ≃_{𝑔𝑟} h \to h ≃_{𝑔𝑟} g)$
3		grictr	$⊢ (g ≃_{𝑔𝑟} h \land h ≃_{𝑔𝑟} k) \to g ≃_{𝑔𝑟} k$
4	3	a1i	$⊢ g \in UHGraph \to ((g ≃_{𝑔𝑟} h \land h ≃_{𝑔𝑟} k) \to g ≃_{𝑔𝑟} k)$
5	1 2 4	brinxper	$⊢ (≃_{𝑔𝑟} \cap (UHGraph \times UHGraph)) Er UHGraph$