Step |
Hyp |
Ref |
Expression |
0 |
|
crngoiso |
Could not format RingOpsIso : No typesetting found for class RingOpsIso with typecode class |
1 |
|
vr |
|
2 |
|
crngo |
|
3 |
|
vs |
|
4 |
|
vf |
|
5 |
1
|
cv |
|
6 |
|
crngohom |
Could not format RingOpsHom : No typesetting found for class RingOpsHom with typecode class |
7 |
3
|
cv |
|
8 |
5 7 6
|
co |
Could not format ( r RingOpsHom s ) : No typesetting found for class ( r RingOpsHom s ) with typecode class |
9 |
4
|
cv |
|
10 |
|
c1st |
|
11 |
5 10
|
cfv |
|
12 |
11
|
crn |
|
13 |
7 10
|
cfv |
|
14 |
13
|
crn |
|
15 |
12 14 9
|
wf1o |
|
16 |
15 4 8
|
crab |
Could not format { f e. ( r RingOpsHom s ) | f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) } : No typesetting found for class { f e. ( r RingOpsHom s ) | f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) } with typecode class |
17 |
1 3 2 2 16
|
cmpo |
Could not format ( 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 class ( r e. RingOps , s e. RingOps |-> { f e. ( r RingOpsHom s ) | f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) } ) with typecode class |
18 |
0 17
|
wceq |
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 wff RingOpsIso = ( r e. RingOps , s e. RingOps |-> { f e. ( r RingOpsHom s ) | f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) } ) with typecode wff |