Theorem ricrel

Description: The domain of the ring isomorphism relation is a relation. (Contributed by AV, 24-Jul-2026)

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

Proof

Step	Hyp	Ref	Expression
1		df-ric	$$⊢{\simeq }_{𝑟}={\mathrm{RingIso}}^{-1}\left[\mathrm{V}\setminus 1_{𝑜}\right]$$
2		cnvimass	$$⊢{\mathrm{RingIso}}^{-1}\left[\mathrm{V}\setminus 1_{𝑜}\right]\subseteq \mathrm{dom}\mathrm{RingIso}$$
3		rimfn	$$⊢\mathrm{RingIso}Fn\left(\mathrm{V}\times \mathrm{V}\right)$$
4	3	fndmi	$$⊢\mathrm{dom}\mathrm{RingIso}=\mathrm{V}\times \mathrm{V}$$
5	2 4	sseqtri	$$⊢{\mathrm{RingIso}}^{-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 }_{𝑟}$$