Theorem rimval

Description: The set of ring isomorphisms. (Contributed by Jeff Madsen, 16-Jun-2011) (Revised by AV, 24-Jul-2026)

	Ref	Expression
Hypotheses	rhmf1o.b	|- B = ( Base ` R )
	rhmf1o.c	|- C = ( Base ` S )
Assertion	rimval	|- ( R RingIso S ) = { f e. ( R RingHom S ) | f : B -1-1-onto-> C }

Proof

Step	Hyp	Ref	Expression
1		rhmf1o.b	|- B = ( Base ` R )
2		rhmf1o.c	|- C = ( Base ` S )
3	1 2	isrim	|- ( x e. ( R RingIso S ) <-> ( x e. ( R RingHom S ) /\ x : B -1-1-onto-> C ) )
4		f1oeq1	|- ( f = x -> ( f : B -1-1-onto-> C <-> x : B -1-1-onto-> C ) )
5	4	elrab	|- ( x e. { f e. ( R RingHom S ) | f : B -1-1-onto-> C } <-> ( x e. ( R RingHom S ) /\ x : B -1-1-onto-> C ) )
6	3 5	bitr4i	|- ( x e. ( R RingIso S ) <-> x e. { f e. ( R RingHom S ) | f : B -1-1-onto-> C } )
7	6	eqriv	|- ( R RingIso S ) = { f e. ( R RingHom S ) | f : B -1-1-onto-> C }