This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem infcvgaux1i

Description: Auxiliary theorem for applications of supcvg . Hypothesis for several supremum theorems. (Contributed by NM, 8-Feb-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
Assertion infcvgaux1i 
|- ( R C_ RR /\ R =/= (/) /\ E. z e. RR A. w e. R w <_ z )

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 2 renegcld 
 |-  ( y e. X -> -u A e. RR )
6 eleq1 
 |-  ( x = -u A -> ( x e. RR <-> -u A e. RR ) )
7 5 6 syl5ibrcom 
 |-  ( y e. X -> ( x = -u A -> x e. RR ) )
8 7 rexlimiv 
 |-  ( E. y e. X x = -u A -> x e. RR )
9 8 abssi 
 |-  { x | E. y e. X x = -u A } C_ RR
10 1 9 eqsstri 
 |-  R C_ RR
11 eqid 
 |-  -u [_ Z / y ]_ A = -u [_ Z / y ]_ A
12 11 nfth 
 |-  F/ y -u [_ Z / y ]_ A = -u [_ Z / y ]_ A
13 csbeq1a 
 |-  ( y = Z -> A = [_ Z / y ]_ A )
14 13 negeqd 
 |-  ( y = Z -> -u A = -u [_ Z / y ]_ A )
15 14 eqeq2d 
 |-  ( y = Z -> ( -u [_ Z / y ]_ A = -u A <-> -u [_ Z / y ]_ A = -u [_ Z / y ]_ A ) )
16 12 15 rspce 
 |-  ( ( Z e. X /\ -u [_ Z / y ]_ A = -u [_ Z / y ]_ A ) -> E. y e. X -u [_ Z / y ]_ A = -u A )
17 3 11 16 mp2an 
 |-  E. y e. X -u [_ Z / y ]_ A = -u A
18 negex 
 |-  -u [_ Z / y ]_ A e. _V
19 nfcsb1v 
 |-  F/_ y [_ Z / y ]_ A
20 19 nfneg 
 |-  F/_ y -u [_ Z / y ]_ A
21 20 nfeq2 
 |-  F/ y x = -u [_ Z / y ]_ A
22 eqeq1 
 |-  ( x = -u [_ Z / y ]_ A -> ( x = -u A <-> -u [_ Z / y ]_ A = -u A ) )
23 21 22 rexbid 
 |-  ( x = -u [_ Z / y ]_ A -> ( E. y e. X x = -u A <-> E. y e. X -u [_ Z / y ]_ A = -u A ) )
24 18 23 elab 
 |-  ( -u [_ Z / y ]_ A e. { x | E. y e. X x = -u A } <-> E. y e. X -u [_ Z / y ]_ A = -u A )
25 17 24 mpbir 
 |-  -u [_ Z / y ]_ A e. { x | E. y e. X x = -u A }
26 25 1 eleqtrri 
 |-  -u [_ Z / y ]_ A e. R
27 26 ne0ii 
 |-  R =/= (/)
28 10 27 4 3pm3.2i 
 |-  ( R C_ RR /\ R =/= (/) /\ E. z e. RR A. w e. R w <_ z )