Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sge0iunmpt Structured version   Unicode version

Theorem sge0iunmpt 38015
Description: Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypotheses
Ref Expression
sge0iunmpt.a  |-  ( ph  ->  A  e.  V )
sge0iunmpt.b  |-  ( (
ph  /\  x  e.  A )  ->  B  e.  W )
sge0iunmpt.dj  |-  ( ph  -> Disj  x  e.  A  B
)
sge0iunmpt.c  |-  ( (
ph  /\  x  e.  A  /\  k  e.  B
)  ->  C  e.  ( 0 [,] +oo ) )
Assertion
Ref Expression
sge0iunmpt  |-  ( ph  ->  (Σ^ `  ( k  e.  U_ x  e.  A  B  |->  C ) )  =  (Σ^ `  ( x  e.  A  |->  (Σ^ `  ( k  e.  B  |->  C ) ) ) ) )
Distinct variable groups:    A, k, x    B, k    x, C   
x, W    ph, k, x
Allowed substitution hints:    B( x)    C( k)    V( x, k)    W( k)

Proof of Theorem sge0iunmpt
Dummy variables  j 
y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1751 . . . 4  |-  F/ x ph
2 nfcv 2582 . . . . . 6  |-  F/_ xΣ^
3 nfiu1 4323 . . . . . . 7  |-  F/_ x U_ x  e.  A  B
4 nfcv 2582 . . . . . . 7  |-  F/_ x C
53, 4nfmpt 4506 . . . . . 6  |-  F/_ x
( k  e.  U_ x  e.  A  B  |->  C )
62, 5nffv 5880 . . . . 5  |-  F/_ x
(Σ^ `  ( k  e.  U_ x  e.  A  B  |->  C ) )
7 nfmpt1 4507 . . . . . 6  |-  F/_ x
( x  e.  A  |->  (Σ^ `  ( k  e.  B  |->  C ) ) )
82, 7nffv 5880 . . . . 5  |-  F/_ x
(Σ^ `  ( x  e.  A  |->  (Σ^ `  ( k  e.  B  |->  C ) ) ) )
96, 8nfeq 2593 . . . 4  |-  F/ x
(Σ^ `  ( k  e.  U_ x  e.  A  B  |->  C ) )  =  (Σ^ `  ( x  e.  A  |->  (Σ^ `  ( k  e.  B  |->  C ) ) ) )
10 sge0iunmpt.a . . . . . . . . . 10  |-  ( ph  ->  A  e.  V )
11 sge0iunmpt.b . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  B  e.  W )
1211ralrimiva 2837 . . . . . . . . . 10  |-  ( ph  ->  A. x  e.  A  B  e.  W )
13 iunexg 6775 . . . . . . . . . 10  |-  ( ( A  e.  V  /\  A. x  e.  A  B  e.  W )  ->  U_ x  e.  A  B  e.  _V )
1410, 12, 13syl2anc 665 . . . . . . . . 9  |-  ( ph  ->  U_ x  e.  A  B  e.  _V )
15 eliun 4298 . . . . . . . . . . . . 13  |-  ( k  e.  U_ x  e.  A  B  <->  E. x  e.  A  k  e.  B )
1615biimpi 197 . . . . . . . . . . . 12  |-  ( k  e.  U_ x  e.  A  B  ->  E. x  e.  A  k  e.  B )
1716adantl 467 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  U_ x  e.  A  B
)  ->  E. x  e.  A  k  e.  B )
18 nfcv 2582 . . . . . . . . . . . . . 14  |-  F/_ x
k
1918, 3nfel 2595 . . . . . . . . . . . . 13  |-  F/ x  k  e.  U_ x  e.  A  B
201, 19nfan 1983 . . . . . . . . . . . 12  |-  F/ x
( ph  /\  k  e.  U_ x  e.  A  B )
214nfel1 2598 . . . . . . . . . . . 12  |-  F/ x  C  e.  ( 0 [,] +oo )
22 sge0iunmpt.c . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  A  /\  k  e.  B
)  ->  C  e.  ( 0 [,] +oo ) )
23223exp 1204 . . . . . . . . . . . . 13  |-  ( ph  ->  ( x  e.  A  ->  ( k  e.  B  ->  C  e.  ( 0 [,] +oo ) ) ) )
2423adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  U_ x  e.  A  B
)  ->  ( x  e.  A  ->  ( k  e.  B  ->  C  e.  ( 0 [,] +oo ) ) ) )
2520, 21, 24rexlimd 2907 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  U_ x  e.  A  B
)  ->  ( E. x  e.  A  k  e.  B  ->  C  e.  ( 0 [,] +oo ) ) )
2617, 25mpd 15 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  U_ x  e.  A  B
)  ->  C  e.  ( 0 [,] +oo ) )
27 eqid 2420 . . . . . . . . . 10  |-  ( k  e.  U_ x  e.  A  B  |->  C )  =  ( k  e. 
U_ x  e.  A  B  |->  C )
2826, 27fmptd 6053 . . . . . . . . 9  |-  ( ph  ->  ( k  e.  U_ x  e.  A  B  |->  C ) : U_ x  e.  A  B --> ( 0 [,] +oo ) )
2914, 28sge0xrcl 37982 . . . . . . . 8  |-  ( ph  ->  (Σ^ `  ( k  e.  U_ x  e.  A  B  |->  C ) )  e. 
RR* )
30293ad2ant1 1026 . . . . . . 7  |-  ( (
ph  /\  x  e.  A  /\  (Σ^ `  ( k  e.  B  |->  C ) )  = +oo )  ->  (Σ^ `  (
k  e.  U_ x  e.  A  B  |->  C ) )  e.  RR* )
31 id 23 . . . . . . . . . . 11  |-  ( (Σ^ `  (
k  e.  B  |->  C ) )  = +oo  ->  (Σ^ `  ( k  e.  B  |->  C ) )  = +oo )
3231eqcomd 2428 . . . . . . . . . 10  |-  ( (Σ^ `  (
k  e.  B  |->  C ) )  = +oo  -> +oo  =  (Σ^ `  ( k  e.  B  |->  C ) ) )
3332adantl 467 . . . . . . . . 9  |-  ( ( x  e.  A  /\  (Σ^ `  ( k  e.  B  |->  C ) )  = +oo )  -> +oo  =  (Σ^ `  ( k  e.  B  |->  C ) ) )
34333adant1 1023 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A  /\  (Σ^ `  ( k  e.  B  |->  C ) )  = +oo )  -> +oo  =  (Σ^ `  ( k  e.  B  |->  C ) ) )
3514adantr 466 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  U_ x  e.  A  B  e.  _V )
3626adantlr 719 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  A )  /\  k  e.  U_ x  e.  A  B )  ->  C  e.  ( 0 [,] +oo ) )
37 ssiun2 4336 . . . . . . . . . . 11  |-  ( x  e.  A  ->  B  C_ 
U_ x  e.  A  B )
3837adantl 467 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  B  C_ 
U_ x  e.  A  B )
3935, 36, 38sge0lessmpt 37996 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  (Σ^ `  (
k  e.  B  |->  C ) )  <_  (Σ^ `  (
k  e.  U_ x  e.  A  B  |->  C ) ) )
40393adant3 1025 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A  /\  (Σ^ `  ( k  e.  B  |->  C ) )  = +oo )  ->  (Σ^ `  (
k  e.  B  |->  C ) )  <_  (Σ^ `  (
k  e.  U_ x  e.  A  B  |->  C ) ) )
4134, 40eqbrtrd 4438 . . . . . . 7  |-  ( (
ph  /\  x  e.  A  /\  (Σ^ `  ( k  e.  B  |->  C ) )  = +oo )  -> +oo  <_  (Σ^ `  (
k  e.  U_ x  e.  A  B  |->  C ) ) )
4230, 41xrgepnfd 37378 . . . . . 6  |-  ( (
ph  /\  x  e.  A  /\  (Σ^ `  ( k  e.  B  |->  C ) )  = +oo )  ->  (Σ^ `  (
k  e.  U_ x  e.  A  B  |->  C ) )  = +oo )
43103ad2ant1 1026 . . . . . . 7  |-  ( (
ph  /\  x  e.  A  /\  (Σ^ `  ( k  e.  B  |->  C ) )  = +oo )  ->  A  e.  V )
44 nfv 1751 . . . . . . . . . . . . 13  |-  F/ x
( ph  /\  y  e.  A )
45 nfcsb1v 3408 . . . . . . . . . . . . . 14  |-  F/_ x [_ y  /  x ]_ B
46 nfcsb1v 3408 . . . . . . . . . . . . . 14  |-  F/_ x [_ y  /  x ]_ W
4745, 46nfel 2595 . . . . . . . . . . . . 13  |-  F/ x [_ y  /  x ]_ B  e.  [_ y  /  x ]_ W
4844, 47nfim 1975 . . . . . . . . . . . 12  |-  F/ x
( ( ph  /\  y  e.  A )  ->  [_ y  /  x ]_ B  e.  [_ y  /  x ]_ W )
49 eleq1 2492 . . . . . . . . . . . . . 14  |-  ( x  =  y  ->  (
x  e.  A  <->  y  e.  A ) )
5049anbi2d 708 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  (
( ph  /\  x  e.  A )  <->  ( ph  /\  y  e.  A ) ) )
51 csbeq1a 3401 . . . . . . . . . . . . . 14  |-  ( x  =  y  ->  B  =  [_ y  /  x ]_ B )
52 csbeq1a 3401 . . . . . . . . . . . . . 14  |-  ( x  =  y  ->  W  =  [_ y  /  x ]_ W )
5351, 52eleq12d 2502 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  ( B  e.  W  <->  [_ y  /  x ]_ B  e.  [_ y  /  x ]_ W
) )
5450, 53imbi12d 321 . . . . . . . . . . . 12  |-  ( x  =  y  ->  (
( ( ph  /\  x  e.  A )  ->  B  e.  W )  <-> 
( ( ph  /\  y  e.  A )  ->  [_ y  /  x ]_ B  e.  [_ y  /  x ]_ W ) ) )
5548, 54, 11chvar 2066 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  A )  ->  [_ y  /  x ]_ B  e. 
[_ y  /  x ]_ W )
5655adantlr 719 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  A )  /\  y  e.  A )  ->  [_ y  /  x ]_ B  e. 
[_ y  /  x ]_ W )
5745, 4nfmpt 4506 . . . . . . . . . . . . . 14  |-  F/_ x
( k  e.  [_ y  /  x ]_ B  |->  C )
58 nfcv 2582 . . . . . . . . . . . . . 14  |-  F/_ x
( 0 [,] +oo )
5957, 45, 58nff 5734 . . . . . . . . . . . . 13  |-  F/ x
( k  e.  [_ y  /  x ]_ B  |->  C ) : [_ y  /  x ]_ B --> ( 0 [,] +oo )
6044, 59nfim 1975 . . . . . . . . . . . 12  |-  F/ x
( ( ph  /\  y  e.  A )  ->  ( k  e.  [_ y  /  x ]_ B  |->  C ) : [_ y  /  x ]_ B --> ( 0 [,] +oo ) )
6151mpteq1d 4499 . . . . . . . . . . . . . 14  |-  ( x  =  y  ->  (
k  e.  B  |->  C )  =  ( k  e.  [_ y  /  x ]_ B  |->  C ) )
6261, 51feq12d 5727 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  (
( k  e.  B  |->  C ) : B --> ( 0 [,] +oo ) 
<->  ( k  e.  [_ y  /  x ]_ B  |->  C ) : [_ y  /  x ]_ B --> ( 0 [,] +oo ) ) )
6350, 62imbi12d 321 . . . . . . . . . . . 12  |-  ( x  =  y  ->  (
( ( ph  /\  x  e.  A )  ->  ( k  e.  B  |->  C ) : B --> ( 0 [,] +oo ) )  <->  ( ( ph  /\  y  e.  A
)  ->  ( k  e.  [_ y  /  x ]_ B  |->  C ) : [_ y  /  x ]_ B --> ( 0 [,] +oo ) ) ) )
6423imp31 433 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  A )  /\  k  e.  B )  ->  C  e.  ( 0 [,] +oo ) )
65 eqid 2420 . . . . . . . . . . . . 13  |-  ( k  e.  B  |->  C )  =  ( k  e.  B  |->  C )
6664, 65fmptd 6053 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  (
k  e.  B  |->  C ) : B --> ( 0 [,] +oo ) )
6760, 63, 66chvar 2066 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  A )  ->  (
k  e.  [_ y  /  x ]_ B  |->  C ) : [_ y  /  x ]_ B --> ( 0 [,] +oo ) )
6867adantlr 719 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  A )  /\  y  e.  A )  ->  (
k  e.  [_ y  /  x ]_ B  |->  C ) : [_ y  /  x ]_ B --> ( 0 [,] +oo ) )
6956, 68sge0cl 37978 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  A )  /\  y  e.  A )  ->  (Σ^ `  (
k  e.  [_ y  /  x ]_ B  |->  C ) )  e.  ( 0 [,] +oo )
)
70 nfcv 2582 . . . . . . . . . 10  |-  F/_ y
(Σ^ `  ( k  e.  B  |->  C ) )
712, 57nffv 5880 . . . . . . . . . 10  |-  F/_ x
(Σ^ `  ( k  e.  [_ y  /  x ]_ B  |->  C ) )
7261fveq2d 5877 . . . . . . . . . 10  |-  ( x  =  y  ->  (Σ^ `  (
k  e.  B  |->  C ) )  =  (Σ^ `  (
k  e.  [_ y  /  x ]_ B  |->  C ) ) )
7370, 71, 72cbvmpt 4509 . . . . . . . . 9  |-  ( x  e.  A  |->  (Σ^ `  ( k  e.  B  |->  C ) ) )  =  ( y  e.  A  |->  (Σ^ `  ( k  e.  [_ y  /  x ]_ B  |->  C ) ) )
7469, 73fmptd 6053 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  (
x  e.  A  |->  (Σ^ `  (
k  e.  B  |->  C ) ) ) : A --> ( 0 [,] +oo ) )
75743adant3 1025 . . . . . . 7  |-  ( (
ph  /\  x  e.  A  /\  (Σ^ `  ( k  e.  B  |->  C ) )  = +oo )  ->  (
x  e.  A  |->  (Σ^ `  (
k  e.  B  |->  C ) ) ) : A --> ( 0 [,] +oo ) )
76 id 23 . . . . . . . . . . 11  |-  ( x  e.  A  ->  x  e.  A )
77 fvex 5883 . . . . . . . . . . . 12  |-  (Σ^ `  ( k  e.  B  |->  C ) )  e. 
_V
7877a1i 11 . . . . . . . . . . 11  |-  ( x  e.  A  ->  (Σ^ `  (
k  e.  B  |->  C ) )  e.  _V )
79 eqid 2420 . . . . . . . . . . . 12  |-  ( x  e.  A  |->  (Σ^ `  ( k  e.  B  |->  C ) ) )  =  ( x  e.  A  |->  (Σ^ `  ( k  e.  B  |->  C ) ) )
8079elrnmpt1 5095 . . . . . . . . . . 11  |-  ( ( x  e.  A  /\  (Σ^ `  ( k  e.  B  |->  C ) )  e. 
_V )  ->  (Σ^ `  (
k  e.  B  |->  C ) )  e.  ran  ( x  e.  A  |->  (Σ^ `  ( k  e.  B  |->  C ) ) ) )
8176, 78, 80syl2anc 665 . . . . . . . . . 10  |-  ( x  e.  A  ->  (Σ^ `  (
k  e.  B  |->  C ) )  e.  ran  ( x  e.  A  |->  (Σ^ `  ( k  e.  B  |->  C ) ) ) )
8281adantr 466 . . . . . . . . 9  |-  ( ( x  e.  A  /\  (Σ^ `  ( k  e.  B  |->  C ) )  = +oo )  ->  (Σ^ `  (
k  e.  B  |->  C ) )  e.  ran  ( x  e.  A  |->  (Σ^ `  ( k  e.  B  |->  C ) ) ) )
8333, 82eqeltrd 2508 . . . . . . . 8  |-  ( ( x  e.  A  /\  (Σ^ `  ( k  e.  B  |->  C ) )  = +oo )  -> +oo  e.  ran  ( x  e.  A  |->  (Σ^ `  ( k  e.  B  |->  C ) ) ) )
84833adant1 1023 . . . . . . 7  |-  ( (
ph  /\  x  e.  A  /\  (Σ^ `  ( k  e.  B  |->  C ) )  = +oo )  -> +oo  e.  ran  ( x  e.  A  |->  (Σ^ `  ( k  e.  B  |->  C ) ) ) )
8543, 75, 84sge0pnfval 37970 . . . . . 6  |-  ( (
ph  /\  x  e.  A  /\  (Σ^ `  ( k  e.  B  |->  C ) )  = +oo )  ->  (Σ^ `  (
x  e.  A  |->  (Σ^ `  (
k  e.  B  |->  C ) ) ) )  = +oo )
8642, 85eqtr4d 2464 . . . . 5  |-  ( (
ph  /\  x  e.  A  /\  (Σ^ `  ( k  e.  B  |->  C ) )  = +oo )  ->  (Σ^ `  (
k  e.  U_ x  e.  A  B  |->  C ) )  =  (Σ^ `  (
x  e.  A  |->  (Σ^ `  (
k  e.  B  |->  C ) ) ) ) )
87863exp 1204 . . . 4  |-  ( ph  ->  ( x  e.  A  ->  ( (Σ^ `  ( k  e.  B  |->  C ) )  = +oo  ->  (Σ^ `  ( k  e.  U_ x  e.  A  B  |->  C ) )  =  (Σ^ `  ( x  e.  A  |->  (Σ^ `  ( k  e.  B  |->  C ) ) ) ) ) ) )
881, 9, 87rexlimd 2907 . . 3  |-  ( ph  ->  ( E. x  e.  A  (Σ^ `  ( k  e.  B  |->  C ) )  = +oo  ->  (Σ^ `  ( k  e.  U_ x  e.  A  B  |->  C ) )  =  (Σ^ `  ( x  e.  A  |->  (Σ^ `  ( k  e.  B  |->  C ) ) ) ) ) )
8988imp 430 . 2  |-  ( (
ph  /\  E. x  e.  A  (Σ^ `  ( k  e.  B  |->  C ) )  = +oo )  ->  (Σ^ `  (
k  e.  U_ x  e.  A  B  |->  C ) )  =  (Σ^ `  (
x  e.  A  |->  (Σ^ `  (
k  e.  B  |->  C ) ) ) ) )
90 simpl 458 . . 3  |-  ( (
ph  /\  -.  E. x  e.  A  (Σ^ `  ( k  e.  B  |->  C ) )  = +oo )  ->  ph )
91 ralnex 2869 . . . . . . 7  |-  ( A. x  e.  A  -.  (Σ^ `  ( k  e.  B  |->  C ) )  = +oo  <->  -.  E. x  e.  A  (Σ^ `  ( k  e.  B  |->  C ) )  = +oo )
9291bicomi 205 . . . . . 6  |-  ( -. 
E. x  e.  A  (Σ^ `  ( k  e.  B  |->  C ) )  = +oo  <->  A. x  e.  A  -.  (Σ^ `  ( k  e.  B  |->  C ) )  = +oo )
93 df-ne 2618 . . . . . . . 8  |-  ( (Σ^ `  (
k  e.  B  |->  C ) )  =/= +oo  <->  -.  (Σ^ `  ( k  e.  B  |->  C ) )  = +oo )
9493bicomi 205 . . . . . . 7  |-  ( -.  (Σ^ `  ( k  e.  B  |->  C ) )  = +oo  <->  (Σ^ `  ( k  e.  B  |->  C ) )  =/= +oo )
9594ralbii 2854 . . . . . 6  |-  ( A. x  e.  A  -.  (Σ^ `  ( k  e.  B  |->  C ) )  = +oo  <->  A. x  e.  A  (Σ^ `  ( k  e.  B  |->  C ) )  =/= +oo )
9692, 95bitri 252 . . . . 5  |-  ( -. 
E. x  e.  A  (Σ^ `  ( k  e.  B  |->  C ) )  = +oo  <->  A. x  e.  A  (Σ^ `  ( k  e.  B  |->  C ) )  =/= +oo )
9796biimpi 197 . . . 4  |-  ( -. 
E. x  e.  A  (Σ^ `  ( k  e.  B  |->  C ) )  = +oo  ->  A. x  e.  A  (Σ^ `  ( k  e.  B  |->  C ) )  =/= +oo )
9897adantl 467 . . 3  |-  ( (
ph  /\  -.  E. x  e.  A  (Σ^ `  ( k  e.  B  |->  C ) )  = +oo )  ->  A. x  e.  A  (Σ^ `  ( k  e.  B  |->  C ) )  =/= +oo )
9910adantr 466 . . . . 5  |-  ( (
ph  /\  A. x  e.  A  (Σ^ `  ( k  e.  B  |->  C ) )  =/= +oo )  ->  A  e.  V )
100 nfcv 2582 . . . . . . . . 9  |-  F/_ x W
10145, 100nfel 2595 . . . . . . . 8  |-  F/ x [_ y  /  x ]_ B  e.  W
10244, 101nfim 1975 . . . . . . 7  |-  F/ x
( ( ph  /\  y  e.  A )  ->  [_ y  /  x ]_ B  e.  W
)
10351eleq1d 2489 . . . . . . . 8  |-  ( x  =  y  ->  ( B  e.  W  <->  [_ y  /  x ]_ B  e.  W
) )
10450, 103imbi12d 321 . . . . . . 7  |-  ( x  =  y  ->  (
( ( ph  /\  x  e.  A )  ->  B  e.  W )  <-> 
( ( ph  /\  y  e.  A )  ->  [_ y  /  x ]_ B  e.  W
) ) )
105102, 104, 11chvar 2066 . . . . . 6  |-  ( (
ph  /\  y  e.  A )  ->  [_ y  /  x ]_ B  e.  W )
106105adantlr 719 . . . . 5  |-  ( ( ( ph  /\  A. x  e.  A  (Σ^ `  (
k  e.  B  |->  C ) )  =/= +oo )  /\  y  e.  A
)  ->  [_ y  /  x ]_ B  e.  W
)
107 sge0iunmpt.dj . . . . . . 7  |-  ( ph  -> Disj  x  e.  A  B
)
108 nfcv 2582 . . . . . . . 8  |-  F/_ y B
109108, 45, 51cbvdisj 4398 . . . . . . 7  |-  (Disj  x  e.  A  B  <-> Disj  y  e.  A  [_ y  /  x ]_ B )
110107, 109sylib 199 . . . . . 6  |-  ( ph  -> Disj  y  e.  A  [_ y  /  x ]_ B )
111110adantr 466 . . . . 5  |-  ( (
ph  /\  A. x  e.  A  (Σ^ `  ( k  e.  B  |->  C ) )  =/= +oo )  -> Disj  y  e.  A  [_ y  /  x ]_ B )
112 nfv 1751 . . . . . . . 8  |-  F/ k ( ph  /\  y  e.  A  /\  j  e.  [_ y  /  x ]_ B )
113 nfcsb1v 3408 . . . . . . . . 9  |-  F/_ k [_ j  /  k ]_ C
114113nfel1 2598 . . . . . . . 8  |-  F/ k
[_ j  /  k ]_ C  e.  (
0 [,] +oo )
115112, 114nfim 1975 . . . . . . 7  |-  F/ k ( ( ph  /\  y  e.  A  /\  j  e.  [_ y  /  x ]_ B )  ->  [_ j  /  k ]_ C  e.  (
0 [,] +oo )
)
116 eleq1 2492 . . . . . . . . 9  |-  ( k  =  j  ->  (
k  e.  [_ y  /  x ]_ B  <->  j  e.  [_ y  /  x ]_ B ) )
1171163anbi3d 1341 . . . . . . . 8  |-  ( k  =  j  ->  (
( ph  /\  y  e.  A  /\  k  e.  [_ y  /  x ]_ B )  <->  ( ph  /\  y  e.  A  /\  j  e.  [_ y  /  x ]_ B ) ) )
118 csbeq1a 3401 . . . . . . . . 9  |-  ( k  =  j  ->  C  =  [_ j  /  k ]_ C )
119118eleq1d 2489 . . . . . . . 8  |-  ( k  =  j  ->  ( C  e.  ( 0 [,] +oo )  <->  [_ j  / 
k ]_ C  e.  ( 0 [,] +oo )
) )
120117, 119imbi12d 321 . . . . . . 7  |-  ( k  =  j  ->  (
( ( ph  /\  y  e.  A  /\  k  e.  [_ y  /  x ]_ B )  ->  C  e.  ( 0 [,] +oo ) )  <-> 
( ( ph  /\  y  e.  A  /\  j  e.  [_ y  /  x ]_ B )  ->  [_ j  /  k ]_ C  e.  (
0 [,] +oo )
) ) )
121 nfv 1751 . . . . . . . . . 10  |-  F/ x  y  e.  A
12218, 45nfel 2595 . . . . . . . . . 10  |-  F/ x  k  e.  [_ y  /  x ]_ B
1231, 121, 122nf3an 1985 . . . . . . . . 9  |-  F/ x
( ph  /\  y  e.  A  /\  k  e.  [_ y  /  x ]_ B )
124123, 21nfim 1975 . . . . . . . 8  |-  F/ x
( ( ph  /\  y  e.  A  /\  k  e.  [_ y  /  x ]_ B )  ->  C  e.  ( 0 [,] +oo ) )
12551eleq2d 2490 . . . . . . . . . 10  |-  ( x  =  y  ->  (
k  e.  B  <->  k  e.  [_ y  /  x ]_ B ) )
12649, 1253anbi23d 1338 . . . . . . . . 9  |-  ( x  =  y  ->  (
( ph  /\  x  e.  A  /\  k  e.  B )  <->  ( ph  /\  y  e.  A  /\  k  e.  [_ y  /  x ]_ B ) ) )
127126imbi1d 318 . . . . . . . 8  |-  ( x  =  y  ->  (
( ( ph  /\  x  e.  A  /\  k  e.  B )  ->  C  e.  ( 0 [,] +oo ) )  <-> 
( ( ph  /\  y  e.  A  /\  k  e.  [_ y  /  x ]_ B )  ->  C  e.  ( 0 [,] +oo ) ) ) )
128124, 127, 22chvar 2066 . . . . . . 7  |-  ( (
ph  /\  y  e.  A  /\  k  e.  [_ y  /  x ]_ B
)  ->  C  e.  ( 0 [,] +oo ) )
129115, 120, 128chvar 2066 . . . . . 6  |-  ( (
ph  /\  y  e.  A  /\  j  e.  [_ y  /  x ]_ B
)  ->  [_ j  / 
k ]_ C  e.  ( 0 [,] +oo )
)
1301293adant1r 1257 . . . . 5  |-  ( ( ( ph  /\  A. x  e.  A  (Σ^ `  (
k  e.  B  |->  C ) )  =/= +oo )  /\  y  e.  A  /\  j  e.  [_ y  /  x ]_ B )  ->  [_ j  /  k ]_ C  e.  (
0 [,] +oo )
)
131 simpr 462 . . . . . . . . 9  |-  ( ( A. x  e.  A  (Σ^ `  ( k  e.  B  |->  C ) )  =/= +oo  /\  y  e.  A
)  ->  y  e.  A )
132 simpl 458 . . . . . . . . 9  |-  ( ( A. x  e.  A  (Σ^ `  ( k  e.  B  |->  C ) )  =/= +oo  /\  y  e.  A
)  ->  A. x  e.  A  (Σ^ `  ( k  e.  B  |->  C ) )  =/= +oo )
133 simpl 458 . . . . . . . . . 10  |-  ( ( y  e.  A  /\  A. x  e.  A  (Σ^ `  (
k  e.  B  |->  C ) )  =/= +oo )  ->  y  e.  A
)
134 simpr 462 . . . . . . . . . 10  |-  ( ( y  e.  A  /\  A. x  e.  A  (Σ^ `  (
k  e.  B  |->  C ) )  =/= +oo )  ->  A. x  e.  A  (Σ^ `  ( k  e.  B  |->  C ) )  =/= +oo )
135 nfcv 2582 . . . . . . . . . . . . . 14  |-  F/_ x [_ j  /  k ]_ C
13645, 135nfmpt 4506 . . . . . . . . . . . . 13  |-  F/_ x
( j  e.  [_ y  /  x ]_ B  |-> 
[_ j  /  k ]_ C )
1372, 136nffv 5880 . . . . . . . . . . . 12  |-  F/_ x
(Σ^ `  ( j  e.  [_ y  /  x ]_ B  |-> 
[_ j  /  k ]_ C ) )
138 nfcv 2582 . . . . . . . . . . . 12  |-  F/_ x +oo
139137, 138nfne 2754 . . . . . . . . . . 11  |-  F/ x
(Σ^ `  ( j  e.  [_ y  /  x ]_ B  |-> 
[_ j  /  k ]_ C ) )  =/= +oo
140 nfcv 2582 . . . . . . . . . . . . . . . 16  |-  F/_ j C
141140, 113, 118cbvmpt 4509 . . . . . . . . . . . . . . 15  |-  ( k  e.  [_ y  /  x ]_ B  |->  C )  =  ( j  e. 
[_ y  /  x ]_ B  |->  [_ j  /  k ]_ C
)
142141a1i 11 . . . . . . . . . . . . . 14  |-  ( x  =  y  ->  (
k  e.  [_ y  /  x ]_ B  |->  C )  =  ( j  e.  [_ y  /  x ]_ B  |->  [_ j  /  k ]_ C
) )
14361, 142eqtrd 2461 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  (
k  e.  B  |->  C )  =  ( j  e.  [_ y  /  x ]_ B  |->  [_ j  /  k ]_ C
) )
144143fveq2d 5877 . . . . . . . . . . . 12  |-  ( x  =  y  ->  (Σ^ `  (
k  e.  B  |->  C ) )  =  (Σ^ `  (
j  e.  [_ y  /  x ]_ B  |->  [_ j  /  k ]_ C
) ) )
145144neeq1d 2699 . . . . . . . . . . 11  |-  ( x  =  y  ->  (
(Σ^ `  ( k  e.  B  |->  C ) )  =/= +oo 
<->  (Σ^ `  ( j  e.  [_ y  /  x ]_ B  |-> 
[_ j  /  k ]_ C ) )  =/= +oo ) )
146139, 145rspc 3173 . . . . . . . . . 10  |-  ( y  e.  A  ->  ( A. x  e.  A  (Σ^ `  ( k  e.  B  |->  C ) )  =/= +oo  ->  (Σ^ `  ( j  e.  [_ y  /  x ]_ B  |-> 
[_ j  /  k ]_ C ) )  =/= +oo ) )
147133, 134, 146sylc 62 . . . . . . . . 9  |-  ( ( y  e.  A  /\  A. x  e.  A  (Σ^ `  (
k  e.  B  |->  C ) )  =/= +oo )  ->  (Σ^ `  ( j  e.  [_ y  /  x ]_ B  |-> 
[_ j  /  k ]_ C ) )  =/= +oo )
148131, 132, 147syl2anc 665 . . . . . . . 8  |-  ( ( A. x  e.  A  (Σ^ `  ( k  e.  B  |->  C ) )  =/= +oo  /\  y  e.  A
)  ->  (Σ^ `  ( j  e.  [_ y  /  x ]_ B  |-> 
[_ j  /  k ]_ C ) )  =/= +oo )
149148neneqd 2623 . . . . . . 7  |-  ( ( A. x  e.  A  (Σ^ `  ( k  e.  B  |->  C ) )  =/= +oo  /\  y  e.  A
)  ->  -.  (Σ^ `  (
j  e.  [_ y  /  x ]_ B  |->  [_ j  /  k ]_ C
) )  = +oo )
150149adantll 718 . . . . . 6  |-  ( ( ( ph  /\  A. x  e.  A  (Σ^ `  (
k  e.  B  |->  C ) )  =/= +oo )  /\  y  e.  A
)  ->  -.  (Σ^ `  (
j  e.  [_ y  /  x ]_ B  |->  [_ j  /  k ]_ C
) )  = +oo )
1511293expa 1205 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  A )  /\  j  e.  [_ y  /  x ]_ B )  ->  [_ j  /  k ]_ C  e.  ( 0 [,] +oo ) )
152 eqid 2420 . . . . . . . . 9  |-  ( j  e.  [_ y  /  x ]_ B  |->  [_ j  /  k ]_ C
)  =  ( j  e.  [_ y  /  x ]_ B  |->  [_ j  /  k ]_ C
)
153151, 152fmptd 6053 . . . . . . . 8  |-  ( (
ph  /\  y  e.  A )  ->  (
j  e.  [_ y  /  x ]_ B  |->  [_ j  /  k ]_ C
) : [_ y  /  x ]_ B --> ( 0 [,] +oo ) )
154153adantlr 719 . . . . . . 7  |-  ( ( ( ph  /\  A. x  e.  A  (Σ^ `  (
k  e.  B  |->  C ) )  =/= +oo )  /\  y  e.  A
)  ->  ( j  e.  [_ y  /  x ]_ B  |->  [_ j  /  k ]_ C
) : [_ y  /  x ]_ B --> ( 0 [,] +oo ) )
155106, 154sge0repnf 37983 . . . . . 6  |-  ( ( ( ph  /\  A. x  e.  A  (Σ^ `  (
k  e.  B  |->  C ) )  =/= +oo )  /\  y  e.  A
)  ->  ( (Σ^ `  (
j  e.  [_ y  /  x ]_ B  |->  [_ j  /  k ]_ C
) )  e.  RR  <->  -.  (Σ^ `  ( j  e.  [_ y  /  x ]_ B  |-> 
[_ j  /  k ]_ C ) )  = +oo ) )
156150, 155mpbird 235 . . . . 5  |-  ( ( ( ph  /\  A. x  e.  A  (Σ^ `  (
k  e.  B  |->  C ) )  =/= +oo )  /\  y  e.  A
)  ->  (Σ^ `  ( j  e.  [_ y  /  x ]_ B  |-> 
[_ j  /  k ]_ C ) )  e.  RR )
157140, 113, 118cbvmpt 4509 . . . . . . . . 9  |-  ( k  e.  U_ x  e.  A  B  |->  C )  =  ( j  e. 
U_ x  e.  A  B  |->  [_ j  /  k ]_ C )
158108, 45, 51cbviun 4330 . . . . . . . . . 10  |-  U_ x  e.  A  B  =  U_ y  e.  A  [_ y  /  x ]_ B
159158mpteq1i 37290 . . . . . . . . 9  |-  ( j  e.  U_ x  e.  A  B  |->  [_ j  /  k ]_ C
)  =  ( j  e.  U_ y  e.  A  [_ y  /  x ]_ B  |->  [_ j  /  k ]_ C
)
160157, 159eqtri 2449 . . . . . . . 8  |-  ( k  e.  U_ x  e.  A  B  |->  C )  =  ( j  e. 
U_ y  e.  A  [_ y  /  x ]_ B  |->  [_ j  /  k ]_ C )
161160fveq2i 5876 . . . . . . 7  |-  (Σ^ `  ( k  e.  U_ x  e.  A  B  |->  C ) )  =  (Σ^ `  ( j  e.  U_ y  e.  A  [_ y  /  x ]_ B  |->  [_ j  /  k ]_ C
) )
162161, 29syl5eqelr 2513 . . . . . 6  |-  ( ph  ->  (Σ^ `  ( j  e.  U_ y  e.  A  [_ y  /  x ]_ B  |->  [_ j  /  k ]_ C
) )  e.  RR* )
163162adantr 466 . . . . 5  |-  ( (
ph  /\  A. x  e.  A  (Σ^ `  ( k  e.  B  |->  C ) )  =/= +oo )  ->  (Σ^ `  ( j  e.  U_ y  e.  A  [_ y  /  x ]_ B  |->  [_ j  /  k ]_ C
) )  e.  RR* )
16470, 137, 144cbvmpt 4509 . . . . . . . 8  |-  ( x  e.  A  |->  (Σ^ `  ( k  e.  B  |->  C ) ) )  =  ( y  e.  A  |->  (Σ^ `  ( j  e.  [_ y  /  x ]_ B  |-> 
[_ j  /  k ]_ C ) ) )
165164fveq2i 5876 . . . . . . 7  |-  (Σ^ `  ( x  e.  A  |->  (Σ^ `  ( k  e.  B  |->  C ) ) ) )  =  (Σ^ `  ( y  e.  A  |->  (Σ^ `  ( j  e.  [_ y  /  x ]_ B  |-> 
[_ j  /  k ]_ C ) ) ) )
16611, 66sge0cl 37978 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  (Σ^ `  (
k  e.  B  |->  C ) )  e.  ( 0 [,] +oo )
)
167166, 79fmptd 6053 . . . . . . . 8  |-  ( ph  ->  ( x  e.  A  |->  (Σ^ `  ( k  e.  B  |->  C ) ) ) : A --> ( 0 [,] +oo ) )
16810, 167sge0xrcl 37982 . . . . . . 7  |-  ( ph  ->  (Σ^ `  ( x  e.  A  |->  (Σ^ `  ( k  e.  B  |->  C ) ) ) )  e.  RR* )
169165, 168syl5eqelr 2513 . . . . . 6  |-  ( ph  ->  (Σ^ `  ( y  e.  A  |->  (Σ^ `  ( j  e.  [_ y  /  x ]_ B  |-> 
[_ j  /  k ]_ C ) ) ) )  e.  RR* )
170169adantr 466 . . . . 5  |-  ( (
ph  /\  A. x  e.  A  (Σ^ `  ( k  e.  B  |->  C ) )  =/= +oo )  ->  (Σ^ `  ( y  e.  A  |->  (Σ^ `  ( j  e.  [_ y  /  x ]_ B  |-> 
[_ j  /  k ]_ C ) ) ) )  e.  RR* )
171 eliun 4298 . . . . . . . . . 10  |-  ( j  e.  U_ y  e.  A  [_ y  /  x ]_ B  <->  E. y  e.  A  j  e.  [_ y  /  x ]_ B )
172171biimpi 197 . . . . . . . . 9  |-  ( j  e.  U_ y  e.  A  [_ y  /  x ]_ B  ->  E. y  e.  A  j  e.  [_ y  /  x ]_ B )
173172adantl 467 . . . . . . . 8  |-  ( (
ph  /\  j  e.  U_ y  e.  A  [_ y  /  x ]_ B
)  ->  E. y  e.  A  j  e.  [_ y  /  x ]_ B )
174 nfv 1751 . . . . . . . . . 10  |-  F/ y
ph
175 nfcv 2582 . . . . . . . . . . 11  |-  F/_ y
j
176 nfiu1 4323 . . . . . . . . . . 11  |-  F/_ y U_ y  e.  A  [_ y  /  x ]_ B
177175, 176nfel 2595 . . . . . . . . . 10  |-  F/ y  j  e.  U_ y  e.  A  [_ y  /  x ]_ B
178174, 177nfan 1983 . . . . . . . . 9  |-  F/ y ( ph  /\  j  e.  U_ y  e.  A  [_ y  /  x ]_ B )
179 nfv 1751 . . . . . . . . 9  |-  F/ y
[_ j  /  k ]_ C  e.  (
0 [,] +oo )
180151exp31 607 . . . . . . . . . 10  |-  ( ph  ->  ( y  e.  A  ->  ( j  e.  [_ y  /  x ]_ B  ->  [_ j  /  k ]_ C  e.  (
0 [,] +oo )
) ) )
181180adantr 466 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  U_ y  e.  A  [_ y  /  x ]_ B
)  ->  ( y  e.  A  ->  ( j  e.  [_ y  /  x ]_ B  ->  [_ j  /  k ]_ C  e.  ( 0 [,] +oo ) ) ) )
182178, 179, 181rexlimd 2907 . . . . . . . 8  |-  ( (
ph  /\  j  e.  U_ y  e.  A  [_ y  /  x ]_ B
)  ->  ( E. y  e.  A  j  e.  [_ y  /  x ]_ B  ->  [_ j  /  k ]_ C  e.  ( 0 [,] +oo ) ) )
183173, 182mpd 15 . . . . . . 7  |-  ( (
ph  /\  j  e.  U_ y  e.  A  [_ y  /  x ]_ B
)  ->  [_ j  / 
k ]_ C  e.  ( 0 [,] +oo )
)
184 eqid 2420 . . . . . . 7  |-  ( j  e.  U_ y  e.  A  [_ y  /  x ]_ B  |->  [_ j  /  k ]_ C
)  =  ( j  e.  U_ y  e.  A  [_ y  /  x ]_ B  |->  [_ j  /  k ]_ C
)
185183, 184fmptd 6053 . . . . . 6  |-  ( ph  ->  ( j  e.  U_ y  e.  A  [_ y  /  x ]_ B  |->  [_ j  /  k ]_ C
) : U_ y  e.  A  [_ y  /  x ]_ B --> ( 0 [,] +oo ) )
186185adantr 466 . . . . 5  |-  ( (
ph  /\  A. x  e.  A  (Σ^ `  ( k  e.  B  |->  C ) )  =/= +oo )  ->  ( j  e.  U_ y  e.  A  [_ y  /  x ]_ B  |->  [_ j  /  k ]_ C
) : U_ y  e.  A  [_ y  /  x ]_ B --> ( 0 [,] +oo ) )
187158, 14syl5eqelr 2513 . . . . . 6  |-  ( ph  ->  U_ y  e.  A  [_ y  /  x ]_ B  e.  _V )
188187adantr 466 . . . . 5  |-  ( (
ph  /\  A. x  e.  A  (Σ^ `  ( k  e.  B  |->  C ) )  =/= +oo )  ->  U_ y  e.  A  [_ y  /  x ]_ B  e.  _V )
18999, 106, 111, 130, 156, 163, 170, 186, 188sge0iunmptlemre 38012 . . . 4  |-  ( (
ph  /\  A. x  e.  A  (Σ^ `  ( k  e.  B  |->  C ) )  =/= +oo )  ->  (Σ^ `  ( j  e.  U_ y  e.  A  [_ y  /  x ]_ B  |->  [_ j  /  k ]_ C
) )  =  (Σ^ `  (
y  e.  A  |->  (Σ^ `  (
j  e.  [_ y  /  x ]_ B  |->  [_ j  /  k ]_ C
) ) ) ) )
190161a1i 11 . . . 4  |-  ( (
ph  /\  A. x  e.  A  (Σ^ `  ( k  e.  B  |->  C ) )  =/= +oo )  ->  (Σ^ `  ( k  e.  U_ x  e.  A  B  |->  C ) )  =  (Σ^ `  ( j  e.  U_ y  e.  A  [_ y  /  x ]_ B  |->  [_ j  /  k ]_ C
) ) )
191165a1i 11 . . . 4  |-  ( (
ph  /\  A. x  e.  A  (Σ^ `  ( k  e.  B  |->  C ) )  =/= +oo )  ->  (Σ^ `  ( x  e.  A  |->  (Σ^ `  ( k  e.  B  |->  C ) ) ) )  =  (Σ^ `  ( y  e.  A  |->  (Σ^ `  ( j  e.  [_ y  /  x ]_ B  |-> 
[_ j  /  k ]_ C ) ) ) ) )
192189, 190, 1913eqtr4d 2471 . . 3  |-  ( (
ph  /\  A. x  e.  A  (Σ^ `  ( k  e.  B  |->  C ) )  =/= +oo )  ->  (Σ^ `  ( k  e.  U_ x  e.  A  B  |->  C ) )  =  (Σ^ `  ( x  e.  A  |->  (Σ^ `  ( k  e.  B  |->  C ) ) ) ) )
19390, 98, 192syl2anc 665 . 2  |-  ( (
ph  /\  -.  E. x  e.  A  (Σ^ `  ( k  e.  B  |->  C ) )  = +oo )  ->  (Σ^ `  (
k  e.  U_ x  e.  A  B  |->  C ) )  =  (Σ^ `  (
x  e.  A  |->  (Σ^ `  (
k  e.  B  |->  C ) ) ) ) )
19489, 193pm2.61dan 798 1  |-  ( ph  ->  (Σ^ `  ( k  e.  U_ x  e.  A  B  |->  C ) )  =  (Σ^ `  ( x  e.  A  |->  (Σ^ `  ( k  e.  B  |->  C ) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1867    =/= wne 2616   A.wral 2773   E.wrex 2774   _Vcvv 3078   [_csb 3392    C_ wss 3433   U_ciun 4293  Disj wdisj 4388   class class class wbr 4417    |-> cmpt 4476   ran crn 4847   -->wf 5589   ` cfv 5593  (class class class)co 6297   RRcr 9534   0cc0 9535   +oocpnf 9668   RR*cxr 9670    <_ cle 9672   [,]cicc 11634  Σ^csumge0 37959
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-rep 4530  ax-sep 4540  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6589  ax-inf2 8144  ax-ac2 8889  ax-cnex 9591  ax-resscn 9592  ax-1cn 9593  ax-icn 9594  ax-addcl 9595  ax-addrcl 9596  ax-mulcl 9597  ax-mulrcl 9598  ax-mulcom 9599  ax-addass 9600  ax-mulass 9601  ax-distr 9602  ax-i2m1 9603  ax-1ne0 9604  ax-1rid 9605  ax-rnegex 9606  ax-rrecex 9607  ax-cnre 9608  ax-pre-lttri 9609  ax-pre-lttrn 9610  ax-pre-ltadd 9611  ax-pre-mulgt0 9612  ax-pre-sup 9613
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-nel 2619  df-ral 2778  df-rex 2779  df-reu 2780  df-rmo 2781  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-pss 3449  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-tp 3998  df-op 4000  df-uni 4214  df-int 4250  df-iun 4295  df-disj 4389  df-br 4418  df-opab 4477  df-mpt 4478  df-tr 4513  df-eprel 4757  df-id 4761  df-po 4767  df-so 4768  df-fr 4805  df-se 4806  df-we 4807  df-xp 4852  df-rel 4853  df-cnv 4854  df-co 4855  df-dm 4856  df-rn 4857  df-res 4858  df-ima 4859  df-pred 5391  df-ord 5437  df-on 5438  df-lim 5439  df-suc 5440  df-iota 5557  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-isom 5602  df-riota 6259  df-ov 6300  df-oprab 6301  df-mpt2 6302  df-om 6699  df-1st 6799  df-2nd 6800  df-wrecs 7028  df-recs 7090  df-rdg 7128  df-1o 7182  df-oadd 7186  df-er 7363  df-map 7474  df-en 7570  df-dom 7571  df-sdom 7572  df-fin 7573  df-sup 7954  df-oi 8023  df-card 8370  df-acn 8373  df-ac 8543  df-pnf 9673  df-mnf 9674  df-xr 9675  df-ltxr 9676  df-le 9677  df-sub 9858  df-neg 9859  df-div 10266  df-nn 10606  df-2 10664  df-3 10665  df-n0 10866  df-z 10934  df-uz 11156  df-rp 11299  df-xadd 11406  df-ico 11637  df-icc 11638  df-fz 11779  df-fzo 11910  df-seq 12207  df-exp 12266  df-hash 12509  df-cj 13141  df-re 13142  df-im 13143  df-sqrt 13277  df-abs 13278  df-clim 13530  df-sum 13731  df-sumge0 37960
This theorem is referenced by:  sge0iun  38016
  Copyright terms: Public domain W3C validator