| Step |
Hyp |
Ref |
Expression |
| 1 |
|
efmnd1bas.1 |
|- G = ( EndoFMnd ` A ) |
| 2 |
|
efmnd1bas.2 |
|- B = ( Base ` G ) |
| 3 |
|
efmnd1bas.0 |
|- A = { I } |
| 4 |
3
|
fveq2i |
|- ( EndoFMnd ` A ) = ( EndoFMnd ` { I } ) |
| 5 |
1 4
|
eqtri |
|- G = ( EndoFMnd ` { I } ) |
| 6 |
5 2
|
efmndbas |
|- B = ( { I } ^m { I } ) |
| 7 |
|
fsng |
|- ( ( I e. V /\ I e. V ) -> ( p : { I } --> { I } <-> p = { <. I , I >. } ) ) |
| 8 |
7
|
anidms |
|- ( I e. V -> ( p : { I } --> { I } <-> p = { <. I , I >. } ) ) |
| 9 |
|
snex |
|- { I } e. _V |
| 10 |
9 9
|
elmap |
|- ( p e. ( { I } ^m { I } ) <-> p : { I } --> { I } ) |
| 11 |
|
velsn |
|- ( p e. { { <. I , I >. } } <-> p = { <. I , I >. } ) |
| 12 |
8 10 11
|
3bitr4g |
|- ( I e. V -> ( p e. ( { I } ^m { I } ) <-> p e. { { <. I , I >. } } ) ) |
| 13 |
12
|
eqrdv |
|- ( I e. V -> ( { I } ^m { I } ) = { { <. I , I >. } } ) |
| 14 |
6 13
|
eqtrid |
|- ( I e. V -> B = { { <. I , I >. } } ) |