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

Theorem voliunnfl 28378
Description: voliun 21004 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 4092 . . . . . . . . 9  |-  ( A  =  (/)  ->  U. A  =  U. (/) )
2 uni0 4111 . . . . . . . . 9  |-  U. (/)  =  (/)
31, 2syl6eq 2485 . . . . . . . 8  |-  ( A  =  (/)  ->  U. A  =  (/) )
43fveq2d 5688 . . . . . . 7  |-  ( A  =  (/)  ->  ( vol `  U. A )  =  ( vol `  (/) ) )
5 0mbl 20990 . . . . . . . . 9  |-  (/)  e.  dom  vol
6 mblvol 20982 . . . . . . . . 9  |-  ( (/)  e.  dom  vol  ->  ( vol `  (/) )  =  ( vol* `  (/) ) )
75, 6ax-mp 5 . . . . . . . 8  |-  ( vol `  (/) )  =  ( vol* `  (/) )
8 ovol0 20945 . . . . . . . 8  |-  ( vol* `  (/) )  =  0
97, 8eqtri 2457 . . . . . . 7  |-  ( vol `  (/) )  =  0
104, 9syl6req 2486 . . . . . 6  |-  ( A  =  (/)  ->  0  =  ( vol `  U. A ) )
1110a1d 25 . . . . 5  |-  ( A  =  (/)  ->  ( ( A  ~<_  NN  /\  ( A. x  e.  A  x  ~<_  NN  /\  U. A  C_  RR ) )  -> 
0  =  ( vol `  U. A ) ) )
12 reldom 7308 . . . . . . . . . . 11  |-  Rel  ~<_
1312brrelexi 4871 . . . . . . . . . 10  |-  ( A  ~<_  NN  ->  A  e.  _V )
14 0sdomg 7432 . . . . . . . . . 10  |-  ( A  e.  _V  ->  ( (/) 
~<  A  <->  A  =/=  (/) ) )
1513, 14syl 16 . . . . . . . . 9  |-  ( A  ~<_  NN  ->  ( (/)  ~<  A  <->  A  =/=  (/) ) )
1615biimparc 487 . . . . . . . 8  |-  ( ( A  =/=  (/)  /\  A  ~<_  NN )  ->  (/)  ~<  A )
17 fodomr 7454 . . . . . . . 8  |-  ( (
(/)  ~<  A  /\  A  ~<_  NN )  ->  E. g 
g : NN -onto-> A
)
1816, 17sylancom 667 . . . . . . 7  |-  ( ( A  =/=  (/)  /\  A  ~<_  NN )  ->  E. g 
g : NN -onto-> A
)
19 unissb 4116 . . . . . . . . . . . . 13  |-  ( U. A  C_  RR  <->  A. x  e.  A  x  C_  RR )
2019anbi1i 695 . . . . . . . . . . . 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 2843 . . . . . . . . . . . 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 252 . . . . . . . . . . 11  |-  ( ( U. A  C_  RR  /\ 
A. x  e.  A  x  ~<_  NN )  <->  A. x  e.  A  ( x  C_  RR  /\  x  ~<_  NN ) )
23 ovolctb2 20944 . . . . . . . . . . . . . 14  |-  ( ( x  C_  RR  /\  x  ~<_  NN )  ->  ( vol* `  x )  =  0 )
2423ex 434 . . . . . . . . . . . . 13  |-  ( x 
C_  RR  ->  ( x  ~<_  NN  ->  ( vol* `  x )  =  0 ) )
2524imdistani 690 . . . . . . . . . . . 12  |-  ( ( x  C_  RR  /\  x  ~<_  NN )  ->  ( x 
C_  RR  /\  ( vol* `  x )  =  0 ) )
2625ralimi 2785 . . . . . . . . . . 11  |-  ( A. x  e.  A  (
x  C_  RR  /\  x  ~<_  NN )  ->  A. x  e.  A  ( x  C_  RR  /\  ( vol* `  x )  =  0 ) )
2722, 26sylbi 195 . . . . . . . . . 10  |-  ( ( U. A  C_  RR  /\ 
A. x  e.  A  x  ~<_  NN )  ->  A. x  e.  A  ( x  C_  RR  /\  ( vol* `  x
)  =  0 ) )
2827ancoms 453 . . . . . . . . 9  |-  ( ( A. x  e.  A  x  ~<_  NN  /\  U. A  C_  RR )  ->  A. x  e.  A  ( x  C_  RR  /\  ( vol* `  x )  =  0 ) )
29 foima 5618 . . . . . . . . . . . 12  |-  ( g : NN -onto-> A  -> 
( g " NN )  =  A )
3029raleqdv 2917 . . . . . . . . . . 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 5615 . . . . . . . . . . . 12  |-  ( g : NN -onto-> A  -> 
g  Fn  NN )
32 ssid 3368 . . . . . . . . . . . 12  |-  NN  C_  NN
33 sseq1 3370 . . . . . . . . . . . . . 14  |-  ( x  =  ( g `  m )  ->  (
x  C_  RR  <->  ( g `  m )  C_  RR ) )
34 fveq2 5684 . . . . . . . . . . . . . . 15  |-  ( x  =  ( g `  m )  ->  ( vol* `  x )  =  ( vol* `  ( g `  m
) ) )
3534eqeq1d 2445 . . . . . . . . . . . . . 14  |-  ( x  =  ( g `  m )  ->  (
( vol* `  x )  =  0  <-> 
( vol* `  ( g `  m
) )  =  0 ) )
3633, 35anbi12d 710 . . . . . . . . . . . . 13  |-  ( x  =  ( g `  m )  ->  (
( x  C_  RR  /\  ( vol* `  x )  =  0 )  <->  ( ( g `
 m )  C_  RR  /\  ( vol* `  ( g `  m
) )  =  0 ) ) )
3736ralima 5950 . . . . . . . . . . . 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 662 . . . . . . . . . . 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 255 . . . . . . . . . 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 3476 . . . . . . . . . . . . . . . . . 18  |-  ( ( g `  m ) 
\  U_ l  e.  ( 1..^ m ) ( g `  l ) )  C_  ( g `  m )
41 ovolssnul 20939 . . . . . . . . . . . . . . . . . 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 1301 . . . . . . . . . . . . . . . . 17  |-  ( ( ( g `  m
)  C_  RR  /\  ( vol* `  ( g `
 m ) )  =  0 )  -> 
( vol* `  ( ( g `  m )  \  U_ l  e.  ( 1..^ m ) ( g `
 l ) ) )  =  0 )
43 ssdifss 3480 . . . . . . . . . . . . . . . . . 18  |-  ( ( g `  m ) 
C_  RR  ->  ( ( g `  m ) 
\  U_ l  e.  ( 1..^ m ) ( g `  l ) )  C_  RR )
44 nulmbl 20986 . . . . . . . . . . . . . . . . . . 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 20982 . . . . . . . . . . . . . . . . . . . . . . . . 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 2445 . . . . . . . . . . . . . . . . . . . . . . . 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 485 . . . . . . . . . . . . . . . . . . . . . . 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 9378 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  e.  RR
4947, 48syl6eqel 2525 . . . . . . . . . . . . . . . . . . . . . 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 435 . . . . . . . . . . . . . . . . . . . . 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 553 . . . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . . 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 471 . . . . . . . . . . . . . . . . 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 470 . . . . . . . . . . . . . . . 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 2785 . . . . . . . . . . . . . . 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 5684 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  =  n  ->  (
g `  m )  =  ( g `  n ) )
58 oveq2 6094 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( m  =  n  ->  (
1..^ m )  =  ( 1..^ n ) )
5958iuneq1d 4188 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  =  n  ->  U_ l  e.  ( 1..^ m ) ( g `  l
)  =  U_ l  e.  ( 1..^ n ) ( g `  l
) )
6057, 59difeq12d 3468 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  n  ->  (
( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) )  =  ( ( g `  n
)  \  U_ l  e.  ( 1..^ n ) ( g `  l
) ) )
61 eqid 2437 . . . . . . . . . . . . . . . . . . . 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 5694 . . . . . . . . . . . . . . . . . . . . 21  |-  ( g `
 n )  e. 
_V
63 difexg 4433 . . . . . . . . . . . . . . . . . . . . 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 5767 . . . . . . . . . . . . . . . . . . 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 2503 . . . . . . . . . . . . . . . . . 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 5688 . . . . . . . . . . . . . . . . . . 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 2503 . . . . . . . . . . . . . . . . . 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 710 . . . . . . . . . . . . . . . . 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 2741 . . . . . . . . . . . . . . . 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 5684 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  m  ->  (
g `  n )  =  ( g `  m ) )
72 oveq2 6094 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  m  ->  (
1..^ n )  =  ( 1..^ m ) )
7372iuneq1d 4188 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  m  ->  U_ l  e.  ( 1..^ n ) ( g `  l
)  =  U_ l  e.  ( 1..^ m ) ( g `  l
) )
7471, 73difeq12d 3468 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  m  ->  (
( g `  n
)  \  U_ l  e.  ( 1..^ n ) ( g `  l
) )  =  ( ( g `  m
)  \  U_ l  e.  ( 1..^ m ) ( g `  l
) ) )
7574eleq1d 2503 . . . . . . . . . . . . . . . . . 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 5688 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  m  ->  ( vol `  ( ( g `
 n )  \  U_ l  e.  (
1..^ n ) ( g `  l ) ) )  =  ( vol `  ( ( g `  m ) 
\  U_ l  e.  ( 1..^ m ) ( g `  l ) ) ) )
7776eleq1d 2503 . . . . . . . . . . . . . . . . . 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 710 . . . . . . . . . . . . . . . . 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 2941 . . . . . . . . . . . . . . . 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 249 . . . . . . . . . . . . . . 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 212 . . . . . . . . . . . . . 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 5684 . . . . . . . . . . . . . . . 16  |-  ( n  =  l  ->  (
g `  n )  =  ( g `  l ) )
8382iundisj2 20999 . . . . . . . . . . . . . . 15  |- Disj  n  e.  NN  ( ( g `
 n )  \  U_ l  e.  (
1..^ n ) ( g `  l ) )
84 disjeq2 4259 . . . . . . . . . . . . . . . 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 2779 . . . . . . . . . . . . . . 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 209 . . . . . . . . . . . . . 14  |- Disj  n  e.  NN  ( ( m  e.  NN  |->  ( ( g `  m ) 
\  U_ l  e.  ( 1..^ m ) ( g `  l ) ) ) `  n
)
87 nnex 10320 . . . . . . . . . . . . . . . . 17  |-  NN  e.  _V
8887mptex 5941 . . . . . . . . . . . . . . . 16  |-  ( m  e.  NN  |->  ( ( g `  m ) 
\  U_ l  e.  ( 1..^ m ) ( g `  l ) ) )  e.  _V
89 fveq1 5683 . . . . . . . . . . . . . . . . . . . . 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 2503 . . . . . . . . . . . . . . . . . . . 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 5688 . . . . . . . . . . . . . . . . . . . . 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 2503 . . . . . . . . . . . . . . . . . . . 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 710 . . . . . . . . . . . . . . . . . . 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 2729 . . . . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . . . . . . 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 4260 . . . . . . . . . . . . . . . . . 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 710 . . . . . . . . . . . . . . . . 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 4190 . . . . . . . . . . . . . . . . . . 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 5688 . . . . . . . . . . . . . . . . . 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 11803 . . . . . . . . . . . . . . . . . . . . . . 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 2457 . . . . . . . . . . . . . . . . . . . . 21  |-  S  =  seq 1 (  +  ,  ( n  e.  NN  |->  ( vol `  (
f `  n )
) ) )
105104rneqi 5058 . . . . . . . . . . . . . . . . . . . 20  |-  ran  S  =  ran  seq 1 (  +  ,  ( n  e.  NN  |->  ( vol `  ( f `  n
) ) ) )
106105supeq1i 7689 . . . . . . . . . . . . . . . . . . 19  |-  sup ( ran  S ,  RR* ,  <  )  =  sup ( ran 
seq 1 (  +  ,  ( n  e.  NN  |->  ( vol `  (
f `  n )
) ) ) , 
RR* ,  <  )
10791mpteq2dv 4372 . . . . . . . . . . . . . . . . . . . . . 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 11806 . . . . . . . . . . . . . . . . . . . . 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 5059 . . . . . . . . . . . . . . . . . . . 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 7688 . . . . . . . . . . . . . . . . . . 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 2481 . . . . . . . . . . . . . . . . . 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 2451 . . . . . . . . . . . . . . . . 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 320 . . . . . . . . . . . . . . . 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 3017 . . . . . . . . . . . . . . 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 4182 . . . . . . . . . . . . . . . 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 5687 . . . . . . . . . . . . . . 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 4367 . . . . . . . . . . . . . . . . . 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 11803 . . . . . . . . . . . . . . . . . 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 5058 . . . . . . . . . . . . . . . 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 7689 . . . . . . . . . . . . . . 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 2492 . . . . . . . . . . . . . 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 662 . . . . . . . . . . . . 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 466 . . . . . . . . . . . 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 20998 . . . . . . . . . . . . . . . 16  |-  U_ n  e.  NN  ( g `  n )  =  U_ n  e.  NN  (
( g `  n
)  \  U_ l  e.  ( 1..^ n ) ( g `  l
) )
127 fofun 5614 . . . . . . . . . . . . . . . . 17  |-  ( g : NN -onto-> A  ->  Fun  g )
128 funiunfv 5958 . . . . . . . . . . . . . . . . 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 2483 . . . . . . . . . . . . . . 15  |-  ( g : NN -onto-> A  ->  U_ n  e.  NN  ( ( g `  n )  \  U_ l  e.  ( 1..^ n ) ( g `
 l ) )  =  U. ( g
" NN ) )
13129unieqd 4094 . . . . . . . . . . . . . . 15  |-  ( g : NN -onto-> A  ->  U. ( g " NN )  =  U. A )
132130, 131eqtrd 2469 . . . . . . . . . . . . . 14  |-  ( g : NN -onto-> A  ->  U_ n  e.  NN  ( ( g `  n )  \  U_ l  e.  ( 1..^ n ) ( g `
 l ) )  =  U. A )
133132fveq2d 5688 . . . . . . . . . . . . 13  |-  ( g : NN -onto-> A  -> 
( vol `  U_ n  e.  NN  ( ( g `
 n )  \  U_ l  e.  (
1..^ n ) ( g `  l ) ) )  =  ( vol `  U. A
) )
134133adantr 465 . . . . . . . . . . . 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 3376 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  =  n  ->  (
( g `  m
)  C_  RR  <->  ( g `  n )  C_  RR ) )
13657fveq2d 5688 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( m  =  n  ->  ( vol* `  ( g `
 m ) )  =  ( vol* `  ( g `  n
) ) )
137136eqeq1d 2445 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  =  n  ->  (
( vol* `  ( g `  m
) )  =  0  <-> 
( vol* `  ( g `  n
) )  =  0 ) )
138135, 137anbi12d 710 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  n  ->  (
( ( g `  m )  C_  RR  /\  ( vol* `  ( g `  m
) )  =  0 )  <->  ( ( g `
 n )  C_  RR  /\  ( vol* `  ( g `  n
) )  =  0 ) ) )
139138rspccva 3065 . . . . . . . . . . . . . . . . . . 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 3480 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( g `  n ) 
C_  RR  ->  ( ( g `  n ) 
\  U_ l  e.  ( 1..^ n ) ( g `  l ) )  C_  RR )
141140adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( g `  n
)  C_  RR  /\  ( vol* `  ( g `
 n ) )  =  0 )  -> 
( ( g `  n )  \  U_ l  e.  ( 1..^ n ) ( g `
 l ) ) 
C_  RR )
142 difss 3476 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( g `  n ) 
\  U_ l  e.  ( 1..^ n ) ( g `  l ) )  C_  ( g `  n )
143 ovolssnul 20939 . . . . . . . . . . . . . . . . . . . . . . 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 1301 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( g `  n
)  C_  RR  /\  ( vol* `  ( g `
 n ) )  =  0 )  -> 
( vol* `  ( ( g `  n )  \  U_ l  e.  ( 1..^ n ) ( g `
 l ) ) )  =  0 )
145141, 144jca 532 . . . . . . . . . . . . . . . . . . . . 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 20986 . . . . . . . . . . . . . . . . . . . . 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 20982 . . . . . . . . . . . . . . . . . . . . 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 20 . . . . . . . . . . . . . . . . . . . 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 2469 . . . . . . . . . . . . . . . . . . 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 4371 . . . . . . . . . . . . . . . . 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 11806 . . . . . . . . . . . . . . . 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 5059 . . . . . . . . . . . . . . 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 7688 . . . . . . . . . . . . . 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 9370 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  CC
156 ser1const 11854 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 0  e.  CC  /\  m  e.  NN )  ->  (  seq 1 (  +  ,  ( NN 
X.  { 0 } ) ) `  m
)  =  ( m  x.  0 ) )
157155, 156mpan 670 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  e.  NN  ->  (  seq 1 (  +  , 
( NN  X.  {
0 } ) ) `
 m )  =  ( m  x.  0 ) )
158 nncn 10322 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( m  e.  NN  ->  m  e.  CC )
159158mul01d 9560 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  e.  NN  ->  (
m  x.  0 )  =  0 )
160157, 159eqtrd 2469 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  e.  NN  ->  (  seq 1 (  +  , 
( NN  X.  {
0 } ) ) `
 m )  =  0 )
161160mpteq2ia 4367 . . . . . . . . . . . . . . . . . . 19  |-  ( m  e.  NN  |->  (  seq 1 (  +  , 
( NN  X.  {
0 } ) ) `
 m ) )  =  ( m  e.  NN  |->  0 )
162 fconstmpt 4874 . . . . . . . . . . . . . . . . . . . . 21  |-  ( NN 
X.  { 0 } )  =  ( n  e.  NN  |->  0 )
163 seqeq3 11803 . . . . . . . . . . . . . . . . . . . . 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 10668 . . . . . . . . . . . . . . . . . . . . . 22  |-  1  e.  ZZ
166 seqfn 11810 . . . . . . . . . . . . . . . . . . . . . 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 10888 . . . . . . . . . . . . . . . . . . . . . . 23  |-  NN  =  ( ZZ>= `  1 )
169168fneq2i 5499 . . . . . . . . . . . . . . . . . . . . . 22  |-  (  seq 1 (  +  , 
( NN  X.  {
0 } ) )  Fn  NN  <->  seq 1
(  +  ,  ( NN  X.  { 0 } ) )  Fn  ( ZZ>= `  1 )
)
170 dffn5 5730 . . . . . . . . . . . . . . . . . . . . . 22  |-  (  seq 1 (  +  , 
( NN  X.  {
0 } ) )  Fn  NN  <->  seq 1
(  +  ,  ( NN  X.  { 0 } ) )  =  ( m  e.  NN  |->  (  seq 1 (  +  ,  ( NN  X.  { 0 } ) ) `  m ) ) )
171169, 170bitr3i 251 . . . . . . . . . . . . . . . . . . . . 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 208 . . . . . . . . . . . . . . . . . . . 20  |-  seq 1
(  +  ,  ( NN  X.  { 0 } ) )  =  ( m  e.  NN  |->  (  seq 1 (  +  ,  ( NN  X.  { 0 } ) ) `  m ) )
173164, 172eqtr3i 2459 . . . . . . . . . . . . . . . . . . 19  |-  seq 1
(  +  ,  ( n  e.  NN  |->  0 ) )  =  ( m  e.  NN  |->  (  seq 1 (  +  ,  ( NN  X.  { 0 } ) ) `  m ) )
174 fconstmpt 4874 . . . . . . . . . . . . . . . . . . 19  |-  ( NN 
X.  { 0 } )  =  ( m  e.  NN  |->  0 )
175161, 173, 1743eqtr4i 2467 . . . . . . . . . . . . . . . . . 18  |-  seq 1
(  +  ,  ( n  e.  NN  |->  0 ) )  =  ( NN  X.  { 0 } )
176175rneqi 5058 . . . . . . . . . . . . . . . . 17  |-  ran  seq 1 (  +  , 
( n  e.  NN  |->  0 ) )  =  ran  ( NN  X.  { 0 } )
177 1nn 10325 . . . . . . . . . . . . . . . . . 18  |-  1  e.  NN
178 ne0i 3636 . . . . . . . . . . . . . . . . . 18  |-  ( 1  e.  NN  ->  NN  =/=  (/) )
179 rnxp 5261 . . . . . . . . . . . . . . . . . 18  |-  ( NN  =/=  (/)  ->  ran  ( NN 
X.  { 0 } )  =  { 0 } )
180177, 178, 179mp2b 10 . . . . . . . . . . . . . . . . 17  |-  ran  ( NN  X.  { 0 } )  =  { 0 }
181176, 180eqtri 2457 . . . . . . . . . . . . . . . 16  |-  ran  seq 1 (  +  , 
( n  e.  NN  |->  0 ) )  =  { 0 }
182181supeq1i 7689 . . . . . . . . . . . . . . 15  |-  sup ( ran  seq 1 (  +  ,  ( n  e.  NN  |->  0 ) ) ,  RR* ,  <  )  =  sup ( { 0 } ,  RR* ,  <  )
183 xrltso 11110 . . . . . . . . . . . . . . . 16  |-  <  Or  RR*
184 0xr 9422 . . . . . . . . . . . . . . . 16  |-  0  e.  RR*
185 supsn 7711 . . . . . . . . . . . . . . . 16  |-  ( (  <  Or  RR*  /\  0  e.  RR* )  ->  sup ( { 0 } ,  RR* ,  <  )  =  0 )
186183, 184, 185mp2an 672 . . . . . . . . . . . . . . 15  |-  sup ( { 0 } ,  RR* ,  <  )  =  0
187182, 186eqtri 2457 . . . . . . . . . . . . . 14  |-  sup ( ran  seq 1 (  +  ,  ( n  e.  NN  |->  0 ) ) ,  RR* ,  <  )  =  0
188154, 187syl6eq 2485 . . . . . . . . . . . . 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 466 . . . . . . . . . . . 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 2478 . . . . . . . . . . 11  |-  ( ( g : NN -onto-> A  /\  A. m  e.  NN  ( ( g `  m )  C_  RR  /\  ( vol* `  ( g `  m
) )  =  0 ) )  ->  0  =  ( vol `  U. A ) )
191190ex 434 . . . . . . . . . 10  |-  ( g : NN -onto-> A  -> 
( A. m  e.  NN  ( ( g `
 m )  C_  RR  /\  ( vol* `  ( g `  m
) )  =  0 )  ->  0  =  ( vol `  U. A
) ) )
19239, 191sylbid 215 . . . . . . . . 9  |-  ( g : NN -onto-> A  -> 
( A. x  e.  A  ( x  C_  RR  /\  ( vol* `  x )  =  0 )  ->  0  =  ( vol `  U. A
) ) )
19328, 192syl5 32 . . . . . . . 8  |-  ( g : NN -onto-> A  -> 
( ( A. x  e.  A  x  ~<_  NN  /\  U. A  C_  RR )  ->  0  =  ( vol `  U. A ) ) )
194193exlimiv 1688 . . . . . . 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 603 . . . . 5  |-  ( A  =/=  (/)  ->  ( ( A  ~<_  NN  /\  ( A. x  e.  A  x  ~<_  NN  /\  U. A  C_  RR ) )  -> 
0  =  ( vol `  U. A ) ) )
19711, 196pm2.61ine 2681 . . . 4  |-  ( ( A  ~<_  NN  /\  ( A. x  e.  A  x  ~<_  NN  /\  U. A  C_  RR ) )  -> 
0  =  ( vol `  U. A ) )
198 renepnf 9423 . . . . . . 7  |-  ( 0  e.  RR  ->  0  =/= +oo )
19948, 198mp1i 12 . . . . . 6  |-  ( U. A  =  RR  ->  0  =/= +oo )
200 fveq2 5684 . . . . . . 7  |-  ( U. A  =  RR  ->  ( vol `  U. A
)  =  ( vol `  RR ) )
201 rembl 20991 . . . . . . . . 9  |-  RR  e.  dom  vol
202 mblvol 20982 . . . . . . . . 9  |-  ( RR  e.  dom  vol  ->  ( vol `  RR )  =  ( vol* `  RR ) )
203201, 202ax-mp 5 . . . . . . . 8  |-  ( vol `  RR )  =  ( vol* `  RR )
204 ovolre 20977 . . . . . . . 8  |-  ( vol* `  RR )  = +oo
205203, 204eqtri 2457 . . . . . . 7  |-  ( vol `  RR )  = +oo
206200, 205syl6eq 2485 . . . . . 6  |-  ( U. A  =  RR  ->  ( vol `  U. A
)  = +oo )
207199, 206neeqtrrd 2626 . . . . 5  |-  ( U. A  =  RR  ->  0  =/=  ( vol `  U. A ) )
208207necon2i 2652 . . . 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 615 . 2  |-  ( ( A  ~<_  NN  /\  A. x  e.  A  x  ~<_  NN )  ->  ( U. A  C_  RR  ->  U. A  =/= 
RR ) )
211 eqimss 3401 . . 3  |-  ( U. A  =  RR  ->  U. A  C_  RR )
212211necon3bi 2646 . 2  |-  ( -. 
U. A  C_  RR  ->  U. A  =/=  RR )
213210, 212pm2.61d1 159 1  |-  ( ( A  ~<_  NN  /\  A. x  e.  A  x  ~<_  NN )  ->  U. A  =/=  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1369   E.wex 1586    e. wcel 1756    =/= wne 2600   A.wral 2709   _Vcvv 2966    \ cdif 3318    C_ wss 3321   (/)c0 3630   {csn 3870   U.cuni 4084   U_ciun 4164  Disj wdisj 4255   class class class wbr 4285    e. cmpt 4343    Or wor 4632    X. cxp 4830   dom cdm 4832   ran crn 4833   "cima 4835   Fun wfun 5405    Fn wfn 5406   -onto->wfo 5409   ` cfv 5411  (class class class)co 6086    ~<_ cdom 7300    ~< csdm 7301   supcsup 7682   CCcc 9272   RRcr 9273   0cc0 9274   1c1 9275    + caddc 9277    x. cmul 9279   +oocpnf 9407   RR*cxr 9409    < clt 9410   NNcn 10314   ZZcz 10638   ZZ>=cuz 10853  ..^cfzo 11540    seqcseq 11798   vol*covol 20915   volcvol 20916
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418  ax-rep 4396  ax-sep 4406  ax-nul 4414  ax-pow 4463  ax-pr 4524  ax-un 6367  ax-inf2 7839  ax-cnex 9330  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351  ax-pre-sup 9352
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-nel 2603  df-ral 2714  df-rex 2715  df-reu 2716  df-rmo 2717  df-rab 2718  df-v 2968  df-sbc 3180  df-csb 3282  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-pss 3337  df-nul 3631  df-if 3785  df-pw 3855  df-sn 3871  df-pr 3873  df-tp 3875  df-op 3877  df-uni 4085  df-int 4122  df-iun 4166  df-disj 4256  df-br 4286  df-opab 4344  df-mpt 4345  df-tr 4379  df-eprel 4624  df-id 4628  df-po 4633  df-so 4634  df-fr 4671  df-se 4672  df-we 4673  df-ord 4714  df-on 4715  df-lim 4716  df-suc 4717  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5374  df-fun 5413  df-fn 5414  df-f 5415  df-f1 5416  df-fo 5417  df-f1o 5418  df-fv 5419  df-isom 5420  df-riota 6045  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-of 6315  df-om 6472  df-1st 6572  df-2nd 6573  df-recs 6824  df-rdg 6858  df-1o 6912  df-2o 6913  df-oadd 6916  df-er 7093  df-map 7208  df-en 7303  df-dom 7304  df-sdom 7305  df-fin 7306  df-fi 7653  df-sup 7683  df-oi 7716  df-card 8101  df-cda 8329  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-div 9986  df-nn 10315  df-2 10372  df-3 10373  df-n0 10572  df-z 10639  df-uz 10854  df-q 10946  df-rp 10984  df-xneg 11081  df-xadd 11082  df-xmul 11083  df-ioo 11296  df-ico 11298  df-icc 11299  df-fz 11430  df-fzo 11541  df-fl 11634  df-seq 11799  df-exp 11858  df-hash 12096  df-cj 12580  df-re 12581  df-im 12582  df-sqr 12716  df-abs 12717  df-clim 12958  df-sum 13156  df-rest 14353  df-topgen 14374  df-psmet 17778  df-xmet 17779  df-met 17780  df-bl 17781  df-mopn 17782  df-top 18472  df-bases 18474  df-topon 18475  df-cmp 18959  df-ovol 20917  df-vol 20918
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator