Step |
Hyp |
Ref |
Expression |
1 |
|
1aryenef |
Could not format ( 1 -aryF X ) ~~ ( X ^m X ) : No typesetting found for |- ( 1 -aryF X ) ~~ ( X ^m X ) with typecode |- |
2 |
|
eqid |
Could not format ( EndoFMnd ` X ) = ( EndoFMnd ` X ) : No typesetting found for |- ( EndoFMnd ` X ) = ( EndoFMnd ` X ) with typecode |- |
3 |
|
eqid |
Could not format ( Base ` ( EndoFMnd ` X ) ) = ( Base ` ( EndoFMnd ` X ) ) : No typesetting found for |- ( Base ` ( EndoFMnd ` X ) ) = ( Base ` ( EndoFMnd ` X ) ) with typecode |- |
4 |
2 3
|
efmndbas |
Could not format ( Base ` ( EndoFMnd ` X ) ) = ( X ^m X ) : No typesetting found for |- ( Base ` ( EndoFMnd ` X ) ) = ( X ^m X ) with typecode |- |
5 |
1 4
|
breqtrri |
Could not format ( 1 -aryF X ) ~~ ( Base ` ( EndoFMnd ` X ) ) : No typesetting found for |- ( 1 -aryF X ) ~~ ( Base ` ( EndoFMnd ` X ) ) with typecode |- |