Step |
Hyp |
Ref |
Expression |
1 |
|
ssidd |
|- ( X e. _V -> { { <. X , X >. } } C_ { { <. X , X >. } } ) |
2 |
|
eqid |
|- ( EndoFMnd ` { X } ) = ( EndoFMnd ` { X } ) |
3 |
|
eqid |
|- ( Base ` ( EndoFMnd ` { X } ) ) = ( Base ` ( EndoFMnd ` { X } ) ) |
4 |
|
eqid |
|- { X } = { X } |
5 |
2 3 4
|
efmnd1bas |
|- ( X e. _V -> ( Base ` ( EndoFMnd ` { X } ) ) = { { <. X , X >. } } ) |
6 |
|
eqid |
|- ( SymGrp ` { X } ) = ( SymGrp ` { X } ) |
7 |
|
eqid |
|- ( Base ` ( SymGrp ` { X } ) ) = ( Base ` ( SymGrp ` { X } ) ) |
8 |
6 7 4
|
symg1bas |
|- ( X e. _V -> ( Base ` ( SymGrp ` { X } ) ) = { { <. X , X >. } } ) |
9 |
1 5 8
|
3sstr4d |
|- ( X e. _V -> ( Base ` ( EndoFMnd ` { X } ) ) C_ ( Base ` ( SymGrp ` { X } ) ) ) |
10 |
|
fvexd |
|- ( X e. _V -> ( EndoFMnd ` { X } ) e. _V ) |
11 |
|
fvexd |
|- ( X e. _V -> ( Base ` ( SymGrp ` { X } ) ) e. _V ) |
12 |
6 7 2
|
symgressbas |
|- ( SymGrp ` { X } ) = ( ( EndoFMnd ` { X } ) |`s ( Base ` ( SymGrp ` { X } ) ) ) |
13 |
12 3
|
ressid2 |
|- ( ( ( Base ` ( EndoFMnd ` { X } ) ) C_ ( Base ` ( SymGrp ` { X } ) ) /\ ( EndoFMnd ` { X } ) e. _V /\ ( Base ` ( SymGrp ` { X } ) ) e. _V ) -> ( SymGrp ` { X } ) = ( EndoFMnd ` { X } ) ) |
14 |
9 10 11 13
|
syl3anc |
|- ( X e. _V -> ( SymGrp ` { X } ) = ( EndoFMnd ` { X } ) ) |
15 |
14
|
eqcomd |
|- ( X e. _V -> ( EndoFMnd ` { X } ) = ( SymGrp ` { X } ) ) |
16 |
|
fveq2 |
|- ( A = { X } -> ( EndoFMnd ` A ) = ( EndoFMnd ` { X } ) ) |
17 |
|
fveq2 |
|- ( A = { X } -> ( SymGrp ` A ) = ( SymGrp ` { X } ) ) |
18 |
16 17
|
eqeq12d |
|- ( A = { X } -> ( ( EndoFMnd ` A ) = ( SymGrp ` A ) <-> ( EndoFMnd ` { X } ) = ( SymGrp ` { X } ) ) ) |
19 |
15 18
|
syl5ibrcom |
|- ( X e. _V -> ( A = { X } -> ( EndoFMnd ` A ) = ( SymGrp ` A ) ) ) |
20 |
|
snprc |
|- ( -. X e. _V <-> { X } = (/) ) |
21 |
20
|
biimpi |
|- ( -. X e. _V -> { X } = (/) ) |
22 |
21
|
eqeq2d |
|- ( -. X e. _V -> ( A = { X } <-> A = (/) ) ) |
23 |
|
0symgefmndeq |
|- ( EndoFMnd ` (/) ) = ( SymGrp ` (/) ) |
24 |
|
fveq2 |
|- ( A = (/) -> ( EndoFMnd ` A ) = ( EndoFMnd ` (/) ) ) |
25 |
|
fveq2 |
|- ( A = (/) -> ( SymGrp ` A ) = ( SymGrp ` (/) ) ) |
26 |
23 24 25
|
3eqtr4a |
|- ( A = (/) -> ( EndoFMnd ` A ) = ( SymGrp ` A ) ) |
27 |
22 26
|
syl6bi |
|- ( -. X e. _V -> ( A = { X } -> ( EndoFMnd ` A ) = ( SymGrp ` A ) ) ) |
28 |
19 27
|
pm2.61i |
|- ( A = { X } -> ( EndoFMnd ` A ) = ( SymGrp ` A ) ) |