Metamath Proof Explorer

Theorem infcvgaux2i

Description: Auxiliary theorem for applications of supcvg . (Contributed by NM, 4-Mar-2008)

Ref Expression
Hypotheses infcvg.1 
|- R = { x | E. y e. X x = -u A }
infcvg.2 
|- ( y e. X -> A e. RR )
infcvg.3 
|- Z e. X
infcvg.4 
|- E. z e. RR A. w e. R w <_ z
infcvg.5a 
|- S = -u sup ( R , RR , < )
infcvg.13 
|- ( y = C -> A = B )
Assertion infcvgaux2i 
|- ( C e. X -> S <_ B )

Proof

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 )