Theorem brric

Description: The relation "is isomorphic to" for (unital) rings. (Contributed by AV, 24-Dec-2019)

	Ref	Expression
Assertion	brric	|- ( R ~=r S <-> ( R RingIso S ) =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		df-ric	|- ~=r = ( `' RingIso " ( _V \ 1o ) )
2		ovex	|- ( r RingHom s ) e. _V
3		rabexg	|- ( ( r RingHom s ) e. _V -> { h e. ( r RingHom s ) | `' h e. ( s RingHom r ) } e. _V )
4	2 3	mp1i	|- ( ( r e. _V /\ s e. _V ) -> { h e. ( r RingHom s ) | `' h e. ( s RingHom r ) } e. _V )
5	4	rgen2	|- A. r e. _V A. s e. _V { h e. ( r RingHom s ) | `' h e. ( s RingHom r ) } e. _V
6		df-rngiso	|- RingIso = ( r e. _V , s e. _V |-> { h e. ( r RingHom s ) | `' h e. ( s RingHom r ) } )
7	6	fnmpo	|- ( A. r e. _V A. s e. _V { h e. ( r RingHom s ) | `' h e. ( s RingHom r ) } e. _V -> RingIso Fn ( _V X. _V ) )
8	5 7	ax-mp	|- RingIso Fn ( _V X. _V )
9	1 8	brwitnlem	|- ( R ~=r S <-> ( R RingIso S ) =/= (/) )