Step |
Hyp |
Ref |
Expression |
0 |
|
csubmnd |
|- SubMnd |
1 |
|
vs |
|- s |
2 |
|
cmnd |
|- Mnd |
3 |
|
vt |
|- t |
4 |
|
cbs |
|- Base |
5 |
1
|
cv |
|- s |
6 |
5 4
|
cfv |
|- ( Base ` s ) |
7 |
6
|
cpw |
|- ~P ( Base ` s ) |
8 |
|
c0g |
|- 0g |
9 |
5 8
|
cfv |
|- ( 0g ` s ) |
10 |
3
|
cv |
|- t |
11 |
9 10
|
wcel |
|- ( 0g ` s ) e. t |
12 |
|
vx |
|- x |
13 |
|
vy |
|- y |
14 |
12
|
cv |
|- x |
15 |
|
cplusg |
|- +g |
16 |
5 15
|
cfv |
|- ( +g ` s ) |
17 |
13
|
cv |
|- y |
18 |
14 17 16
|
co |
|- ( x ( +g ` s ) y ) |
19 |
18 10
|
wcel |
|- ( x ( +g ` s ) y ) e. t |
20 |
19 13 10
|
wral |
|- A. y e. t ( x ( +g ` s ) y ) e. t |
21 |
20 12 10
|
wral |
|- A. x e. t A. y e. t ( x ( +g ` s ) y ) e. t |
22 |
11 21
|
wa |
|- ( ( 0g ` s ) e. t /\ A. x e. t A. y e. t ( x ( +g ` s ) y ) e. t ) |
23 |
22 3 7
|
crab |
|- { t e. ~P ( Base ` s ) | ( ( 0g ` s ) e. t /\ A. x e. t A. y e. t ( x ( +g ` s ) y ) e. t ) } |
24 |
1 2 23
|
cmpt |
|- ( s e. Mnd |-> { t e. ~P ( Base ` s ) | ( ( 0g ` s ) e. t /\ A. x e. t A. y e. t ( x ( +g ` s ) y ) e. t ) } ) |
25 |
0 24
|
wceq |
|- SubMnd = ( s e. Mnd |-> { t e. ~P ( Base ` s ) | ( ( 0g ` s ) e. t /\ A. x e. t A. y e. t ( x ( +g ` s ) y ) e. t ) } ) |