| Step |
Hyp |
Ref |
Expression |
| 1 |
|
infcvg.1 |
|- R = { x | E. y e. X x = -u A } |
| 2 |
|
infcvg.2 |
|- ( y e. X -> A e. RR ) |
| 3 |
|
infcvg.3 |
|- Z e. X |
| 4 |
|
infcvg.4 |
|- E. z e. RR A. w e. R w <_ z |
| 5 |
|
infcvg.5a |
|- S = -u sup ( R , RR , < ) |
| 6 |
|
infcvg.13 |
|- ( y = C -> A = B ) |
| 7 |
|
eqid |
|- -u B = -u B |
| 8 |
6
|
negeqd |
|- ( y = C -> -u A = -u B ) |
| 9 |
8
|
rspceeqv |
|- ( ( C e. X /\ -u B = -u B ) -> E. y e. X -u B = -u A ) |
| 10 |
7 9
|
mpan2 |
|- ( C e. X -> E. y e. X -u B = -u A ) |
| 11 |
|
negex |
|- -u B e. _V |
| 12 |
|
eqeq1 |
|- ( x = -u B -> ( x = -u A <-> -u B = -u A ) ) |
| 13 |
12
|
rexbidv |
|- ( x = -u B -> ( E. y e. X x = -u A <-> E. y e. X -u B = -u A ) ) |
| 14 |
11 13 1
|
elab2 |
|- ( -u B e. R <-> E. y e. X -u B = -u A ) |
| 15 |
10 14
|
sylibr |
|- ( C e. X -> -u B e. R ) |
| 16 |
1 2 3 4
|
infcvgaux1i |
|- ( R C_ RR /\ R =/= (/) /\ E. z e. RR A. w e. R w <_ z ) |
| 17 |
16
|
suprubii |
|- ( -u B e. R -> -u B <_ sup ( R , RR , < ) ) |
| 18 |
15 17
|
syl |
|- ( C e. X -> -u B <_ sup ( R , RR , < ) ) |
| 19 |
6
|
eleq1d |
|- ( y = C -> ( A e. RR <-> B e. RR ) ) |
| 20 |
19 2
|
vtoclga |
|- ( C e. X -> B e. RR ) |
| 21 |
16
|
suprclii |
|- sup ( R , RR , < ) e. RR |
| 22 |
|
lenegcon1 |
|- ( ( B e. RR /\ sup ( R , RR , < ) e. RR ) -> ( -u B <_ sup ( R , RR , < ) <-> -u sup ( R , RR , < ) <_ B ) ) |
| 23 |
20 21 22
|
sylancl |
|- ( C e. X -> ( -u B <_ sup ( R , RR , < ) <-> -u sup ( R , RR , < ) <_ B ) ) |
| 24 |
18 23
|
mpbid |
|- ( C e. X -> -u sup ( R , RR , < ) <_ B ) |
| 25 |
5 24
|
eqbrtrid |
|- ( C e. X -> S <_ B ) |