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

Proof

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