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 >. } } ) |