Step |
Hyp |
Ref |
Expression |
1 |
|
gexcl.1 |
|- X = ( Base ` G ) |
2 |
|
gexcl.2 |
|- E = ( gEx ` G ) |
3 |
|
eqid |
|- ( .g ` G ) = ( .g ` G ) |
4 |
|
eqid |
|- ( 0g ` G ) = ( 0g ` G ) |
5 |
|
eqid |
|- { y e. NN | A. x e. X ( y ( .g ` G ) x ) = ( 0g ` G ) } = { y e. NN | A. x e. X ( y ( .g ` G ) x ) = ( 0g ` G ) } |
6 |
1 3 4 2 5
|
gexlem1 |
|- ( G e. V -> ( ( E = 0 /\ { y e. NN | A. x e. X ( y ( .g ` G ) x ) = ( 0g ` G ) } = (/) ) \/ E e. { y e. NN | A. x e. X ( y ( .g ` G ) x ) = ( 0g ` G ) } ) ) |
7 |
|
simpl |
|- ( ( E = 0 /\ { y e. NN | A. x e. X ( y ( .g ` G ) x ) = ( 0g ` G ) } = (/) ) -> E = 0 ) |
8 |
|
elrabi |
|- ( E e. { y e. NN | A. x e. X ( y ( .g ` G ) x ) = ( 0g ` G ) } -> E e. NN ) |
9 |
7 8
|
orim12i |
|- ( ( ( E = 0 /\ { y e. NN | A. x e. X ( y ( .g ` G ) x ) = ( 0g ` G ) } = (/) ) \/ E e. { y e. NN | A. x e. X ( y ( .g ` G ) x ) = ( 0g ` G ) } ) -> ( E = 0 \/ E e. NN ) ) |
10 |
6 9
|
syl |
|- ( G e. V -> ( E = 0 \/ E e. NN ) ) |
11 |
10
|
orcomd |
|- ( G e. V -> ( E e. NN \/ E = 0 ) ) |
12 |
|
elnn0 |
|- ( E e. NN0 <-> ( E e. NN \/ E = 0 ) ) |
13 |
11 12
|
sylibr |
|- ( G e. V -> E e. NN0 ) |