Step |
Hyp |
Ref |
Expression |
1 |
|
gexcl.1 |
|- X = ( Base ` G ) |
2 |
|
gexcl.2 |
|- E = ( gEx ` G ) |
3 |
|
gexid.3 |
|- .x. = ( .g ` G ) |
4 |
|
gexid.4 |
|- .0. = ( 0g ` G ) |
5 |
|
oveq1 |
|- ( y = N -> ( y .x. x ) = ( N .x. x ) ) |
6 |
5
|
eqeq1d |
|- ( y = N -> ( ( y .x. x ) = .0. <-> ( N .x. x ) = .0. ) ) |
7 |
6
|
ralbidv |
|- ( y = N -> ( A. x e. X ( y .x. x ) = .0. <-> A. x e. X ( N .x. x ) = .0. ) ) |
8 |
7
|
elrab |
|- ( N e. { y e. NN | A. x e. X ( y .x. x ) = .0. } <-> ( N e. NN /\ A. x e. X ( N .x. x ) = .0. ) ) |
9 |
|
eqid |
|- { y e. NN | A. x e. X ( y .x. x ) = .0. } = { y e. NN | A. x e. X ( y .x. x ) = .0. } |
10 |
1 3 4 2 9
|
gexval |
|- ( G e. V -> E = if ( { y e. NN | A. x e. X ( y .x. x ) = .0. } = (/) , 0 , inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) ) ) |
11 |
|
ne0i |
|- ( N e. { y e. NN | A. x e. X ( y .x. x ) = .0. } -> { y e. NN | A. x e. X ( y .x. x ) = .0. } =/= (/) ) |
12 |
|
ifnefalse |
|- ( { y e. NN | A. x e. X ( y .x. x ) = .0. } =/= (/) -> if ( { y e. NN | A. x e. X ( y .x. x ) = .0. } = (/) , 0 , inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) ) = inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) ) |
13 |
11 12
|
syl |
|- ( N e. { y e. NN | A. x e. X ( y .x. x ) = .0. } -> if ( { y e. NN | A. x e. X ( y .x. x ) = .0. } = (/) , 0 , inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) ) = inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) ) |
14 |
10 13
|
sylan9eq |
|- ( ( G e. V /\ N e. { y e. NN | A. x e. X ( y .x. x ) = .0. } ) -> E = inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) ) |
15 |
|
ssrab2 |
|- { y e. NN | A. x e. X ( y .x. x ) = .0. } C_ NN |
16 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
17 |
15 16
|
sseqtri |
|- { y e. NN | A. x e. X ( y .x. x ) = .0. } C_ ( ZZ>= ` 1 ) |
18 |
11
|
adantl |
|- ( ( G e. V /\ N e. { y e. NN | A. x e. X ( y .x. x ) = .0. } ) -> { y e. NN | A. x e. X ( y .x. x ) = .0. } =/= (/) ) |
19 |
|
infssuzcl |
|- ( ( { y e. NN | A. x e. X ( y .x. x ) = .0. } C_ ( ZZ>= ` 1 ) /\ { y e. NN | A. x e. X ( y .x. x ) = .0. } =/= (/) ) -> inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) e. { y e. NN | A. x e. X ( y .x. x ) = .0. } ) |
20 |
17 18 19
|
sylancr |
|- ( ( G e. V /\ N e. { y e. NN | A. x e. X ( y .x. x ) = .0. } ) -> inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) e. { y e. NN | A. x e. X ( y .x. x ) = .0. } ) |
21 |
15 20
|
sselid |
|- ( ( G e. V /\ N e. { y e. NN | A. x e. X ( y .x. x ) = .0. } ) -> inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) e. NN ) |
22 |
|
infssuzle |
|- ( ( { y e. NN | A. x e. X ( y .x. x ) = .0. } C_ ( ZZ>= ` 1 ) /\ N e. { y e. NN | A. x e. X ( y .x. x ) = .0. } ) -> inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) <_ N ) |
23 |
17 22
|
mpan |
|- ( N e. { y e. NN | A. x e. X ( y .x. x ) = .0. } -> inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) <_ N ) |
24 |
23
|
adantl |
|- ( ( G e. V /\ N e. { y e. NN | A. x e. X ( y .x. x ) = .0. } ) -> inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) <_ N ) |
25 |
|
elrabi |
|- ( N e. { y e. NN | A. x e. X ( y .x. x ) = .0. } -> N e. NN ) |
26 |
25
|
nnzd |
|- ( N e. { y e. NN | A. x e. X ( y .x. x ) = .0. } -> N e. ZZ ) |
27 |
|
fznn |
|- ( N e. ZZ -> ( inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) e. ( 1 ... N ) <-> ( inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) e. NN /\ inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) <_ N ) ) ) |
28 |
26 27
|
syl |
|- ( N e. { y e. NN | A. x e. X ( y .x. x ) = .0. } -> ( inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) e. ( 1 ... N ) <-> ( inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) e. NN /\ inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) <_ N ) ) ) |
29 |
28
|
adantl |
|- ( ( G e. V /\ N e. { y e. NN | A. x e. X ( y .x. x ) = .0. } ) -> ( inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) e. ( 1 ... N ) <-> ( inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) e. NN /\ inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) <_ N ) ) ) |
30 |
21 24 29
|
mpbir2and |
|- ( ( G e. V /\ N e. { y e. NN | A. x e. X ( y .x. x ) = .0. } ) -> inf ( { y e. NN | A. x e. X ( y .x. x ) = .0. } , RR , < ) e. ( 1 ... N ) ) |
31 |
14 30
|
eqeltrd |
|- ( ( G e. V /\ N e. { y e. NN | A. x e. X ( y .x. x ) = .0. } ) -> E e. ( 1 ... N ) ) |
32 |
8 31
|
sylan2br |
|- ( ( G e. V /\ ( N e. NN /\ A. x e. X ( N .x. x ) = .0. ) ) -> E e. ( 1 ... N ) ) |
33 |
32
|
3impb |
|- ( ( G e. V /\ N e. NN /\ A. x e. X ( N .x. x ) = .0. ) -> E e. ( 1 ... N ) ) |