Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
|
2 |
|
eqid |
|
3 |
|
eqid |
|
4 |
|
eqid |
|
5 |
1 2 3 4
|
isrngoiso |
Could not format ( ( R e. RingOps /\ S e. RingOps ) -> ( F e. ( R RingOpsIso S ) <-> ( F e. ( R RingOpsHom S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) ) ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps ) -> ( F e. ( R RingOpsIso S ) <-> ( F e. ( R RingOpsHom S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) ) ) with typecode |- |
6 |
5
|
simprbda |
Could not format ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsIso S ) ) -> F e. ( R RingOpsHom S ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsIso S ) ) -> F e. ( R RingOpsHom S ) ) with typecode |- |
7 |
6
|
3impa |
Could not format ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsIso S ) ) -> F e. ( R RingOpsHom S ) ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsIso S ) ) -> F e. ( R RingOpsHom S ) ) with typecode |- |