Theorem rngoisoval

Description: The set of ring isomorphisms. (Contributed by Jeff Madsen, 16-Jun-2011)

	Ref	Expression
Hypotheses	rngisoval.1	$$⊢G=1^{st}\left(R\right)$$
	rngisoval.2	$$⊢X=\mathrm{ran}G$$
	rngisoval.3	$$⊢J=1^{st}\left(S\right)$$
	rngisoval.4	$$⊢Y=\mathrm{ran}J$$
Assertion	rngoisoval	Could not format assertion : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps ) -> ( R RingOpsIso S ) = { f e. ( R RingOpsHom S ) | f : X -1-1-onto-> Y } ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		rngisoval.1	$$⊢G=1^{st}\left(R\right)$$
2		rngisoval.2	$$⊢X=\mathrm{ran}G$$
3		rngisoval.3	$$⊢J=1^{st}\left(S\right)$$
4		rngisoval.4	$$⊢Y=\mathrm{ran}J$$
5		oveq12	Could not format ( ( r = R /\ s = S ) -> ( r RingOpsHom s ) = ( R RingOpsHom S ) ) : No typesetting found for |- ( ( r = R /\ s = S ) -> ( r RingOpsHom s ) = ( R RingOpsHom S ) ) with typecode |-
6		fveq2	$$⊢r=R\to 1^{st}\left(r\right)=1^{st}\left(R\right)$$
7	6 1	eqtr4di	$$⊢r=R\to 1^{st}\left(r\right)=G$$
8	7	rneqd	$$⊢r=R\to \mathrm{ran}{1}^{st}\left(r\right)=\mathrm{ran}G$$
9	8 2	eqtr4di	$$⊢r=R\to \mathrm{ran}{1}^{st}\left(r\right)=X$$
10	9	f1oeq2d	$$⊢r=R\to \left(f:\mathrm{ran}{1}^{st}\left(r\right)\underset{1-1\; onto}{⟶}\mathrm{ran}{1}^{st}\left(s\right)\leftrightarrow f:X\underset{1-1\; onto}{⟶}\mathrm{ran}{1}^{st}\left(s\right)\right)$$
11		fveq2	$$⊢s=S\to 1^{st}\left(s\right)=1^{st}\left(S\right)$$
12	11 3	eqtr4di	$$⊢s=S\to 1^{st}\left(s\right)=J$$
13	12	rneqd	$$⊢s=S\to \mathrm{ran}{1}^{st}\left(s\right)=\mathrm{ran}J$$
14	13 4	eqtr4di	$$⊢s=S\to \mathrm{ran}{1}^{st}\left(s\right)=Y$$
15	14	f1oeq3d	$$⊢s=S\to \left(f:X\underset{1-1\; onto}{⟶}\mathrm{ran}{1}^{st}\left(s\right)\leftrightarrow f:X\underset{1-1\; onto}{⟶}Y\right)$$
16	10 15	sylan9bb	$$⊢\left(r=R\wedge s=S\right)\to \left(f:\mathrm{ran}{1}^{st}\left(r\right)\underset{1-1\; onto}{⟶}\mathrm{ran}{1}^{st}\left(s\right)\leftrightarrow f:X\underset{1-1\; onto}{⟶}Y\right)$$
17	5 16	rabeqbidv	Could not format ( ( r = R /\ s = S ) -> { f e. ( r RingOpsHom s ) | f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) } = { f e. ( R RingOpsHom S ) | f : X -1-1-onto-> Y } ) : No typesetting found for |- ( ( r = R /\ s = S ) -> { f e. ( r RingOpsHom s ) | f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) } = { f e. ( R RingOpsHom S ) | f : X -1-1-onto-> Y } ) with typecode |-
18		df-rngoiso	Could not format RingOpsIso = ( r e. RingOps , s e. RingOps |-> { f e. ( r RingOpsHom s ) | f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) } ) : No typesetting found for |- RingOpsIso = ( r e. RingOps , s e. RingOps |-> { f e. ( r RingOpsHom s ) | f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) } ) with typecode |-
19		ovex	Could not format ( R RingOpsHom S ) e. _V : No typesetting found for |- ( R RingOpsHom S ) e. _V with typecode |-
20	19	rabex	Could not format { f e. ( R RingOpsHom S ) | f : X -1-1-onto-> Y } e. _V : No typesetting found for |- { f e. ( R RingOpsHom S ) | f : X -1-1-onto-> Y } e. _V with typecode |-
21	17 18 20	ovmpoa	Could not format ( ( R e. RingOps /\ S e. RingOps ) -> ( R RingOpsIso S ) = { f e. ( R RingOpsHom S ) | f : X -1-1-onto-> Y } ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps ) -> ( R RingOpsIso S ) = { f e. ( R RingOpsHom S ) | f : X -1-1-onto-> Y } ) with typecode |-