Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  voliunnfl Structured version   Unicode version

Theorem voliunnfl 26286
Description: voliun 19479 is incompatible with the Feferman-Levy model; in that model, therefore, the Lebesgue measure as we've defined it isn't actually a measure. (Contributed by Brendan Leahy, 16-Dec-2017.)
Hypotheses
Ref Expression
voliunnfl.1  |-  S  =  seq  1 (  +  ,  G )
voliunnfl.2  |-  G  =  ( n  e.  NN  |->  ( vol `  ( f `
 n ) ) )
voliunnfl.3  |-  ( ( A. n  e.  NN  ( ( f `  n )  e.  dom  vol 
/\  ( vol `  (
f `  n )
)  e.  RR )  /\ Disj  n  e.  NN ( f `  n ) )  ->  ( vol ` 
U_ n  e.  NN  ( f `  n
) )  =  sup ( ran  S ,  RR* ,  <  ) )
Assertion
Ref Expression
voliunnfl  |-  ( ( A  ~<_  NN  /\  A. x  e.  A  x  ~<_  NN )  ->  U. A  =/=  RR )
Distinct variable group:    f, n, x, A
Allowed substitution hints:    S( x, f, n)    G( x, f, n)

Proof of Theorem voliunnfl
Dummy variables  g  m  l are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 unieq 4048 . . . . . . . . 9  |-  ( A  =  (/)  ->  U. A  =  U. (/) )
2 uni0 4066 . . . . . . . . 9  |-  U. (/)  =  (/)
31, 2syl6eq 2490 . . . . . . . 8  |-  ( A  =  (/)  ->  U. A  =  (/) )
43fveq2d 5761 . . . . . . 7  |-  ( A  =  (/)  ->  ( vol `  U. A )  =  ( vol `  (/) ) )
5 0mbl 19465 . . . . . . . . 9  |-  (/)  e.  dom  vol
6 mblvol 19457 . . . . . . . . 9  |-  ( (/)  e.  dom  vol  ->  ( vol `  (/) )  =  ( vol * `  (/) ) )
75, 6ax-mp 5 . . . . . . . 8  |-  ( vol `  (/) )  =  ( vol * `  (/) )
8 ovol0 19420 . . . . . . . 8  |-  ( vol
* `  (/) )  =  0
97, 8eqtri 2462 . . . . . . 7  |-  ( vol `  (/) )  =  0
104, 9syl6req 2491 . . . . . 6  |-  ( A  =  (/)  ->  0  =  ( vol `  U. A ) )
1110a1d 24 . . . . 5  |-  ( A  =  (/)  ->  ( ( A  ~<_  NN  /\  ( A. x  e.  A  x  ~<_  NN  /\  U. A  C_  RR ) )  -> 
0  =  ( vol `  U. A ) ) )
12 reldom 7144 . . . . . . . . . . 11  |-  Rel  ~<_
1312brrelexi 4947 . . . . . . . . . 10  |-  ( A  ~<_  NN  ->  A  e.  _V )
14 0sdomg 7265 . . . . . . . . . 10  |-  ( A  e.  _V  ->  ( (/) 
~<  A  <->  A  =/=  (/) ) )
1513, 14syl 16 . . . . . . . . 9  |-  ( A  ~<_  NN  ->  ( (/)  ~<  A  <->  A  =/=  (/) ) )
1615biimparc 475 . . . . . . . 8  |-  ( ( A  =/=  (/)  /\  A  ~<_  NN )  ->  (/)  ~<  A )
17 fodomr 7287 . . . . . . . 8  |-  ( (
(/)  ~<  A  /\  A  ~<_  NN )  ->  E. g 
g : NN -onto-> A
)
1816, 17sylancom 650 . . . . . . 7  |-  ( ( A  =/=  (/)  /\  A  ~<_  NN )  ->  E. g 
g : NN -onto-> A
)
19 unissb 4069 . . . . . . . . . . . . 13  |-  ( U. A  C_  RR  <->  A. x  e.  A  x  C_  RR )
2019anbi1i 678 . . . . . . . . . . . 12  |-  ( ( U. A  C_  RR  /\ 
A. x  e.  A  x  ~<_  NN )  <->  ( A. x  e.  A  x  C_  RR  /\  A. x  e.  A  x  ~<_  NN ) )
21 r19.26 2844 . . . . . . . . . . . 12  |-  ( A. x  e.  A  (
x  C_  RR  /\  x  ~<_  NN )  <->  ( A. x  e.  A  x  C_  RR  /\ 
A. x  e.  A  x  ~<_  NN ) )
2220, 21bitr4i 245 . . . . . . . . . . 11  |-  ( ( U. A  C_  RR  /\ 
A. x  e.  A  x  ~<_  NN )  <->  A. x  e.  A  ( x  C_  RR  /\  x  ~<_  NN ) )
23 ovolctb2 19419 . . . . . . . . . . . . . 14  |-  ( ( x  C_  RR  /\  x  ~<_  NN )  ->  ( vol
* `  x )  =  0 )
2423ex 425 . . . . . . . . . . . . 13  |-  ( x 
C_  RR  ->  ( x  ~<_  NN  ->  ( vol * `
 x )  =  0 ) )
2524imdistani 673 . . . . . . . . . . . 12  |-  ( ( x  C_  RR  /\  x  ~<_  NN )  ->  ( x 
C_  RR  /\  ( vol * `  x )  =  0 ) )
2625ralimi 2787 . . . . . . . . . . 11  |-  ( A. x  e.  A  (
x  C_  RR  /\  x  ~<_  NN )  ->  A. x  e.  A  ( x  C_  RR  /\  ( vol
* `  x )  =  0 ) )
2722, 26sylbi 189 . . . . . . . . . 10  |-  ( ( U. A  C_  RR  /\ 
A. x  e.  A  x  ~<_  NN )  ->  A. x  e.  A  ( x  C_  RR  /\  ( vol * `  x
)  =  0 ) )
2827ancoms 441 . . . . . . . . 9  |-  ( ( A. x  e.  A  x  ~<_  NN  /\  U. A  C_  RR )  ->  A. x  e.  A  ( x  C_  RR  /\  ( vol
* `  x )  =  0 ) )
29 foima 5687 . . . . . . . . . . . 12  |-  ( g : NN -onto-> A  -> 
( g " NN )  =  A )
3029raleqdv 2916 . . . . . . . . . . 11  |-  ( g : NN -onto-> A  -> 
( A. x  e.  ( g " NN ) ( x  C_  RR  /\  ( vol * `  x )  =  0 )  <->  A. x  e.  A  ( x  C_  RR  /\  ( vol * `  x
)  =  0 ) ) )
31 fofn 5684 . . . . . . . . . . . 12  |-  ( g : NN -onto-> A  -> 
g  Fn  NN )
32 ssid 3353 . . . . . . . . . . . 12  |-  NN  C_  NN
33 sseq1 3355 . . . . . . . . . . . . . 14  |-  ( x  =  ( g `  m )  ->  (
x  C_  RR  <->  ( g `  m )  C_  RR ) )
34 fveq2 5757 . . . . . . . . . . . . . . 15  |-  ( x  =  ( g `  m )  ->  ( vol * `  x )  =  ( vol * `  ( g `  m
) ) )
3534eqeq1d 2450 . . . . . . . . . . . . . 14  |-  ( x  =  ( g `  m )  ->  (
( vol * `  x )  =  0  <-> 
( vol * `  ( g `  m
) )  =  0 ) )
3633, 35anbi12d 693 . . . . . . . . . . . . 13  |-  ( x  =  ( g `  m )  ->  (
( x  C_  RR  /\  ( vol * `  x )  =  0 )  <->  ( ( g `
 m )  C_  RR  /\  ( vol * `  ( g `  m
) )  =  0 ) ) )
3736ralima 6007 . . . . . . . . . . . 12  |-  ( ( g  Fn  NN  /\  NN  C_  NN )  -> 
( A. x  e.  ( g " NN ) ( x  C_  RR  /\  ( vol * `  x )  =  0 )  <->  A. m  e.  NN  ( ( g `  m )  C_  RR  /\  ( vol * `  ( g `  m
) )  =  0 ) ) )
3831, 32, 37sylancl 645 . . . . . . . . . . 11  |-  ( g : NN -onto-> A  -> 
( A. x  e.  ( g " NN ) ( x  C_  RR  /\  ( vol * `  x )  =  0 )  <->  A. m  e.  NN  ( ( g `  m )  C_  RR  /\  ( vol * `  ( g `  m
) )  =  0 ) ) )
3930, 38bitr3d 248 . . . . . . . . . 10  |-  ( g : NN -onto-> A  -> 
( A. x  e.  A  ( x  C_  RR  /\  ( vol * `  x )  =  0 )  <->  A. m  e.  NN  ( ( g `  m )  C_  RR  /\  ( vol * `  ( g `  m
) )  =  0 ) ) )
40 difss 3460 . . . . . . . . . . . . . . . . . 18  |-  ( ( g `  m ) 
\  U_ l  e.  ( 1..^ m ) ( g `  l ) )  C_  ( g `  m )
41 ovolssnul 19414 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( g `  m )  \  U_ l  e.  ( 1..^ m ) ( g `
 l ) ) 
C_  ( g `  m )  /\  (
g `  m )  C_  RR  /\  ( vol
* `  ( g `  m ) )  =  0 )  ->  ( vol * `  ( ( g `  m ) 
\  U_ l  e.  ( 1..^ m ) ( g `  l ) ) )  =  0 )
4240, 41mp3an1 1267 . . . . . . . . . . . . . . . . 17  |-  ( ( ( g `  m
)  C_  RR  /\  ( vol * `  ( g `
 m ) )  =  0 )  -> 
( vol * `  ( ( g `  m )  \  U_ l  e.  ( 1..^ m ) ( g `
 l ) ) )  =  0 )
43 ssdifss 3464 . . . . . . . . . . . . . . . . . 18  |-  ( ( g `  m ) 
C_  RR  ->  ( ( g `  m ) 
\  U_ l  e.  ( 1..^ m ) ( g `  l ) )  C_  RR )
44 nulmbl 19461 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( g `  m )  \  U_ l  e.  ( 1..^ m ) ( g `
 l ) ) 
C_  RR  /\  ( vol * `  ( ( g `  m ) 
\  U_ l  e.  ( 1..^ m ) ( g `  l ) ) )  =  0 )  ->  ( (
g `  m )  \  U_ l  e.  ( 1..^ m ) ( g `  l ) )  e.  dom  vol )
45 mblvol 19457 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) )  e.  dom  vol 
->  ( vol `  (
( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) ) )  =  ( vol * `  ( ( g `  m )  \  U_ l  e.  ( 1..^ m ) ( g `
 l ) ) ) )
4645eqeq1d 2450 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) )  e.  dom  vol 
->  ( ( vol `  (
( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) ) )  =  0  <->  ( vol * `  ( ( g `  m )  \  U_ l  e.  ( 1..^ m ) ( g `
 l ) ) )  =  0 ) )
4746biimpar 473 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( g `  m )  \  U_ l  e.  ( 1..^ m ) ( g `
 l ) )  e.  dom  vol  /\  ( vol * `  (
( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) ) )  =  0 )  ->  ( vol `  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) )  =  0 )
48 0re 9122 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  e.  RR
4947, 48syl6eqel 2530 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( g `  m )  \  U_ l  e.  ( 1..^ m ) ( g `
 l ) )  e.  dom  vol  /\  ( vol * `  (
( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) ) )  =  0 )  ->  ( vol `  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) )  e.  RR )
5049expcom 426 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( vol * `  (
( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) ) )  =  0  ->  ( (
( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) )  e.  dom  vol 
->  ( vol `  (
( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) ) )  e.  RR ) )
5150ancld 538 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( vol * `  (
( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) ) )  =  0  ->  ( (
( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) )  e.  dom  vol 
->  ( ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) )  e.  dom  vol  /\  ( vol `  (
( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) ) )  e.  RR ) ) )
5251adantl 454 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( g `  m )  \  U_ l  e.  ( 1..^ m ) ( g `
 l ) ) 
C_  RR  /\  ( vol * `  ( ( g `  m ) 
\  U_ l  e.  ( 1..^ m ) ( g `  l ) ) )  =  0 )  ->  ( (
( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) )  e.  dom  vol 
->  ( ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) )  e.  dom  vol  /\  ( vol `  (
( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) ) )  e.  RR ) ) )
5344, 52mpd 15 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( g `  m )  \  U_ l  e.  ( 1..^ m ) ( g `
 l ) ) 
C_  RR  /\  ( vol * `  ( ( g `  m ) 
\  U_ l  e.  ( 1..^ m ) ( g `  l ) ) )  =  0 )  ->  ( (
( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) )  e.  dom  vol 
/\  ( vol `  (
( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) ) )  e.  RR ) )
5443, 53sylan 459 . . . . . . . . . . . . . . . . 17  |-  ( ( ( g `  m
)  C_  RR  /\  ( vol * `  ( ( g `  m ) 
\  U_ l  e.  ( 1..^ m ) ( g `  l ) ) )  =  0 )  ->  ( (
( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) )  e.  dom  vol 
/\  ( vol `  (
( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) ) )  e.  RR ) )
5542, 54syldan 458 . . . . . . . . . . . . . . . 16  |-  ( ( ( g `  m
)  C_  RR  /\  ( vol * `  ( g `
 m ) )  =  0 )  -> 
( ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) )  e.  dom  vol  /\  ( vol `  (
( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) ) )  e.  RR ) )
5655ralimi 2787 . . . . . . . . . . . . . . 15  |-  ( A. m  e.  NN  (
( g `  m
)  C_  RR  /\  ( vol * `  ( g `
 m ) )  =  0 )  ->  A. m  e.  NN  ( ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) )  e.  dom  vol  /\  ( vol `  (
( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) ) )  e.  RR ) )
57 fveq2 5757 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  =  n  ->  (
g `  m )  =  ( g `  n ) )
58 oveq2 6118 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( m  =  n  ->  (
1..^ m )  =  ( 1..^ n ) )
5958iuneq1d 4140 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  =  n  ->  U_ l  e.  ( 1..^ m ) ( g `  l
)  =  U_ l  e.  ( 1..^ n ) ( g `  l
) )
6057, 59difeq12d 3452 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  n  ->  (
( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) )  =  ( ( g `  n
)  \  U_ l  e.  ( 1..^ n ) ( g `  l
) ) )
61 eqid 2442 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  e.  NN  |->  ( ( g `  m ) 
\  U_ l  e.  ( 1..^ m ) ( g `  l ) ) )  =  ( m  e.  NN  |->  ( ( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) ) )
62 fvex 5771 . . . . . . . . . . . . . . . . . . . . 21  |-  ( g `
 n )  e. 
_V
63 difexg 4380 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( g `  n )  e.  _V  ->  (
( g `  n
)  \  U_ l  e.  ( 1..^ n ) ( g `  l
) )  e.  _V )
6462, 63ax-mp 5 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( g `  n ) 
\  U_ l  e.  ( 1..^ n ) ( g `  l ) )  e.  _V
6560, 61, 64fvmpt 5835 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  NN  ->  (
( m  e.  NN  |->  ( ( g `  m )  \  U_ l  e.  ( 1..^ m ) ( g `
 l ) ) ) `  n )  =  ( ( g `
 n )  \  U_ l  e.  (
1..^ n ) ( g `  l ) ) )
6665eleq1d 2508 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  NN  ->  (
( ( m  e.  NN  |->  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) ) `  n
)  e.  dom  vol  <->  (
( g `  n
)  \  U_ l  e.  ( 1..^ n ) ( g `  l
) )  e.  dom  vol ) )
6765fveq2d 5761 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  NN  ->  ( vol `  ( ( m  e.  NN  |->  ( ( g `  m ) 
\  U_ l  e.  ( 1..^ m ) ( g `  l ) ) ) `  n
) )  =  ( vol `  ( ( g `  n ) 
\  U_ l  e.  ( 1..^ n ) ( g `  l ) ) ) )
6867eleq1d 2508 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  NN  ->  (
( vol `  (
( m  e.  NN  |->  ( ( g `  m )  \  U_ l  e.  ( 1..^ m ) ( g `
 l ) ) ) `  n ) )  e.  RR  <->  ( vol `  ( ( g `  n )  \  U_ l  e.  ( 1..^ n ) ( g `
 l ) ) )  e.  RR ) )
6966, 68anbi12d 693 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  NN  ->  (
( ( ( m  e.  NN  |->  ( ( g `  m ) 
\  U_ l  e.  ( 1..^ m ) ( g `  l ) ) ) `  n
)  e.  dom  vol  /\  ( vol `  (
( m  e.  NN  |->  ( ( g `  m )  \  U_ l  e.  ( 1..^ m ) ( g `
 l ) ) ) `  n ) )  e.  RR )  <-> 
( ( ( g `
 n )  \  U_ l  e.  (
1..^ n ) ( g `  l ) )  e.  dom  vol  /\  ( vol `  (
( g `  n
)  \  U_ l  e.  ( 1..^ n ) ( g `  l
) ) )  e.  RR ) ) )
7069ralbiia 2743 . . . . . . . . . . . . . . . 16  |-  ( A. n  e.  NN  (
( ( m  e.  NN  |->  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) ) `  n
)  e.  dom  vol  /\  ( vol `  (
( m  e.  NN  |->  ( ( g `  m )  \  U_ l  e.  ( 1..^ m ) ( g `
 l ) ) ) `  n ) )  e.  RR )  <->  A. n  e.  NN  ( ( ( g `
 n )  \  U_ l  e.  (
1..^ n ) ( g `  l ) )  e.  dom  vol  /\  ( vol `  (
( g `  n
)  \  U_ l  e.  ( 1..^ n ) ( g `  l
) ) )  e.  RR ) )
71 fveq2 5757 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  m  ->  (
g `  n )  =  ( g `  m ) )
72 oveq2 6118 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  m  ->  (
1..^ n )  =  ( 1..^ m ) )
7372iuneq1d 4140 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  m  ->  U_ l  e.  ( 1..^ n ) ( g `  l
)  =  U_ l  e.  ( 1..^ m ) ( g `  l
) )
7471, 73difeq12d 3452 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  m  ->  (
( g `  n
)  \  U_ l  e.  ( 1..^ n ) ( g `  l
) )  =  ( ( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) ) )
7574eleq1d 2508 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  m  ->  (
( ( g `  n )  \  U_ l  e.  ( 1..^ n ) ( g `
 l ) )  e.  dom  vol  <->  ( (
g `  m )  \  U_ l  e.  ( 1..^ m ) ( g `  l ) )  e.  dom  vol ) )
7674fveq2d 5761 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  m  ->  ( vol `  ( ( g `
 n )  \  U_ l  e.  (
1..^ n ) ( g `  l ) ) )  =  ( vol `  ( ( g `  m ) 
\  U_ l  e.  ( 1..^ m ) ( g `  l ) ) ) )
7776eleq1d 2508 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  m  ->  (
( vol `  (
( g `  n
)  \  U_ l  e.  ( 1..^ n ) ( g `  l
) ) )  e.  RR  <->  ( vol `  (
( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) ) )  e.  RR ) )
7875, 77anbi12d 693 . . . . . . . . . . . . . . . . 17  |-  ( n  =  m  ->  (
( ( ( g `
 n )  \  U_ l  e.  (
1..^ n ) ( g `  l ) )  e.  dom  vol  /\  ( vol `  (
( g `  n
)  \  U_ l  e.  ( 1..^ n ) ( g `  l
) ) )  e.  RR )  <->  ( (
( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) )  e.  dom  vol 
/\  ( vol `  (
( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) ) )  e.  RR ) ) )
7978cbvralv 2938 . . . . . . . . . . . . . . . 16  |-  ( A. n  e.  NN  (
( ( g `  n )  \  U_ l  e.  ( 1..^ n ) ( g `
 l ) )  e.  dom  vol  /\  ( vol `  ( ( g `  n ) 
\  U_ l  e.  ( 1..^ n ) ( g `  l ) ) )  e.  RR ) 
<-> 
A. m  e.  NN  ( ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) )  e.  dom  vol  /\  ( vol `  (
( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) ) )  e.  RR ) )
8070, 79bitri 242 . . . . . . . . . . . . . . 15  |-  ( A. n  e.  NN  (
( ( m  e.  NN  |->  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) ) `  n
)  e.  dom  vol  /\  ( vol `  (
( m  e.  NN  |->  ( ( g `  m )  \  U_ l  e.  ( 1..^ m ) ( g `
 l ) ) ) `  n ) )  e.  RR )  <->  A. m  e.  NN  ( ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) )  e.  dom  vol  /\  ( vol `  (
( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) ) )  e.  RR ) )
8156, 80sylibr 205 . . . . . . . . . . . . . 14  |-  ( A. m  e.  NN  (
( g `  m
)  C_  RR  /\  ( vol * `  ( g `
 m ) )  =  0 )  ->  A. n  e.  NN  ( ( ( m  e.  NN  |->  ( ( g `  m ) 
\  U_ l  e.  ( 1..^ m ) ( g `  l ) ) ) `  n
)  e.  dom  vol  /\  ( vol `  (
( m  e.  NN  |->  ( ( g `  m )  \  U_ l  e.  ( 1..^ m ) ( g `
 l ) ) ) `  n ) )  e.  RR ) )
82 fveq2 5757 . . . . . . . . . . . . . . . 16  |-  ( n  =  l  ->  (
g `  n )  =  ( g `  l ) )
8382iundisj2 19474 . . . . . . . . . . . . . . 15  |- Disj  n  e.  NN ( ( g `
 n )  \  U_ l  e.  (
1..^ n ) ( g `  l ) )
84 disjeq2 4211 . . . . . . . . . . . . . . . 16  |-  ( A. n  e.  NN  (
( m  e.  NN  |->  ( ( g `  m )  \  U_ l  e.  ( 1..^ m ) ( g `
 l ) ) ) `  n )  =  ( ( g `
 n )  \  U_ l  e.  (
1..^ n ) ( g `  l ) )  ->  (Disj  n  e.  NN ( ( m  e.  NN  |->  ( ( g `  m ) 
\  U_ l  e.  ( 1..^ m ) ( g `  l ) ) ) `  n
)  <-> Disj  n  e.  NN ( ( g `  n
)  \  U_ l  e.  ( 1..^ n ) ( g `  l
) ) ) )
8584, 65mprg 2781 . . . . . . . . . . . . . . 15  |-  (Disj  n  e.  NN ( ( m  e.  NN  |->  ( ( g `  m ) 
\  U_ l  e.  ( 1..^ m ) ( g `  l ) ) ) `  n
)  <-> Disj  n  e.  NN ( ( g `  n
)  \  U_ l  e.  ( 1..^ n ) ( g `  l
) ) )
8683, 85mpbir 202 . . . . . . . . . . . . . 14  |- Disj  n  e.  NN ( ( m  e.  NN  |->  ( ( g `  m ) 
\  U_ l  e.  ( 1..^ m ) ( g `  l ) ) ) `  n
)
87 nnex 10037 . . . . . . . . . . . . . . . . 17  |-  NN  e.  _V
8887mptex 5995 . . . . . . . . . . . . . . . 16  |-  ( m  e.  NN  |->  ( ( g `  m ) 
\  U_ l  e.  ( 1..^ m ) ( g `  l ) ) )  e.  _V
89 fveq1 5756 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f  =  ( m  e.  NN  |->  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) )  ->  (
f `  n )  =  ( ( m  e.  NN  |->  ( ( g `  m ) 
\  U_ l  e.  ( 1..^ m ) ( g `  l ) ) ) `  n
) )
9089eleq1d 2508 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  =  ( m  e.  NN  |->  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) )  ->  (
( f `  n
)  e.  dom  vol  <->  (
( m  e.  NN  |->  ( ( g `  m )  \  U_ l  e.  ( 1..^ m ) ( g `
 l ) ) ) `  n )  e.  dom  vol )
)
9189fveq2d 5761 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f  =  ( m  e.  NN  |->  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) )  ->  ( vol `  ( f `  n ) )  =  ( vol `  (
( m  e.  NN  |->  ( ( g `  m )  \  U_ l  e.  ( 1..^ m ) ( g `
 l ) ) ) `  n ) ) )
9291eleq1d 2508 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  =  ( m  e.  NN  |->  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) )  ->  (
( vol `  (
f `  n )
)  e.  RR  <->  ( vol `  ( ( m  e.  NN  |->  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) ) `  n
) )  e.  RR ) )
9390, 92anbi12d 693 . . . . . . . . . . . . . . . . . . 19  |-  ( f  =  ( m  e.  NN  |->  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) )  ->  (
( ( f `  n )  e.  dom  vol 
/\  ( vol `  (
f `  n )
)  e.  RR )  <-> 
( ( ( m  e.  NN  |->  ( ( g `  m ) 
\  U_ l  e.  ( 1..^ m ) ( g `  l ) ) ) `  n
)  e.  dom  vol  /\  ( vol `  (
( m  e.  NN  |->  ( ( g `  m )  \  U_ l  e.  ( 1..^ m ) ( g `
 l ) ) ) `  n ) )  e.  RR ) ) )
9493ralbidv 2731 . . . . . . . . . . . . . . . . . 18  |-  ( f  =  ( m  e.  NN  |->  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) )  ->  ( A. n  e.  NN  ( ( f `  n )  e.  dom  vol 
/\  ( vol `  (
f `  n )
)  e.  RR )  <->  A. n  e.  NN  ( ( ( m  e.  NN  |->  ( ( g `  m ) 
\  U_ l  e.  ( 1..^ m ) ( g `  l ) ) ) `  n
)  e.  dom  vol  /\  ( vol `  (
( m  e.  NN  |->  ( ( g `  m )  \  U_ l  e.  ( 1..^ m ) ( g `
 l ) ) ) `  n ) )  e.  RR ) ) )
9589adantr 453 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f  =  ( m  e.  NN  |->  ( ( g `  m ) 
\  U_ l  e.  ( 1..^ m ) ( g `  l ) ) )  /\  n  e.  NN )  ->  (
f `  n )  =  ( ( m  e.  NN  |->  ( ( g `  m ) 
\  U_ l  e.  ( 1..^ m ) ( g `  l ) ) ) `  n
) )
9695disjeq2dv 4212 . . . . . . . . . . . . . . . . . 18  |-  ( f  =  ( m  e.  NN  |->  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) )  ->  (Disj  n  e.  NN ( f `
 n )  <-> Disj  n  e.  NN ( ( m  e.  NN  |->  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) ) `  n
) ) )
9794, 96anbi12d 693 . . . . . . . . . . . . . . . . 17  |-  ( f  =  ( m  e.  NN  |->  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) )  ->  (
( A. n  e.  NN  ( ( f `
 n )  e. 
dom  vol  /\  ( vol `  ( f `  n
) )  e.  RR )  /\ Disj  n  e.  NN ( f `  n ) )  <->  ( A. n  e.  NN  ( ( ( m  e.  NN  |->  ( ( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) ) ) `  n )  e.  dom  vol 
/\  ( vol `  (
( m  e.  NN  |->  ( ( g `  m )  \  U_ l  e.  ( 1..^ m ) ( g `
 l ) ) ) `  n ) )  e.  RR )  /\ Disj  n  e.  NN ( ( m  e.  NN  |->  ( ( g `  m )  \  U_ l  e.  ( 1..^ m ) ( g `
 l ) ) ) `  n ) ) ) )
9889iuneq2d 4142 . . . . . . . . . . . . . . . . . . 19  |-  ( f  =  ( m  e.  NN  |->  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) )  ->  U_ n  e.  NN  ( f `  n )  =  U_ n  e.  NN  (
( m  e.  NN  |->  ( ( g `  m )  \  U_ l  e.  ( 1..^ m ) ( g `
 l ) ) ) `  n ) )
9998fveq2d 5761 . . . . . . . . . . . . . . . . . 18  |-  ( f  =  ( m  e.  NN  |->  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) )  ->  ( vol `  U_ n  e.  NN  ( f `  n ) )  =  ( vol `  U_ n  e.  NN  ( ( m  e.  NN  |->  ( ( g `  m ) 
\  U_ l  e.  ( 1..^ m ) ( g `  l ) ) ) `  n
) ) )
100 voliunnfl.1 . . . . . . . . . . . . . . . . . . . . . 22  |-  S  =  seq  1 (  +  ,  G )
101 voliunnfl.2 . . . . . . . . . . . . . . . . . . . . . . 23  |-  G  =  ( n  e.  NN  |->  ( vol `  ( f `
 n ) ) )
102 seqeq3 11359 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( G  =  ( n  e.  NN  |->  ( vol `  (
f `  n )
) )  ->  seq  1 (  +  ,  G )  =  seq  1 (  +  , 
( n  e.  NN  |->  ( vol `  ( f `
 n ) ) ) ) )
103101, 102ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22  |-  seq  1
(  +  ,  G
)  =  seq  1
(  +  ,  ( n  e.  NN  |->  ( vol `  ( f `
 n ) ) ) )
104100, 103eqtri 2462 . . . . . . . . . . . . . . . . . . . . 21  |-  S  =  seq  1 (  +  ,  ( n  e.  NN  |->  ( vol `  (
f `  n )
) ) )
105104rneqi 5125 . . . . . . . . . . . . . . . . . . . 20  |-  ran  S  =  ran  seq  1 (  +  ,  ( n  e.  NN  |->  ( vol `  ( f `  n
) ) ) )
106105supeq1i 7481 . . . . . . . . . . . . . . . . . . 19  |-  sup ( ran  S ,  RR* ,  <  )  =  sup ( ran 
seq  1 (  +  ,  ( n  e.  NN  |->  ( vol `  (
f `  n )
) ) ) , 
RR* ,  <  )
10791mpteq2dv 4321 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f  =  ( m  e.  NN  |->  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) )  ->  (
n  e.  NN  |->  ( vol `  ( f `
 n ) ) )  =  ( n  e.  NN  |->  ( vol `  ( ( m  e.  NN  |->  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) ) `  n
) ) ) )
108107seqeq3d 11362 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f  =  ( m  e.  NN  |->  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) )  ->  seq  1 (  +  , 
( n  e.  NN  |->  ( vol `  ( f `
 n ) ) ) )  =  seq  1 (  +  , 
( n  e.  NN  |->  ( vol `  ( ( m  e.  NN  |->  ( ( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) ) ) `  n ) ) ) ) )
109108rneqd 5126 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  =  ( m  e.  NN  |->  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) )  ->  ran  seq  1 (  +  , 
( n  e.  NN  |->  ( vol `  ( f `
 n ) ) ) )  =  ran  seq  1 (  +  , 
( n  e.  NN  |->  ( vol `  ( ( m  e.  NN  |->  ( ( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) ) ) `  n ) ) ) ) )
110109supeq1d 7480 . . . . . . . . . . . . . . . . . . 19  |-  ( f  =  ( m  e.  NN  |->  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) )  ->  sup ( ran  seq  1 (  +  ,  ( n  e.  NN  |->  ( vol `  ( f `  n
) ) ) ) ,  RR* ,  <  )  =  sup ( ran  seq  1 (  +  , 
( n  e.  NN  |->  ( vol `  ( ( m  e.  NN  |->  ( ( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) ) ) `  n ) ) ) ) ,  RR* ,  <  ) )
111106, 110syl5eq 2486 . . . . . . . . . . . . . . . . . 18  |-  ( f  =  ( m  e.  NN  |->  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) )  ->  sup ( ran  S ,  RR* ,  <  )  =  sup ( ran  seq  1 (  +  ,  ( n  e.  NN  |->  ( vol `  ( ( m  e.  NN  |->  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) ) `  n
) ) ) ) ,  RR* ,  <  )
)
11299, 111eqeq12d 2456 . . . . . . . . . . . . . . . . 17  |-  ( f  =  ( m  e.  NN  |->  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) )  ->  (
( vol `  U_ n  e.  NN  ( f `  n ) )  =  sup ( ran  S ,  RR* ,  <  )  <->  ( vol `  U_ n  e.  NN  ( ( m  e.  NN  |->  ( ( g `  m ) 
\  U_ l  e.  ( 1..^ m ) ( g `  l ) ) ) `  n
) )  =  sup ( ran  seq  1 (  +  ,  ( n  e.  NN  |->  ( vol `  ( ( m  e.  NN  |->  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) ) `  n
) ) ) ) ,  RR* ,  <  )
) )
11397, 112imbi12d 313 . . . . . . . . . . . . . . . 16  |-  ( f  =  ( m  e.  NN  |->  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) )  ->  (
( ( A. n  e.  NN  ( ( f `
 n )  e. 
dom  vol  /\  ( vol `  ( f `  n
) )  e.  RR )  /\ Disj  n  e.  NN ( f `  n ) )  ->  ( vol ` 
U_ n  e.  NN  ( f `  n
) )  =  sup ( ran  S ,  RR* ,  <  ) )  <->  ( ( A. n  e.  NN  ( ( ( m  e.  NN  |->  ( ( g `  m ) 
\  U_ l  e.  ( 1..^ m ) ( g `  l ) ) ) `  n
)  e.  dom  vol  /\  ( vol `  (
( m  e.  NN  |->  ( ( g `  m )  \  U_ l  e.  ( 1..^ m ) ( g `
 l ) ) ) `  n ) )  e.  RR )  /\ Disj  n  e.  NN ( ( m  e.  NN  |->  ( ( g `  m )  \  U_ l  e.  ( 1..^ m ) ( g `
 l ) ) ) `  n ) )  ->  ( vol ` 
U_ n  e.  NN  ( ( m  e.  NN  |->  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) ) `  n
) )  =  sup ( ran  seq  1 (  +  ,  ( n  e.  NN  |->  ( vol `  ( ( m  e.  NN  |->  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) ) `  n
) ) ) ) ,  RR* ,  <  )
) ) )
114 voliunnfl.3 . . . . . . . . . . . . . . . 16  |-  ( ( A. n  e.  NN  ( ( f `  n )  e.  dom  vol 
/\  ( vol `  (
f `  n )
)  e.  RR )  /\ Disj  n  e.  NN ( f `  n ) )  ->  ( vol ` 
U_ n  e.  NN  ( f `  n
) )  =  sup ( ran  S ,  RR* ,  <  ) )
11588, 113, 114vtocl 3012 . . . . . . . . . . . . . . 15  |-  ( ( A. n  e.  NN  ( ( ( m  e.  NN  |->  ( ( g `  m ) 
\  U_ l  e.  ( 1..^ m ) ( g `  l ) ) ) `  n
)  e.  dom  vol  /\  ( vol `  (
( m  e.  NN  |->  ( ( g `  m )  \  U_ l  e.  ( 1..^ m ) ( g `
 l ) ) ) `  n ) )  e.  RR )  /\ Disj  n  e.  NN ( ( m  e.  NN  |->  ( ( g `  m )  \  U_ l  e.  ( 1..^ m ) ( g `
 l ) ) ) `  n ) )  ->  ( vol ` 
U_ n  e.  NN  ( ( m  e.  NN  |->  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) ) `  n
) )  =  sup ( ran  seq  1 (  +  ,  ( n  e.  NN  |->  ( vol `  ( ( m  e.  NN  |->  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) ) `  n
) ) ) ) ,  RR* ,  <  )
)
11665iuneq2i 4135 . . . . . . . . . . . . . . . 16  |-  U_ n  e.  NN  ( ( m  e.  NN  |->  ( ( g `  m ) 
\  U_ l  e.  ( 1..^ m ) ( g `  l ) ) ) `  n
)  =  U_ n  e.  NN  ( ( g `
 n )  \  U_ l  e.  (
1..^ n ) ( g `  l ) )
117116fveq2i 5760 . . . . . . . . . . . . . . 15  |-  ( vol `  U_ n  e.  NN  ( ( m  e.  NN  |->  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) ) `  n
) )  =  ( vol `  U_ n  e.  NN  ( ( g `
 n )  \  U_ l  e.  (
1..^ n ) ( g `  l ) ) )
11867mpteq2ia 4316 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  NN  |->  ( vol `  ( ( m  e.  NN  |->  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) ) `  n
) ) )  =  ( n  e.  NN  |->  ( vol `  ( ( g `  n ) 
\  U_ l  e.  ( 1..^ n ) ( g `  l ) ) ) )
119 seqeq3 11359 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  e.  NN  |->  ( vol `  ( ( m  e.  NN  |->  ( ( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) ) ) `  n ) ) )  =  ( n  e.  NN  |->  ( vol `  (
( g `  n
)  \  U_ l  e.  ( 1..^ n ) ( g `  l
) ) ) )  ->  seq  1 (  +  ,  ( n  e.  NN  |->  ( vol `  ( ( m  e.  NN  |->  ( ( g `
 m )  \  U_ l  e.  (
1..^ m ) ( g `  l ) ) ) `  n
) ) ) )  =  seq  1 (  +  ,  ( n  e.  NN  |->  ( vol `  ( ( g `  n )  \  U_ l  e.  ( 1..^ n ) ( g `
 l ) ) ) ) ) )
120118, 119ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  seq  1
(  +  ,  ( n  e.  NN  |->  ( vol `  ( ( m  e.  NN  |->  ( ( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) ) ) `  n ) ) ) )  =  seq  1
(  +  ,  ( n  e.  NN  |->  ( vol `  ( ( g `  n ) 
\  U_ l  e.  ( 1..^ n ) ( g `  l ) ) ) ) )
121120rneqi 5125 . . . . . . . . . . . . . . . 16  |-  ran  seq  1 (  +  , 
( n  e.  NN  |->  ( vol `  ( ( m  e.  NN  |->  ( ( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) ) ) `  n ) ) ) )  =  ran  seq  1 (  +  , 
( n  e.  NN  |->  ( vol `  ( ( g `  n ) 
\  U_ l  e.  ( 1..^ n ) ( g `  l ) ) ) ) )
122121supeq1i 7481 . . . . . . . . . . . . . . 15  |-  sup ( ran  seq  1 (  +  ,  ( n  e.  NN  |->  ( vol `  (
( m  e.  NN  |->  ( ( g `  m )  \  U_ l  e.  ( 1..^ m ) ( g `
 l ) ) ) `  n ) ) ) ) , 
RR* ,  <  )  =  sup ( ran  seq  1 (  +  , 
( n  e.  NN  |->  ( vol `  ( ( g `  n ) 
\  U_ l  e.  ( 1..^ n ) ( g `  l ) ) ) ) ) ,  RR* ,  <  )
123115, 117, 1223eqtr3g 2497 . . . . . . . . . . . . . 14  |-  ( ( A. n  e.  NN  ( ( ( m  e.  NN  |->  ( ( g `  m ) 
\  U_ l  e.  ( 1..^ m ) ( g `  l ) ) ) `  n
)  e.  dom  vol  /\  ( vol `  (
( m  e.  NN  |->  ( ( g `  m )  \  U_ l  e.  ( 1..^ m ) ( g `
 l ) ) ) `  n ) )  e.  RR )  /\ Disj  n  e.  NN ( ( m  e.  NN  |->  ( ( g `  m )  \  U_ l  e.  ( 1..^ m ) ( g `
 l ) ) ) `  n ) )  ->  ( vol ` 
U_ n  e.  NN  ( ( g `  n )  \  U_ l  e.  ( 1..^ n ) ( g `
 l ) ) )  =  sup ( ran  seq  1 (  +  ,  ( n  e.  NN  |->  ( vol `  (
( g `  n
)  \  U_ l  e.  ( 1..^ n ) ( g `  l
) ) ) ) ) ,  RR* ,  <  ) )
12481, 86, 123sylancl 645 . . . . . . . . . . . . 13  |-  ( A. m  e.  NN  (
( g `  m
)  C_  RR  /\  ( vol * `  ( g `
 m ) )  =  0 )  -> 
( vol `  U_ n  e.  NN  ( ( g `
 n )  \  U_ l  e.  (
1..^ n ) ( g `  l ) ) )  =  sup ( ran  seq  1 (  +  ,  ( n  e.  NN  |->  ( vol `  ( ( g `  n )  \  U_ l  e.  ( 1..^ n ) ( g `
 l ) ) ) ) ) , 
RR* ,  <  ) )
125124adantl 454 . . . . . . . . . . . 12  |-  ( ( g : NN -onto-> A  /\  A. m  e.  NN  ( ( g `  m )  C_  RR  /\  ( vol * `  ( g `  m
) )  =  0 ) )  ->  ( vol `  U_ n  e.  NN  ( ( g `
 n )  \  U_ l  e.  (
1..^ n ) ( g `  l ) ) )  =  sup ( ran  seq  1 (  +  ,  ( n  e.  NN  |->  ( vol `  ( ( g `  n )  \  U_ l  e.  ( 1..^ n ) ( g `
 l ) ) ) ) ) , 
RR* ,  <  ) )
12682iundisj 19473 . . . . . . . . . . . . . . . 16  |-  U_ n  e.  NN  ( g `  n )  =  U_ n  e.  NN  (
( g `  n
)  \  U_ l  e.  ( 1..^ n ) ( g `  l
) )
127 fofun 5683 . . . . . . . . . . . . . . . . 17  |-  ( g : NN -onto-> A  ->  Fun  g )
128 funiunfv 6024 . . . . . . . . . . . . . . . . 17  |-  ( Fun  g  ->  U_ n  e.  NN  ( g `  n )  =  U. ( g " NN ) )
129127, 128syl 16 . . . . . . . . . . . . . . . 16  |-  ( g : NN -onto-> A  ->  U_ n  e.  NN  ( g `  n
)  =  U. (
g " NN ) )
130126, 129syl5eqr 2488 . . . . . . . . . . . . . . 15  |-  ( g : NN -onto-> A  ->  U_ n  e.  NN  ( ( g `  n )  \  U_ l  e.  ( 1..^ n ) ( g `
 l ) )  =  U. ( g
" NN ) )
13129unieqd 4050 . . . . . . . . . . . . . . 15  |-  ( g : NN -onto-> A  ->  U. ( g " NN )  =  U. A )
132130, 131eqtrd 2474 . . . . . . . . . . . . . 14  |-  ( g : NN -onto-> A  ->  U_ n  e.  NN  ( ( g `  n )  \  U_ l  e.  ( 1..^ n ) ( g `
 l ) )  =  U. A )
133132fveq2d 5761 . . . . . . . . . . . . 13  |-  ( g : NN -onto-> A  -> 
( vol `  U_ n  e.  NN  ( ( g `
 n )  \  U_ l  e.  (
1..^ n ) ( g `  l ) ) )  =  ( vol `  U. A
) )
134133adantr 453 . . . . . . . . . . . 12  |-  ( ( g : NN -onto-> A  /\  A. m  e.  NN  ( ( g `  m )  C_  RR  /\  ( vol * `  ( g `  m
) )  =  0 ) )  ->  ( vol `  U_ n  e.  NN  ( ( g `
 n )  \  U_ l  e.  (
1..^ n ) ( g `  l ) ) )  =  ( vol `  U. A
) )
13557sseq1d 3361 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  =  n  ->  (
( g `  m
)  C_  RR  <->  ( g `  n )  C_  RR ) )
13657fveq2d 5761 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( m  =  n  ->  ( vol * `  ( g `
 m ) )  =  ( vol * `  ( g `  n
) ) )
137136eqeq1d 2450 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  =  n  ->  (
( vol * `  ( g `  m
) )  =  0  <-> 
( vol * `  ( g `  n
) )  =  0 ) )
138135, 137anbi12d 693 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  n  ->  (
( ( g `  m )  C_  RR  /\  ( vol * `  ( g `  m
) )  =  0 )  <->  ( ( g `
 n )  C_  RR  /\  ( vol * `  ( g `  n
) )  =  0 ) ) )
139138rspccva 3057 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A. m  e.  NN  ( ( g `  m )  C_  RR  /\  ( vol * `  ( g `  m
) )  =  0 )  /\  n  e.  NN )  ->  (
( g `  n
)  C_  RR  /\  ( vol * `  ( g `
 n ) )  =  0 ) )
140 ssdifss 3464 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( g `  n ) 
C_  RR  ->  ( ( g `  n ) 
\  U_ l  e.  ( 1..^ n ) ( g `  l ) )  C_  RR )
141140adantr 453 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( g `  n
)  C_  RR  /\  ( vol * `  ( g `
 n ) )  =  0 )  -> 
( ( g `  n )  \  U_ l  e.  ( 1..^ n ) ( g `
 l ) ) 
C_  RR )
142 difss 3460 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( g `  n ) 
\  U_ l  e.  ( 1..^ n ) ( g `  l ) )  C_  ( g `  n )
143 ovolssnul 19414 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( g `  n )  \  U_ l  e.  ( 1..^ n ) ( g `
 l ) ) 
C_  ( g `  n )  /\  (
g `  n )  C_  RR  /\  ( vol
* `  ( g `  n ) )  =  0 )  ->  ( vol * `  ( ( g `  n ) 
\  U_ l  e.  ( 1..^ n ) ( g `  l ) ) )  =  0 )
144142, 143mp3an1 1267 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( g `  n
)  C_  RR  /\  ( vol * `  ( g `
 n ) )  =  0 )  -> 
( vol * `  ( ( g `  n )  \  U_ l  e.  ( 1..^ n ) ( g `
 l ) ) )  =  0 )
145141, 144jca 520 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( g `  n
)  C_  RR  /\  ( vol * `  ( g `
 n ) )  =  0 )  -> 
( ( ( g `
 n )  \  U_ l  e.  (
1..^ n ) ( g `  l ) )  C_  RR  /\  ( vol * `  ( ( g `  n ) 
\  U_ l  e.  ( 1..^ n ) ( g `  l ) ) )  =  0 ) )
146 nulmbl 19461 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( g `  n )  \  U_ l  e.  ( 1..^ n ) ( g `
 l ) ) 
C_  RR  /\  ( vol * `  ( ( g `  n ) 
\  U_ l  e.  ( 1..^ n ) ( g `  l ) ) )  =  0 )  ->  ( (
g `  n )  \  U_ l  e.  ( 1..^ n ) ( g `  l ) )  e.  dom  vol )
147 mblvol 19457 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( g `  n
)  \  U_ l  e.  ( 1..^ n ) ( g `  l
) )  e.  dom  vol 
->  ( vol `  (
( g `  n
)  \  U_ l  e.  ( 1..^ n ) ( g `  l
) ) )  =  ( vol * `  ( ( g `  n )  \  U_ l  e.  ( 1..^ n ) ( g `
 l ) ) ) )
148145, 146, 1473syl 19 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( g `  n
)  C_  RR  /\  ( vol * `  ( g `
 n ) )  =  0 )  -> 
( vol `  (
( g `  n
)  \  U_ l  e.  ( 1..^ n ) ( g `  l
) ) )  =  ( vol * `  ( ( g `  n )  \  U_ l  e.  ( 1..^ n ) ( g `
 l ) ) ) )
149148, 144eqtrd 2474 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( g `  n
)  C_  RR  /\  ( vol * `  ( g `
 n ) )  =  0 )  -> 
( vol `  (
( g `  n
)  \  U_ l  e.  ( 1..^ n ) ( g `  l
) ) )  =  0 )
150139, 149syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( A. m  e.  NN  ( ( g `  m )  C_  RR  /\  ( vol * `  ( g `  m
) )  =  0 )  /\  n  e.  NN )  ->  ( vol `  ( ( g `
 n )  \  U_ l  e.  (
1..^ n ) ( g `  l ) ) )  =  0 )
151150mpteq2dva 4320 . . . . . . . . . . . . . . . . 17  |-  ( A. m  e.  NN  (
( g `  m
)  C_  RR  /\  ( vol * `  ( g `
 m ) )  =  0 )  -> 
( n  e.  NN  |->  ( vol `  ( ( g `  n ) 
\  U_ l  e.  ( 1..^ n ) ( g `  l ) ) ) )  =  ( n  e.  NN  |->  0 ) )
152151seqeq3d 11362 . . . . . . . . . . . . . . . 16  |-  ( A. m  e.  NN  (
( g `  m
)  C_  RR  /\  ( vol * `  ( g `
 m ) )  =  0 )  ->  seq  1 (  +  , 
( n  e.  NN  |->  ( vol `  ( ( g `  n ) 
\  U_ l  e.  ( 1..^ n ) ( g `  l ) ) ) ) )  =  seq  1 (  +  ,  ( n  e.  NN  |->  0 ) ) )
153152rneqd 5126 . . . . . . . . . . . . . . 15  |-  ( A. m  e.  NN  (
( g `  m
)  C_  RR  /\  ( vol * `  ( g `
 m ) )  =  0 )  ->  ran  seq  1 (  +  ,  ( n  e.  NN  |->  ( vol `  (
( g `  n
)  \  U_ l  e.  ( 1..^ n ) ( g `  l
) ) ) ) )  =  ran  seq  1 (  +  , 
( n  e.  NN  |->  0 ) ) )
154153supeq1d 7480 . . . . . . . . . . . . . 14  |-  ( A. m  e.  NN  (
( g `  m
)  C_  RR  /\  ( vol * `  ( g `
 m ) )  =  0 )  ->  sup ( ran  seq  1
(  +  ,  ( n  e.  NN  |->  ( vol `  ( ( g `  n ) 
\  U_ l  e.  ( 1..^ n ) ( g `  l ) ) ) ) ) ,  RR* ,  <  )  =  sup ( ran  seq  1 (  +  , 
( n  e.  NN  |->  0 ) ) , 
RR* ,  <  ) )
155 0cn 9115 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  CC
156 ser1const 11410 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 0  e.  CC  /\  m  e.  NN )  ->  (  seq  1 (  +  ,  ( NN 
X.  { 0 } ) ) `  m
)  =  ( m  x.  0 ) )
157155, 156mpan 653 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  e.  NN  ->  (  seq  1 (  +  , 
( NN  X.  {
0 } ) ) `
 m )  =  ( m  x.  0 ) )
158 nncn 10039 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( m  e.  NN  ->  m  e.  CC )
159158mul01d 9296 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  e.  NN  ->  (
m  x.  0 )  =  0 )
160157, 159eqtrd 2474 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  e.  NN  ->  (  seq  1 (  +  , 
( NN  X.  {
0 } ) ) `
 m )  =  0 )
161160mpteq2ia 4316 . . . . . . . . . . . . . . . . . . 19  |-  ( m  e.  NN  |->  (  seq  1 (  +  , 
( NN  X.  {
0 } ) ) `
 m ) )  =  ( m  e.  NN  |->  0 )
162 fconstmpt 4950 . . . . . . . . . . . . . . . . . . . . 21  |-  ( NN 
X.  { 0 } )  =  ( n  e.  NN  |->  0 )
163 seqeq3 11359 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( NN  X.  { 0 } )  =  ( n  e.  NN  |->  0 )  ->  seq  1
(  +  ,  ( NN  X.  { 0 } ) )  =  seq  1 (  +  ,  ( n  e.  NN  |->  0 ) ) )
164162, 163ax-mp 5 . . . . . . . . . . . . . . . . . . . 20  |-  seq  1
(  +  ,  ( NN  X.  { 0 } ) )  =  seq  1 (  +  ,  ( n  e.  NN  |->  0 ) )
165 1z 10342 . . . . . . . . . . . . . . . . . . . . . 22  |-  1  e.  ZZ
166 seqfn 11366 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 1  e.  ZZ  ->  seq  1 (  +  , 
( NN  X.  {
0 } ) )  Fn  ( ZZ>= `  1
) )
167165, 166ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21  |-  seq  1
(  +  ,  ( NN  X.  { 0 } ) )  Fn  ( ZZ>= `  1 )
168 nnuz 10552 . . . . . . . . . . . . . . . . . . . . . . 23  |-  NN  =  ( ZZ>= `  1 )
169168fneq2i 5569 . . . . . . . . . . . . . . . . . . . . . 22  |-  (  seq  1 (  +  , 
( NN  X.  {
0 } ) )  Fn  NN  <->  seq  1
(  +  ,  ( NN  X.  { 0 } ) )  Fn  ( ZZ>= `  1 )
)
170 dffn5 5801 . . . . . . . . . . . . . . . . . . . . . 22  |-  (  seq  1 (  +  , 
( NN  X.  {
0 } ) )  Fn  NN  <->  seq  1
(  +  ,  ( NN  X.  { 0 } ) )  =  ( m  e.  NN  |->  (  seq  1 (  +  ,  ( NN  X.  { 0 } ) ) `  m ) ) )
171169, 170bitr3i 244 . . . . . . . . . . . . . . . . . . . . 21  |-  (  seq  1 (  +  , 
( NN  X.  {
0 } ) )  Fn  ( ZZ>= `  1
)  <->  seq  1 (  +  ,  ( NN  X.  { 0 } ) )  =  ( m  e.  NN  |->  (  seq  1 (  +  , 
( NN  X.  {
0 } ) ) `
 m ) ) )
172167, 171mpbi 201 . . . . . . . . . . . . . . . . . . . 20  |-  seq  1
(  +  ,  ( NN  X.  { 0 } ) )  =  ( m  e.  NN  |->  (  seq  1 (  +  ,  ( NN  X.  { 0 } ) ) `  m ) )
173164, 172eqtr3i 2464 . . . . . . . . . . . . . . . . . . 19  |-  seq  1
(  +  ,  ( n  e.  NN  |->  0 ) )  =  ( m  e.  NN  |->  (  seq  1 (  +  ,  ( NN  X.  { 0 } ) ) `  m ) )
174 fconstmpt 4950 . . . . . . . . . . . . . . . . . . 19  |-  ( NN 
X.  { 0 } )  =  ( m  e.  NN  |->  0 )
175161, 173, 1743eqtr4i 2472 . . . . . . . . . . . . . . . . . 18  |-  seq  1
(  +  ,  ( n  e.  NN  |->  0 ) )  =  ( NN  X.  { 0 } )
176175rneqi 5125 . . . . . . . . . . . . . . . . 17  |-  ran  seq  1 (  +  , 
( n  e.  NN  |->  0 ) )  =  ran  ( NN  X.  { 0 } )
177 1nn 10042 . . . . . . . . . . . . . . . . . 18  |-  1  e.  NN
178 ne0i 3619 . . . . . . . . . . . . . . . . . 18  |-  ( 1  e.  NN  ->  NN  =/=  (/) )
179 rnxp 5328 . . . . . . . . . . . . . . . . . 18  |-  ( NN  =/=  (/)  ->  ran  ( NN 
X.  { 0 } )  =  { 0 } )
180177, 178, 179mp2b 10 . . . . . . . . . . . . . . . . 17  |-  ran  ( NN  X.  { 0 } )  =  { 0 }
181176, 180eqtri 2462 . . . . . . . . . . . . . . . 16  |-  ran  seq  1 (  +  , 
( n  e.  NN  |->  0 ) )  =  { 0 }
182181supeq1i 7481 . . . . . . . . . . . . . . 15  |-  sup ( ran  seq  1 (  +  ,  ( n  e.  NN  |->  0 ) ) ,  RR* ,  <  )  =  sup ( { 0 } ,  RR* ,  <  )
183 xrltso 10765 . . . . . . . . . . . . . . . 16  |-  <  Or  RR*
184 0xr 9162 . . . . . . . . . . . . . . . 16  |-  0  e.  RR*
185 supsn 7503 . . . . . . . . . . . . . . . 16  |-  ( (  <  Or  RR*  /\  0  e.  RR* )  ->  sup ( { 0 } ,  RR* ,  <  )  =  0 )
186183, 184, 185mp2an 655 . . . . . . . . . . . . . . 15  |-  sup ( { 0 } ,  RR* ,  <  )  =  0
187182, 186eqtri 2462 . . . . . . . . . . . . . 14  |-  sup ( ran  seq  1 (  +  ,  ( n  e.  NN  |->  0 ) ) ,  RR* ,  <  )  =  0
188154, 187syl6eq 2490 . . . . . . . . . . . . 13  |-  ( A. m  e.  NN  (
( g `  m
)  C_  RR  /\  ( vol * `  ( g `
 m ) )  =  0 )  ->  sup ( ran  seq  1
(  +  ,  ( n  e.  NN  |->  ( vol `  ( ( g `  n ) 
\  U_ l  e.  ( 1..^ n ) ( g `  l ) ) ) ) ) ,  RR* ,  <  )  =  0 )
189188adantl 454 . . . . . . . . . . . 12  |-  ( ( g : NN -onto-> A  /\  A. m  e.  NN  ( ( g `  m )  C_  RR  /\  ( vol * `  ( g `  m
) )  =  0 ) )  ->  sup ( ran  seq  1 (  +  ,  ( n  e.  NN  |->  ( vol `  ( ( g `  n )  \  U_ l  e.  ( 1..^ n ) ( g `
 l ) ) ) ) ) , 
RR* ,  <  )  =  0 )
190125, 134, 1893eqtr3rd 2483 . . . . . . . . . . 11  |-  ( ( g : NN -onto-> A  /\  A. m  e.  NN  ( ( g `  m )  C_  RR  /\  ( vol * `  ( g `  m
) )  =  0 ) )  ->  0  =  ( vol `  U. A ) )
191190ex 425 . . . . . . . . . 10  |-  ( g : NN -onto-> A  -> 
( A. m  e.  NN  ( ( g `
 m )  C_  RR  /\  ( vol * `  ( g `  m
) )  =  0 )  ->  0  =  ( vol `  U. A
) ) )
19239, 191sylbid 208 . . . . . . . . 9  |-  ( g : NN -onto-> A  -> 
( A. x  e.  A  ( x  C_  RR  /\  ( vol * `  x )  =  0 )  ->  0  =  ( vol `  U. A
) ) )
19328, 192syl5 31 . . . . . . . 8  |-  ( g : NN -onto-> A  -> 
( ( A. x  e.  A  x  ~<_  NN  /\  U. A  C_  RR )  ->  0  =  ( vol `  U. A ) ) )
194193exlimiv 1645 . . . . . . 7  |-  ( E. g  g : NN -onto-> A  ->  ( ( A. x  e.  A  x  ~<_  NN  /\  U. A  C_  RR )  ->  0  =  ( vol `  U. A ) ) )
19518, 194syl 16 . . . . . 6  |-  ( ( A  =/=  (/)  /\  A  ~<_  NN )  ->  ( ( A. x  e.  A  x  ~<_  NN  /\  U. A  C_  RR )  ->  0  =  ( vol `  U. A ) ) )
196195expimpd 588 . . . . 5  |-  ( A  =/=  (/)  ->  ( ( A  ~<_  NN  /\  ( A. x  e.  A  x  ~<_  NN  /\  U. A  C_  RR ) )  -> 
0  =  ( vol `  U. A ) ) )
19711, 196pm2.61ine 2686 . . . 4  |-  ( ( A  ~<_  NN  /\  ( A. x  e.  A  x  ~<_  NN  /\  U. A  C_  RR ) )  -> 
0  =  ( vol `  U. A ) )
198 renepnf 9163 . . . . . . 7  |-  ( 0  e.  RR  ->  0  =/=  +oo )
19948, 198mp1i 12 . . . . . 6  |-  ( U. A  =  RR  ->  0  =/=  +oo )
200 fveq2 5757 . . . . . . 7  |-  ( U. A  =  RR  ->  ( vol `  U. A
)  =  ( vol `  RR ) )
201 rembl 19466 . . . . . . . . 9  |-  RR  e.  dom  vol
202 mblvol 19457 . . . . . . . . 9  |-  ( RR  e.  dom  vol  ->  ( vol `  RR )  =  ( vol * `  RR ) )
203201, 202ax-mp 5 . . . . . . . 8  |-  ( vol `  RR )  =  ( vol * `  RR )
204 ovolre 19452 . . . . . . . 8  |-  ( vol
* `  RR )  =  +oo
205203, 204eqtri 2462 . . . . . . 7  |-  ( vol `  RR )  =  +oo
206200, 205syl6eq 2490 . . . . . 6  |-  ( U. A  =  RR  ->  ( vol `  U. A
)  =  +oo )
207199, 206neeqtrrd 2631 . . . . 5  |-  ( U. A  =  RR  ->  0  =/=  ( vol `  U. A ) )
208207necon2i 2657 . . . 4  |-  ( 0  =  ( vol `  U. A )  ->  U. A  =/=  RR )
209197, 208syl 16 . . 3  |-  ( ( A  ~<_  NN  /\  ( A. x  e.  A  x  ~<_  NN  /\  U. A  C_  RR ) )  ->  U. A  =/=  RR )
210209expr 600 . 2  |-  ( ( A  ~<_  NN  /\  A. x  e.  A  x  ~<_  NN )  ->  ( U. A  C_  RR  ->  U. A  =/= 
RR ) )
211 eqimss 3386 . . 3  |-  ( U. A  =  RR  ->  U. A  C_  RR )
212211necon3bi 2651 . 2  |-  ( -. 
U. A  C_  RR  ->  U. A  =/=  RR )
213210, 212pm2.61d1 154 1  |-  ( ( A  ~<_  NN  /\  A. x  e.  A  x  ~<_  NN )  ->  U. A  =/=  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360   E.wex 1551    = wceq 1653    e. wcel 1727    =/= wne 2605   A.wral 2711   _Vcvv 2962    \ cdif 3303    C_ wss 3306   (/)c0 3613   {csn 3838   U.cuni 4039   U_ciun 4117  Disj wdisj 4207   class class class wbr 4237    e. cmpt 4291    Or wor 4531    X. cxp 4905   dom cdm 4907   ran crn 4908   "cima 4910   Fun wfun 5477    Fn wfn 5478   -onto->wfo 5481   ` cfv 5483  (class class class)co 6110    ~<_ cdom 7136    ~< csdm 7137   supcsup 7474   CCcc 9019   RRcr 9020   0cc0 9021   1c1 9022    + caddc 9024    x. cmul 9026    +oocpnf 9148   RR*cxr 9150    < clt 9151   NNcn 10031   ZZcz 10313   ZZ>=cuz 10519  ..^cfzo 11166    seq cseq 11354   vol *covol 19390   volcvol 19391
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-13 1729  ax-14 1731  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423  ax-rep 4345  ax-sep 4355  ax-nul 4363  ax-pow 4406  ax-pr 4432  ax-un 4730  ax-inf2 7625  ax-cnex 9077  ax-resscn 9078  ax-1cn 9079  ax-icn 9080  ax-addcl 9081  ax-addrcl 9082  ax-mulcl 9083  ax-mulrcl 9084  ax-mulcom 9085  ax-addass 9086  ax-mulass 9087  ax-distr 9088  ax-i2m1 9089  ax-1ne0 9090  ax-1rid 9091  ax-rnegex 9092  ax-rrecex 9093  ax-cnre 9094  ax-pre-lttri 9095  ax-pre-lttrn 9096  ax-pre-ltadd 9097  ax-pre-mulgt0 9098  ax-pre-sup 9099
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2291  df-mo 2292  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-nel 2608  df-ral 2716  df-rex 2717  df-reu 2718  df-rmo 2719  df-rab 2720  df-v 2964  df-sbc 3168  df-csb 3268  df-dif 3309  df-un 3311  df-in 3313  df-ss 3320  df-pss 3322  df-nul 3614  df-if 3764  df-pw 3825  df-sn 3844  df-pr 3845  df-tp 3846  df-op 3847  df-uni 4040  df-int 4075  df-iun 4119  df-disj 4208  df-br 4238  df-opab 4292  df-mpt 4293  df-tr 4328  df-eprel 4523  df-id 4527  df-po 4532  df-so 4533  df-fr 4570  df-se 4571  df-we 4572  df-ord 4613  df-on 4614  df-lim 4615  df-suc 4616  df-om 4875  df-xp 4913  df-rel 4914  df-cnv 4915  df-co 4916  df-dm 4917  df-rn 4918  df-res 4919  df-ima 4920  df-iota 5447  df-fun 5485  df-fn 5486  df-f 5487  df-f1 5488  df-fo 5489  df-f1o 5490  df-fv 5491  df-isom 5492  df-ov 6113  df-oprab 6114  df-mpt2 6115  df-of 6334  df-1st 6378  df-2nd 6379  df-riota 6578  df-recs 6662  df-rdg 6697  df-1o 6753  df-2o 6754  df-oadd 6757  df-er 6934  df-map 7049  df-en 7139  df-dom 7140  df-sdom 7141  df-fin 7142  df-fi 7445  df-sup 7475  df-oi 7508  df-card 7857  df-cda 8079  df-pnf 9153  df-mnf 9154  df-xr 9155  df-ltxr 9156  df-le 9157  df-sub 9324  df-neg 9325  df-div 9709  df-nn 10032  df-2 10089  df-3 10090  df-n0 10253  df-z 10314  df-uz 10520  df-q 10606  df-rp 10644  df-xneg 10741  df-xadd 10742  df-xmul 10743  df-ioo 10951  df-ico 10953  df-icc 10954  df-fz 11075  df-fzo 11167  df-fl 11233  df-seq 11355  df-exp 11414  df-hash 11650  df-cj 11935  df-re 11936  df-im 11937  df-sqr 12071  df-abs 12072  df-clim 12313  df-sum 12511  df-rest 13681  df-topgen 13698  df-psmet 16725  df-xmet 16726  df-met 16727  df-bl 16728  df-mopn 16729  df-top 16994  df-bases 16996  df-topon 16997  df-cmp 17481  df-ovol 19392  df-vol 19393
  Copyright terms: Public domain W3C validator