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 | y X x = A
infcvg.2 y X A
infcvg.3 Z X
infcvg.4 z w R w z
Assertion infcvgaux1i R R z w R w z

Proof

Step Hyp Ref Expression
1 infcvg.1 R = x | y X x = A
2 infcvg.2 y X A
3 infcvg.3 Z X
4 infcvg.4 z w R w z
5 2 renegcld y X A
6 eleq1 x = A x A
7 5 6 syl5ibrcom y X x = A x
8 7 rexlimiv y X x = A x
9 8 abssi x | y X x = A
10 1 9 eqsstri R
11 eqid Z / y A = Z / y A
12 11 nfth y Z / y A = Z / y A
13 csbeq1a y = Z A = Z / y A
14 13 negeqd y = Z A = Z / y A
15 14 eqeq2d y = Z Z / y A = A Z / y A = Z / y A
16 12 15 rspce Z X Z / y A = Z / y A y X Z / y A = A
17 3 11 16 mp2an y X Z / y A = A
18 negex Z / y A V
19 nfcsb1v _ y Z / y A
20 19 nfneg _ y Z / y A
21 20 nfeq2 y x = Z / y A
22 eqeq1 x = Z / y A x = A Z / y A = A
23 21 22 rexbid x = Z / y A y X x = A y X Z / y A = A
24 18 23 elab Z / y A x | y X x = A y X Z / y A = A
25 17 24 mpbir Z / y A x | y X x = A
26 25 1 eleqtrri Z / y A R
27 26 ne0ii R
28 10 27 4 3pm3.2i R R z w R w z