Theorem gricrel

Description: The "is isomorphic to" relation for graphs is a relation. (Contributed by AV, 11-Nov-2022) (Revised by AV, 5-May-2025)

	Ref	Expression
Assertion	gricrel	$$⊢\mathrm{Rel}{\simeq }_{𝑔𝑟}$$

Proof

Step	Hyp	Ref	Expression
1		df-gric	$$⊢{\simeq }_{𝑔𝑟}={\mathrm{GraphIso}}^{-1}\left[\mathrm{V}\setminus 1_{𝑜}\right]$$
2		cnvimass	$$⊢{\mathrm{GraphIso}}^{-1}\left[\mathrm{V}\setminus 1_{𝑜}\right]\subseteq \mathrm{dom}\mathrm{GraphIso}$$
3		grimfn	$$⊢\mathrm{GraphIso}Fn\left(\mathrm{V}\times \mathrm{V}\right)$$
4	3	fndmi	$$⊢\mathrm{dom}\mathrm{GraphIso}=\mathrm{V}\times \mathrm{V}$$
5	2 4	sseqtri	$$⊢{\mathrm{GraphIso}}^{-1}\left[\mathrm{V}\setminus 1_{𝑜}\right]\subseteq \mathrm{V}\times \mathrm{V}$$
6	1 5	eqsstri	$$⊢{\simeq }_{𝑔𝑟}\subseteq \mathrm{V}\times \mathrm{V}$$
7		relxp	$$⊢\mathrm{Rel}\left(\mathrm{V}\times \mathrm{V}\right)$$
8		relss	$$⊢{\simeq }_{𝑔𝑟}\subseteq \mathrm{V}\times \mathrm{V}\to \left(\mathrm{Rel}\left(\mathrm{V}\times \mathrm{V}\right)\to \mathrm{Rel}{\simeq }_{𝑔𝑟}\right)$$
9	6 7 8	mp2	$$⊢\mathrm{Rel}{\simeq }_{𝑔𝑟}$$