Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
Could not format ( EndoFMnd ` (/) ) = ( EndoFMnd ` (/) ) : No typesetting found for |- ( EndoFMnd ` (/) ) = ( EndoFMnd ` (/) ) with typecode |- |
2 |
|
eqid |
Could not format ( Base ` ( EndoFMnd ` (/) ) ) = ( Base ` ( EndoFMnd ` (/) ) ) : No typesetting found for |- ( Base ` ( EndoFMnd ` (/) ) ) = ( Base ` ( EndoFMnd ` (/) ) ) with typecode |- |
3 |
1 2
|
efmndbas |
Could not format ( Base ` ( EndoFMnd ` (/) ) ) = ( (/) ^m (/) ) : No typesetting found for |- ( Base ` ( EndoFMnd ` (/) ) ) = ( (/) ^m (/) ) with typecode |- |
4 |
|
0map0sn0 |
|
5 |
3 4
|
eqtri |
Could not format ( Base ` ( EndoFMnd ` (/) ) ) = { (/) } : No typesetting found for |- ( Base ` ( EndoFMnd ` (/) ) ) = { (/) } with typecode |- |