Step |
Hyp |
Ref |
Expression |
1 |
|
sursubmefmnd.m |
|- M = ( EndoFMnd ` A ) |
2 |
|
vex |
|- x e. _V |
3 |
|
foeq1 |
|- ( h = x -> ( h : A -onto-> A <-> x : A -onto-> A ) ) |
4 |
2 3
|
elab |
|- ( x e. { h | h : A -onto-> A } <-> x : A -onto-> A ) |
5 |
|
fof |
|- ( x : A -onto-> A -> x : A --> A ) |
6 |
|
eqid |
|- ( Base ` M ) = ( Base ` M ) |
7 |
1 6
|
elefmndbas |
|- ( A e. V -> ( x e. ( Base ` M ) <-> x : A --> A ) ) |
8 |
5 7
|
syl5ibr |
|- ( A e. V -> ( x : A -onto-> A -> x e. ( Base ` M ) ) ) |
9 |
4 8
|
syl5bi |
|- ( A e. V -> ( x e. { h | h : A -onto-> A } -> x e. ( Base ` M ) ) ) |
10 |
9
|
ssrdv |
|- ( A e. V -> { h | h : A -onto-> A } C_ ( Base ` M ) ) |
11 |
1
|
efmndid |
|- ( A e. V -> ( _I |` A ) = ( 0g ` M ) ) |
12 |
|
resiexg |
|- ( A e. V -> ( _I |` A ) e. _V ) |
13 |
|
f1oi |
|- ( _I |` A ) : A -1-1-onto-> A |
14 |
|
f1ofo |
|- ( ( _I |` A ) : A -1-1-onto-> A -> ( _I |` A ) : A -onto-> A ) |
15 |
13 14
|
mp1i |
|- ( A e. V -> ( _I |` A ) : A -onto-> A ) |
16 |
|
foeq1 |
|- ( h = ( _I |` A ) -> ( h : A -onto-> A <-> ( _I |` A ) : A -onto-> A ) ) |
17 |
12 15 16
|
elabd |
|- ( A e. V -> ( _I |` A ) e. { h | h : A -onto-> A } ) |
18 |
11 17
|
eqeltrrd |
|- ( A e. V -> ( 0g ` M ) e. { h | h : A -onto-> A } ) |
19 |
|
vex |
|- y e. _V |
20 |
|
foeq1 |
|- ( h = y -> ( h : A -onto-> A <-> y : A -onto-> A ) ) |
21 |
19 20
|
elab |
|- ( y e. { h | h : A -onto-> A } <-> y : A -onto-> A ) |
22 |
4 21
|
anbi12i |
|- ( ( x e. { h | h : A -onto-> A } /\ y e. { h | h : A -onto-> A } ) <-> ( x : A -onto-> A /\ y : A -onto-> A ) ) |
23 |
|
foco |
|- ( ( x : A -onto-> A /\ y : A -onto-> A ) -> ( x o. y ) : A -onto-> A ) |
24 |
23
|
adantl |
|- ( ( A e. V /\ ( x : A -onto-> A /\ y : A -onto-> A ) ) -> ( x o. y ) : A -onto-> A ) |
25 |
|
fof |
|- ( y : A -onto-> A -> y : A --> A ) |
26 |
5 25
|
anim12i |
|- ( ( x : A -onto-> A /\ y : A -onto-> A ) -> ( x : A --> A /\ y : A --> A ) ) |
27 |
1 6
|
elefmndbas |
|- ( A e. V -> ( y e. ( Base ` M ) <-> y : A --> A ) ) |
28 |
7 27
|
anbi12d |
|- ( A e. V -> ( ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) <-> ( x : A --> A /\ y : A --> A ) ) ) |
29 |
26 28
|
syl5ibr |
|- ( A e. V -> ( ( x : A -onto-> A /\ y : A -onto-> A ) -> ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) ) ) |
30 |
29
|
imp |
|- ( ( A e. V /\ ( x : A -onto-> A /\ y : A -onto-> A ) ) -> ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) ) |
31 |
|
eqid |
|- ( +g ` M ) = ( +g ` M ) |
32 |
1 6 31
|
efmndov |
|- ( ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) -> ( x ( +g ` M ) y ) = ( x o. y ) ) |
33 |
30 32
|
syl |
|- ( ( A e. V /\ ( x : A -onto-> A /\ y : A -onto-> A ) ) -> ( x ( +g ` M ) y ) = ( x o. y ) ) |
34 |
33
|
eleq1d |
|- ( ( A e. V /\ ( x : A -onto-> A /\ y : A -onto-> A ) ) -> ( ( x ( +g ` M ) y ) e. { h | h : A -onto-> A } <-> ( x o. y ) e. { h | h : A -onto-> A } ) ) |
35 |
2 19
|
coex |
|- ( x o. y ) e. _V |
36 |
|
foeq1 |
|- ( h = ( x o. y ) -> ( h : A -onto-> A <-> ( x o. y ) : A -onto-> A ) ) |
37 |
35 36
|
elab |
|- ( ( x o. y ) e. { h | h : A -onto-> A } <-> ( x o. y ) : A -onto-> A ) |
38 |
34 37
|
bitrdi |
|- ( ( A e. V /\ ( x : A -onto-> A /\ y : A -onto-> A ) ) -> ( ( x ( +g ` M ) y ) e. { h | h : A -onto-> A } <-> ( x o. y ) : A -onto-> A ) ) |
39 |
24 38
|
mpbird |
|- ( ( A e. V /\ ( x : A -onto-> A /\ y : A -onto-> A ) ) -> ( x ( +g ` M ) y ) e. { h | h : A -onto-> A } ) |
40 |
39
|
ex |
|- ( A e. V -> ( ( x : A -onto-> A /\ y : A -onto-> A ) -> ( x ( +g ` M ) y ) e. { h | h : A -onto-> A } ) ) |
41 |
22 40
|
syl5bi |
|- ( A e. V -> ( ( x e. { h | h : A -onto-> A } /\ y e. { h | h : A -onto-> A } ) -> ( x ( +g ` M ) y ) e. { h | h : A -onto-> A } ) ) |
42 |
41
|
ralrimivv |
|- ( A e. V -> A. x e. { h | h : A -onto-> A } A. y e. { h | h : A -onto-> A } ( x ( +g ` M ) y ) e. { h | h : A -onto-> A } ) |
43 |
1
|
efmndmnd |
|- ( A e. V -> M e. Mnd ) |
44 |
|
eqid |
|- ( 0g ` M ) = ( 0g ` M ) |
45 |
6 44 31
|
issubm |
|- ( M e. Mnd -> ( { h | h : A -onto-> A } e. ( SubMnd ` M ) <-> ( { h | h : A -onto-> A } C_ ( Base ` M ) /\ ( 0g ` M ) e. { h | h : A -onto-> A } /\ A. x e. { h | h : A -onto-> A } A. y e. { h | h : A -onto-> A } ( x ( +g ` M ) y ) e. { h | h : A -onto-> A } ) ) ) |
46 |
43 45
|
syl |
|- ( A e. V -> ( { h | h : A -onto-> A } e. ( SubMnd ` M ) <-> ( { h | h : A -onto-> A } C_ ( Base ` M ) /\ ( 0g ` M ) e. { h | h : A -onto-> A } /\ A. x e. { h | h : A -onto-> A } A. y e. { h | h : A -onto-> A } ( x ( +g ` M ) y ) e. { h | h : A -onto-> A } ) ) ) |
47 |
10 18 42 46
|
mpbir3and |
|- ( A e. V -> { h | h : A -onto-> A } e. ( SubMnd ` M ) ) |