Theorem ricrel

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

	Ref	Expression
Assertion	ricrel	|- Rel ~=r

Proof

Step	Hyp	Ref	Expression
1		df-ric	|- ~=r = ( `' RingIso " ( _V \ 1o ) )
2		cnvimass	|- ( `' RingIso " ( _V \ 1o ) ) C_ dom RingIso
3		rimfn	|- RingIso Fn ( _V X. _V )
4	3	fndmi	|- dom RingIso = ( _V X. _V )
5	2 4	sseqtri	|- ( `' RingIso " ( _V \ 1o ) ) C_ ( _V X. _V )
6	1 5	eqsstri	|- ~=r C_ ( _V X. _V )
7		relxp	|- Rel ( _V X. _V )
8		relss	|- ( ~=r C_ ( _V X. _V ) -> ( Rel ( _V X. _V ) -> Rel ~=r ) )
9	6 7 8	mp2	|- Rel ~=r