Step |
Hyp |
Ref |
Expression |
1 |
|
rngisoval.1 |
|
2 |
|
rngisoval.2 |
|
3 |
|
rngisoval.3 |
|
4 |
|
rngisoval.4 |
|
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 : X -1-1-onto-> Y ) ) ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps ) -> ( F e. ( R RingOpsIso S ) <-> ( F e. ( R RingOpsHom S ) /\ F : X -1-1-onto-> Y ) ) ) with typecode |- |
6 |
5
|
simplbda |
Could not format ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsIso S ) ) -> F : X -1-1-onto-> Y ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsIso S ) ) -> F : X -1-1-onto-> Y ) with typecode |- |
7 |
6
|
3impa |
Could not format ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsIso S ) ) -> F : X -1-1-onto-> Y ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsIso S ) ) -> F : X -1-1-onto-> Y ) with typecode |- |