Step |
Hyp |
Ref |
Expression |
1 |
|
gexval.1 |
|- X = ( Base ` G ) |
2 |
|
gexval.2 |
|- .x. = ( .g ` G ) |
3 |
|
gexval.3 |
|- .0. = ( 0g ` G ) |
4 |
|
gexval.4 |
|- E = ( gEx ` G ) |
5 |
|
gexval.i |
|- I = { y e. NN | A. x e. X ( y .x. x ) = .0. } |
6 |
1 2 3 4 5
|
gexval |
|- ( G e. V -> E = if ( I = (/) , 0 , inf ( I , RR , < ) ) ) |
7 |
|
eqeq2 |
|- ( 0 = if ( I = (/) , 0 , inf ( I , RR , < ) ) -> ( E = 0 <-> E = if ( I = (/) , 0 , inf ( I , RR , < ) ) ) ) |
8 |
7
|
imbi1d |
|- ( 0 = if ( I = (/) , 0 , inf ( I , RR , < ) ) -> ( ( E = 0 -> ( ( E = 0 /\ I = (/) ) \/ E e. I ) ) <-> ( E = if ( I = (/) , 0 , inf ( I , RR , < ) ) -> ( ( E = 0 /\ I = (/) ) \/ E e. I ) ) ) ) |
9 |
|
eqeq2 |
|- ( inf ( I , RR , < ) = if ( I = (/) , 0 , inf ( I , RR , < ) ) -> ( E = inf ( I , RR , < ) <-> E = if ( I = (/) , 0 , inf ( I , RR , < ) ) ) ) |
10 |
9
|
imbi1d |
|- ( inf ( I , RR , < ) = if ( I = (/) , 0 , inf ( I , RR , < ) ) -> ( ( E = inf ( I , RR , < ) -> ( ( E = 0 /\ I = (/) ) \/ E e. I ) ) <-> ( E = if ( I = (/) , 0 , inf ( I , RR , < ) ) -> ( ( E = 0 /\ I = (/) ) \/ E e. I ) ) ) ) |
11 |
|
orc |
|- ( ( E = 0 /\ I = (/) ) -> ( ( E = 0 /\ I = (/) ) \/ E e. I ) ) |
12 |
11
|
expcom |
|- ( I = (/) -> ( E = 0 -> ( ( E = 0 /\ I = (/) ) \/ E e. I ) ) ) |
13 |
12
|
adantl |
|- ( ( G e. V /\ I = (/) ) -> ( E = 0 -> ( ( E = 0 /\ I = (/) ) \/ E e. I ) ) ) |
14 |
|
ssrab2 |
|- { y e. NN | A. x e. X ( y .x. x ) = .0. } C_ NN |
15 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
16 |
15
|
eqcomi |
|- ( ZZ>= ` 1 ) = NN |
17 |
14 5 16
|
3sstr4i |
|- I C_ ( ZZ>= ` 1 ) |
18 |
|
neqne |
|- ( -. I = (/) -> I =/= (/) ) |
19 |
18
|
adantl |
|- ( ( G e. V /\ -. I = (/) ) -> I =/= (/) ) |
20 |
|
infssuzcl |
|- ( ( I C_ ( ZZ>= ` 1 ) /\ I =/= (/) ) -> inf ( I , RR , < ) e. I ) |
21 |
17 19 20
|
sylancr |
|- ( ( G e. V /\ -. I = (/) ) -> inf ( I , RR , < ) e. I ) |
22 |
|
eleq1a |
|- ( inf ( I , RR , < ) e. I -> ( E = inf ( I , RR , < ) -> E e. I ) ) |
23 |
21 22
|
syl |
|- ( ( G e. V /\ -. I = (/) ) -> ( E = inf ( I , RR , < ) -> E e. I ) ) |
24 |
|
olc |
|- ( E e. I -> ( ( E = 0 /\ I = (/) ) \/ E e. I ) ) |
25 |
23 24
|
syl6 |
|- ( ( G e. V /\ -. I = (/) ) -> ( E = inf ( I , RR , < ) -> ( ( E = 0 /\ I = (/) ) \/ E e. I ) ) ) |
26 |
8 10 13 25
|
ifbothda |
|- ( G e. V -> ( E = if ( I = (/) , 0 , inf ( I , RR , < ) ) -> ( ( E = 0 /\ I = (/) ) \/ E e. I ) ) ) |
27 |
6 26
|
mpd |
|- ( G e. V -> ( ( E = 0 /\ I = (/) ) \/ E e. I ) ) |