Step |
Hyp |
Ref |
Expression |
1 |
|
mgmidsssn0.b |
|- B = ( Base ` G ) |
2 |
|
mgmidsssn0.z |
|- .0. = ( 0g ` G ) |
3 |
|
mgmidsssn0.p |
|- .+ = ( +g ` G ) |
4 |
|
mgmidsssn0.o |
|- O = { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } |
5 |
|
simpr |
|- ( ( G e. V /\ ( x e. B /\ A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) ) -> ( x e. B /\ A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) ) |
6 |
|
oveq1 |
|- ( z = x -> ( z .+ y ) = ( x .+ y ) ) |
7 |
6
|
eqeq1d |
|- ( z = x -> ( ( z .+ y ) = y <-> ( x .+ y ) = y ) ) |
8 |
7
|
ovanraleqv |
|- ( z = x -> ( A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) <-> A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) ) |
9 |
8
|
rspcev |
|- ( ( x e. B /\ A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) -> E. z e. B A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) ) |
10 |
9
|
adantl |
|- ( ( G e. V /\ ( x e. B /\ A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) ) -> E. z e. B A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) ) |
11 |
1 2 3 10
|
ismgmid |
|- ( ( G e. V /\ ( x e. B /\ A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) ) -> ( ( x e. B /\ A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) <-> .0. = x ) ) |
12 |
5 11
|
mpbid |
|- ( ( G e. V /\ ( x e. B /\ A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) ) -> .0. = x ) |
13 |
12
|
eqcomd |
|- ( ( G e. V /\ ( x e. B /\ A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) ) -> x = .0. ) |
14 |
|
velsn |
|- ( x e. { .0. } <-> x = .0. ) |
15 |
13 14
|
sylibr |
|- ( ( G e. V /\ ( x e. B /\ A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) ) -> x e. { .0. } ) |
16 |
15
|
expr |
|- ( ( G e. V /\ x e. B ) -> ( A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) -> x e. { .0. } ) ) |
17 |
16
|
ralrimiva |
|- ( G e. V -> A. x e. B ( A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) -> x e. { .0. } ) ) |
18 |
|
rabss |
|- ( { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } C_ { .0. } <-> A. x e. B ( A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) -> x e. { .0. } ) ) |
19 |
17 18
|
sylibr |
|- ( G e. V -> { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } C_ { .0. } ) |
20 |
4 19
|
eqsstrid |
|- ( G e. V -> O C_ { .0. } ) |