Metamath Proof Explorer

Theorem voliunnfl

Description: voliun 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)

Ref Expression
Hypotheses 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 voliunnfl 
|- ( ( A ~<_ NN /\ A. x e. A x ~<_ NN ) -> U. A =/= RR )

Proof

Step Hyp Ref Expression
1 voliunnfl.1 
 |-  S = seq 1 ( + , G )
2 voliunnfl.2 
 |-  G = ( n e. NN |-> ( vol ` ( f ` n ) ) )
3 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* , < ) )
4 unieq 
 |-  ( A = (/) -> U. A = U. (/) )
5 uni0 
 |-  U. (/) = (/)
6 4 5 eqtrdi 
 |-  ( A = (/) -> U. A = (/) )
7 6 fveq2d 
 |-  ( A = (/) -> ( vol ` U. A ) = ( vol ` (/) ) )
8 0mbl 
 |-  (/) e. dom vol
9 mblvol 
 |-  ( (/) e. dom vol -> ( vol ` (/) ) = ( vol* ` (/) ) )
10 8 9 ax-mp 
 |-  ( vol ` (/) ) = ( vol* ` (/) )
11 ovol0 
 |-  ( vol* ` (/) ) = 0
12 10 11 eqtri 
 |-  ( vol ` (/) ) = 0
13 7 12 eqtr2di 
 |-  ( A = (/) -> 0 = ( vol ` U. A ) )
14 13 a1d 
 |-  ( A = (/) -> ( ( A ~<_ NN /\ ( A. x e. A x ~<_ NN /\ U. A C_ RR ) ) -> 0 = ( vol ` U. A ) ) )
15 reldom 
 |-  Rel ~<_
16 15 brrelex1i 
 |-  ( A ~<_ NN -> A e. _V )
17 0sdomg 
 |-  ( A e. _V -> ( (/) ~< A <-> A =/= (/) ) )
18 16 17 syl 
 |-  ( A ~<_ NN -> ( (/) ~< A <-> A =/= (/) ) )
19 18 biimparc 
 |-  ( ( A =/= (/) /\ A ~<_ NN ) -> (/) ~< A )
20 fodomr 
 |-  ( ( (/) ~< A /\ A ~<_ NN ) -> E. g g : NN -onto-> A )
21 19 20 sylancom 
 |-  ( ( A =/= (/) /\ A ~<_ NN ) -> E. g g : NN -onto-> A )
22 unissb 
 |-  ( U. A C_ RR <-> A. x e. A x C_ RR )
23 22 anbi1i 
 |-  ( ( U. A C_ RR /\ A. x e. A x ~<_ NN ) <-> ( A. x e. A x C_ RR /\ A. x e. A x ~<_ NN ) )
24 r19.26 
 |-  ( A. x e. A ( x C_ RR /\ x ~<_ NN ) <-> ( A. x e. A x C_ RR /\ A. x e. A x ~<_ NN ) )
25 23 24 bitr4i 
 |-  ( ( U. A C_ RR /\ A. x e. A x ~<_ NN ) <-> A. x e. A ( x C_ RR /\ x ~<_ NN ) )
26 ovolctb2 
 |-  ( ( x C_ RR /\ x ~<_ NN ) -> ( vol* ` x ) = 0 )
27 26 ex 
 |-  ( x C_ RR -> ( x ~<_ NN -> ( vol* ` x ) = 0 ) )
28 27 imdistani 
 |-  ( ( x C_ RR /\ x ~<_ NN ) -> ( x C_ RR /\ ( vol* ` x ) = 0 ) )
29 28 ralimi 
 |-  ( A. x e. A ( x C_ RR /\ x ~<_ NN ) -> A. x e. A ( x C_ RR /\ ( vol* ` x ) = 0 ) )
30 25 29 sylbi 
 |-  ( ( U. A C_ RR /\ A. x e. A x ~<_ NN ) -> A. x e. A ( x C_ RR /\ ( vol* ` x ) = 0 ) )
31 30 ancoms 
 |-  ( ( A. x e. A x ~<_ NN /\ U. A C_ RR ) -> A. x e. A ( x C_ RR /\ ( vol* ` x ) = 0 ) )
32 foima 
 |-  ( g : NN -onto-> A -> ( g " NN ) = A )
33 32 raleqdv 
 |-  ( 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 ) ) )
34 fofn 
 |-  ( g : NN -onto-> A -> g Fn NN )
35 ssid 
 |-  NN C_ NN
36 sseq1 
 |-  ( x = ( g ` m ) -> ( x C_ RR <-> ( g ` m ) C_ RR ) )
37 fveqeq2 
 |-  ( x = ( g ` m ) -> ( ( vol* ` x ) = 0 <-> ( vol* ` ( g ` m ) ) = 0 ) )
38 36 37 anbi12d 
 |-  ( x = ( g ` m ) -> ( ( x C_ RR /\ ( vol* ` x ) = 0 ) <-> ( ( g ` m ) C_ RR /\ ( vol* ` ( g ` m ) ) = 0 ) ) )
39 38 ralima 
 |-  ( ( 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 ) ) )
40 34 35 39 sylancl 
 |-  ( 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 ) ) )
41 33 40 bitr3d 
 |-  ( 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 ) ) )
42 difss 
 |-  ( ( g ` m ) \ U_ l e. ( 1 ..^ m ) ( g ` l ) ) C_ ( g ` m )
43 ovolssnul 
 |-  ( ( ( ( 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 )
44 42 43 mp3an1 
 |-  ( ( ( g ` m ) C_ RR /\ ( vol* ` ( g ` m ) ) = 0 ) -> ( vol* ` ( ( g ` m ) \ U_ l e. ( 1 ..^ m ) ( g ` l ) ) ) = 0 )
45 ssdifss 
 |-  ( ( g ` m ) C_ RR -> ( ( g ` m ) \ U_ l e. ( 1 ..^ m ) ( g ` l ) ) C_ RR )
46 nulmbl 
 |-  ( ( ( ( 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 )
47 mblvol 
 |-  ( ( ( 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 ) ) ) )
48 47 eqeq1d 
 |-  ( ( ( 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 ) )
49 48 biimpar 
 |-  ( ( ( ( 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 )
50 0re 
 |-  0 e. RR
51 49 50 eqeltrdi 
 |-  ( ( ( ( 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 )
52 51 expcom 
 |-  ( ( 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 ) )
53 52 ancld 
 |-  ( ( 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 ) ) )
54 53 adantl 
 |-  ( ( ( ( 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 ) ) )
55 46 54 mpd 
 |-  ( ( ( ( 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 ) )
56 45 55 sylan 
 |-  ( ( ( 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 ) )
57 44 56 syldan 
 |-  ( ( ( 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 ) )
58 57 ralimi 
 |-  ( 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 ) )
59 fveq2 
 |-  ( m = n -> ( g ` m ) = ( g ` n ) )
60 oveq2 
 |-  ( m = n -> ( 1 ..^ m ) = ( 1 ..^ n ) )
61 60 iuneq1d 
 |-  ( m = n -> U_ l e. ( 1 ..^ m ) ( g ` l ) = U_ l e. ( 1 ..^ n ) ( g ` l ) )
62 59 61 difeq12d 
 |-  ( m = n -> ( ( g ` m ) \ U_ l e. ( 1 ..^ m ) ( g ` l ) ) = ( ( g ` n ) \ U_ l e. ( 1 ..^ n ) ( g ` l ) ) )
63 eqid 
 |-  ( m e. NN |-> ( ( g ` m ) \ U_ l e. ( 1 ..^ m ) ( g ` l ) ) ) = ( m e. NN |-> ( ( g ` m ) \ U_ l e. ( 1 ..^ m ) ( g ` l ) ) )
64 fvex 
 |-  ( g ` n ) e. _V
65 difexg 
 |-  ( ( g ` n ) e. _V -> ( ( g ` n ) \ U_ l e. ( 1 ..^ n ) ( g ` l ) ) e. _V )
66 64 65 ax-mp 
 |-  ( ( g ` n ) \ U_ l e. ( 1 ..^ n ) ( g ` l ) ) e. _V
67 62 63 66 fvmpt 
 |-  ( 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 ) ) )
68 67 eleq1d 
 |-  ( 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 ) )
69 67 fveq2d 
 |-  ( 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 ) ) ) )
70 69 eleq1d 
 |-  ( 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 ) )
71 68 70 anbi12d 
 |-  ( 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 ) ) )
72 71 ralbiia 
 |-  ( 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 ) )
73 fveq2 
 |-  ( n = m -> ( g ` n ) = ( g ` m ) )
74 oveq2 
 |-  ( n = m -> ( 1 ..^ n ) = ( 1 ..^ m ) )
75 74 iuneq1d 
 |-  ( n = m -> U_ l e. ( 1 ..^ n ) ( g ` l ) = U_ l e. ( 1 ..^ m ) ( g ` l ) )
76 73 75 difeq12d 
 |-  ( n = m -> ( ( g ` n ) \ U_ l e. ( 1 ..^ n ) ( g ` l ) ) = ( ( g ` m ) \ U_ l e. ( 1 ..^ m ) ( g ` l ) ) )
77 76 eleq1d 
 |-  ( 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 ) )
78 76 fveq2d 
 |-  ( n = m -> ( vol ` ( ( g ` n ) \ U_ l e. ( 1 ..^ n ) ( g ` l ) ) ) = ( vol ` ( ( g ` m ) \ U_ l e. ( 1 ..^ m ) ( g ` l ) ) ) )
79 78 eleq1d 
 |-  ( 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 ) )
80 77 79 anbi12d 
 |-  ( 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 ) ) )
81 80 cbvralvw 
 |-  ( 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 ) )
82 72 81 bitri 
 |-  ( 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 ) )
83 58 82 sylibr 
 |-  ( 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 ) )
84 fveq2 
 |-  ( n = l -> ( g ` n ) = ( g ` l ) )
85 84 iundisj2 
 |-  Disj_ n e. NN ( ( g ` n ) \ U_ l e. ( 1 ..^ n ) ( g ` l ) )
86 disjeq2 
 |-  ( 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 ) ) ) )
87 86 67 mprg 
 |-  ( 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 ) ) )
88 85 87 mpbir 
 |-  Disj_ n e. NN ( ( m e. NN |-> ( ( g ` m ) \ U_ l e. ( 1 ..^ m ) ( g ` l ) ) ) ` n )
89 nnex 
 |-  NN e. _V
90 89 mptex 
 |-  ( m e. NN |-> ( ( g ` m ) \ U_ l e. ( 1 ..^ m ) ( g ` l ) ) ) e. _V
91 fveq1 
 |-  ( 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 ) )
92 91 eleq1d 
 |-  ( 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 ) )
93 91 fveq2d 
 |-  ( 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 ) ) )
94 93 eleq1d 
 |-  ( 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 ) )
95 92 94 anbi12d 
 |-  ( 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 ) ) )
96 95 ralbidv 
 |-  ( 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 ) ) )
97 91 adantr 
 |-  ( ( 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 ) )
98 97 disjeq2dv 
 |-  ( 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 ) ) )
99 96 98 anbi12d 
 |-  ( 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 ) ) ) )
100 91 iuneq2d 
 |-  ( 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 ) )
101 100 fveq2d 
 |-  ( 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 ) ) )
102 seqeq3 
 |-  ( G = ( n e. NN |-> ( vol ` ( f ` n ) ) ) -> seq 1 ( + , G ) = seq 1 ( + , ( n e. NN |-> ( vol ` ( f ` n ) ) ) ) )
103 2 102 ax-mp 
 |-  seq 1 ( + , G ) = seq 1 ( + , ( n e. NN |-> ( vol ` ( f ` n ) ) ) )
104 1 103 eqtri 
 |-  S = seq 1 ( + , ( n e. NN |-> ( vol ` ( f ` n ) ) ) )
105 104 rneqi 
 |-  ran S = ran seq 1 ( + , ( n e. NN |-> ( vol ` ( f ` n ) ) ) )
106 105 supeq1i 
 |-  sup ( ran S , RR* , < ) = sup ( ran seq 1 ( + , ( n e. NN |-> ( vol ` ( f ` n ) ) ) ) , RR* , < )
107 93 mpteq2dv 
 |-  ( 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 ) ) ) )
108 107 seqeq3d 
 |-  ( 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 ) ) ) ) )
109 108 rneqd 
 |-  ( 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 ) ) ) ) )
110 109 supeq1d 
 |-  ( 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* , < ) )
111 106 110 syl5eq 
 |-  ( 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* , < ) )
112 101 111 eqeq12d 
 |-  ( 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* , < ) ) )
113 99 112 imbi12d 
 |-  ( 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 90 113 3 vtocl 
 |-  ( ( 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* , < ) )
115 67 iuneq2i 
 |-  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 ) )
116 115 fveq2i 
 |-  ( 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 ) ) )
117 69 mpteq2ia 
 |-  ( 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 ) ) ) )
118 seqeq3 
 |-  ( ( 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 ) ) ) ) ) )
119 117 118 ax-mp 
 |-  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 ) ) ) ) )
120 119 rneqi 
 |-  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 ) ) ) ) )
121 120 supeq1i 
 |-  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* , < )
122 114 116 121 3eqtr3g 
 |-  ( ( 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* , < ) )
123 83 88 122 sylancl 
 |-  ( 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* , < ) )
124 123 adantl 
 |-  ( ( 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* , < ) )
125 84 iundisj 
 |-  U_ n e. NN ( g ` n ) = U_ n e. NN ( ( g ` n ) \ U_ l e. ( 1 ..^ n ) ( g ` l ) )
126 fofun 
 |-  ( g : NN -onto-> A -> Fun g )
127 funiunfv 
 |-  ( Fun g -> U_ n e. NN ( g ` n ) = U. ( g " NN ) )
128 126 127 syl 
 |-  ( g : NN -onto-> A -> U_ n e. NN ( g ` n ) = U. ( g " NN ) )
129 125 128 eqtr3id 
 |-  ( g : NN -onto-> A -> U_ n e. NN ( ( g ` n ) \ U_ l e. ( 1 ..^ n ) ( g ` l ) ) = U. ( g " NN ) )
130 32 unieqd 
 |-  ( g : NN -onto-> A -> U. ( g " NN ) = U. A )
131 129 130 eqtrd 
 |-  ( g : NN -onto-> A -> U_ n e. NN ( ( g ` n ) \ U_ l e. ( 1 ..^ n ) ( g ` l ) ) = U. A )
132 131 fveq2d 
 |-  ( g : NN -onto-> A -> ( vol ` U_ n e. NN ( ( g ` n ) \ U_ l e. ( 1 ..^ n ) ( g ` l ) ) ) = ( vol ` U. A ) )
133 132 adantr 
 |-  ( ( 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 ) )
134 59 sseq1d 
 |-  ( m = n -> ( ( g ` m ) C_ RR <-> ( g ` n ) C_ RR ) )
135 59 fveqeq2d 
 |-  ( m = n -> ( ( vol* ` ( g ` m ) ) = 0 <-> ( vol* ` ( g ` n ) ) = 0 ) )
136 134 135 anbi12d 
 |-  ( m = n -> ( ( ( g ` m ) C_ RR /\ ( vol* ` ( g ` m ) ) = 0 ) <-> ( ( g ` n ) C_ RR /\ ( vol* ` ( g ` n ) ) = 0 ) ) )
137 136 rspccva 
 |-  ( ( A. m e. NN ( ( g ` m ) C_ RR /\ ( vol* ` ( g ` m ) ) = 0 ) /\ n e. NN ) -> ( ( g ` n ) C_ RR /\ ( vol* ` ( g ` n ) ) = 0 ) )
138 ssdifss 
 |-  ( ( g ` n ) C_ RR -> ( ( g ` n ) \ U_ l e. ( 1 ..^ n ) ( g ` l ) ) C_ RR )
139 138 adantr 
 |-  ( ( ( g ` n ) C_ RR /\ ( vol* ` ( g ` n ) ) = 0 ) -> ( ( g ` n ) \ U_ l e. ( 1 ..^ n ) ( g ` l ) ) C_ RR )
140 difss 
 |-  ( ( g ` n ) \ U_ l e. ( 1 ..^ n ) ( g ` l ) ) C_ ( g ` n )
141 ovolssnul 
 |-  ( ( ( ( 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 )
142 140 141 mp3an1 
 |-  ( ( ( g ` n ) C_ RR /\ ( vol* ` ( g ` n ) ) = 0 ) -> ( vol* ` ( ( g ` n ) \ U_ l e. ( 1 ..^ n ) ( g ` l ) ) ) = 0 )
143 139 142 jca 
 |-  ( ( ( 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 ) )
144 nulmbl 
 |-  ( ( ( ( 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 )
145 mblvol 
 |-  ( ( ( 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 ) ) ) )
146 143 144 145 3syl 
 |-  ( ( ( 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 ) ) ) )
147 146 142 eqtrd 
 |-  ( ( ( g ` n ) C_ RR /\ ( vol* ` ( g ` n ) ) = 0 ) -> ( vol ` ( ( g ` n ) \ U_ l e. ( 1 ..^ n ) ( g ` l ) ) ) = 0 )
148 137 147 syl 
 |-  ( ( 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 )
149 148 mpteq2dva 
 |-  ( 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 ) )
150 149 seqeq3d 
 |-  ( 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 ) ) )
151 150 rneqd 
 |-  ( 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 ) ) )
152 151 supeq1d 
 |-  ( 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* , < ) )
153 0cn 
 |-  0 e. CC
154 ser1const 
 |-  ( ( 0 e. CC /\ m e. NN ) -> ( seq 1 ( + , ( NN X. { 0 } ) ) ` m ) = ( m x. 0 ) )
155 153 154 mpan 
 |-  ( m e. NN -> ( seq 1 ( + , ( NN X. { 0 } ) ) ` m ) = ( m x. 0 ) )
156 nncn 
 |-  ( m e. NN -> m e. CC )
157 156 mul01d 
 |-  ( m e. NN -> ( m x. 0 ) = 0 )
158 155 157 eqtrd 
 |-  ( m e. NN -> ( seq 1 ( + , ( NN X. { 0 } ) ) ` m ) = 0 )
159 158 mpteq2ia 
 |-  ( m e. NN |-> ( seq 1 ( + , ( NN X. { 0 } ) ) ` m ) ) = ( m e. NN |-> 0 )
160 fconstmpt 
 |-  ( NN X. { 0 } ) = ( n e. NN |-> 0 )
161 seqeq3 
 |-  ( ( NN X. { 0 } ) = ( n e. NN |-> 0 ) -> seq 1 ( + , ( NN X. { 0 } ) ) = seq 1 ( + , ( n e. NN |-> 0 ) ) )
162 160 161 ax-mp 
 |-  seq 1 ( + , ( NN X. { 0 } ) ) = seq 1 ( + , ( n e. NN |-> 0 ) )
163 1z 
 |-  1 e. ZZ
164 seqfn 
 |-  ( 1 e. ZZ -> seq 1 ( + , ( NN X. { 0 } ) ) Fn ( ZZ>= ` 1 ) )
165 163 164 ax-mp 
 |-  seq 1 ( + , ( NN X. { 0 } ) ) Fn ( ZZ>= ` 1 )
166 nnuz 
 |-  NN = ( ZZ>= ` 1 )
167 166 fneq2i 
 |-  ( seq 1 ( + , ( NN X. { 0 } ) ) Fn NN <-> seq 1 ( + , ( NN X. { 0 } ) ) Fn ( ZZ>= ` 1 ) )
168 dffn5 
 |-  ( seq 1 ( + , ( NN X. { 0 } ) ) Fn NN <-> seq 1 ( + , ( NN X. { 0 } ) ) = ( m e. NN |-> ( seq 1 ( + , ( NN X. { 0 } ) ) ` m ) ) )
169 167 168 bitr3i 
 |-  ( seq 1 ( + , ( NN X. { 0 } ) ) Fn ( ZZ>= ` 1 ) <-> seq 1 ( + , ( NN X. { 0 } ) ) = ( m e. NN |-> ( seq 1 ( + , ( NN X. { 0 } ) ) ` m ) ) )
170 165 169 mpbi 
 |-  seq 1 ( + , ( NN X. { 0 } ) ) = ( m e. NN |-> ( seq 1 ( + , ( NN X. { 0 } ) ) ` m ) )
171 162 170 eqtr3i 
 |-  seq 1 ( + , ( n e. NN |-> 0 ) ) = ( m e. NN |-> ( seq 1 ( + , ( NN X. { 0 } ) ) ` m ) )
172 fconstmpt 
 |-  ( NN X. { 0 } ) = ( m e. NN |-> 0 )
173 159 171 172 3eqtr4i 
 |-  seq 1 ( + , ( n e. NN |-> 0 ) ) = ( NN X. { 0 } )
174 173 rneqi 
 |-  ran seq 1 ( + , ( n e. NN |-> 0 ) ) = ran ( NN X. { 0 } )
175 1nn 
 |-  1 e. NN
176 ne0i 
 |-  ( 1 e. NN -> NN =/= (/) )
177 rnxp 
 |-  ( NN =/= (/) -> ran ( NN X. { 0 } ) = { 0 } )
178 175 176 177 mp2b 
 |-  ran ( NN X. { 0 } ) = { 0 }
179 174 178 eqtri 
 |-  ran seq 1 ( + , ( n e. NN |-> 0 ) ) = { 0 }
180 179 supeq1i 
 |-  sup ( ran seq 1 ( + , ( n e. NN |-> 0 ) ) , RR* , < ) = sup ( { 0 } , RR* , < )
181 xrltso 
 |-  < Or RR*
182 0xr 
 |-  0 e. RR*
183 supsn 
 |-  ( ( < Or RR* /\ 0 e. RR* ) -> sup ( { 0 } , RR* , < ) = 0 )
184 181 182 183 mp2an 
 |-  sup ( { 0 } , RR* , < ) = 0
185 180 184 eqtri 
 |-  sup ( ran seq 1 ( + , ( n e. NN |-> 0 ) ) , RR* , < ) = 0
186 152 185 eqtrdi 
 |-  ( 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 )
187 186 adantl 
 |-  ( ( 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 )
188 124 133 187 3eqtr3rd 
 |-  ( ( g : NN -onto-> A /\ A. m e. NN ( ( g ` m ) C_ RR /\ ( vol* ` ( g ` m ) ) = 0 ) ) -> 0 = ( vol ` U. A ) )
189 188 ex 
 |-  ( g : NN -onto-> A -> ( A. m e. NN ( ( g ` m ) C_ RR /\ ( vol* ` ( g ` m ) ) = 0 ) -> 0 = ( vol ` U. A ) ) )
190 41 189 sylbid 
 |-  ( g : NN -onto-> A -> ( A. x e. A ( x C_ RR /\ ( vol* ` x ) = 0 ) -> 0 = ( vol ` U. A ) ) )
191 31 190 syl5 
 |-  ( g : NN -onto-> A -> ( ( A. x e. A x ~<_ NN /\ U. A C_ RR ) -> 0 = ( vol ` U. A ) ) )
192 191 exlimiv 
 |-  ( E. g g : NN -onto-> A -> ( ( A. x e. A x ~<_ NN /\ U. A C_ RR ) -> 0 = ( vol ` U. A ) ) )
193 21 192 syl 
 |-  ( ( A =/= (/) /\ A ~<_ NN ) -> ( ( A. x e. A x ~<_ NN /\ U. A C_ RR ) -> 0 = ( vol ` U. A ) ) )
194 193 expimpd 
 |-  ( A =/= (/) -> ( ( A ~<_ NN /\ ( A. x e. A x ~<_ NN /\ U. A C_ RR ) ) -> 0 = ( vol ` U. A ) ) )
195 14 194 pm2.61ine 
 |-  ( ( A ~<_ NN /\ ( A. x e. A x ~<_ NN /\ U. A C_ RR ) ) -> 0 = ( vol ` U. A ) )
196 renepnf 
 |-  ( 0 e. RR -> 0 =/= +oo )
197 50 196 mp1i 
 |-  ( U. A = RR -> 0 =/= +oo )
198 fveq2 
 |-  ( U. A = RR -> ( vol ` U. A ) = ( vol ` RR ) )
199 rembl 
 |-  RR e. dom vol
200 mblvol 
 |-  ( RR e. dom vol -> ( vol ` RR ) = ( vol* ` RR ) )
201 199 200 ax-mp 
 |-  ( vol ` RR ) = ( vol* ` RR )
202 ovolre 
 |-  ( vol* ` RR ) = +oo
203 201 202 eqtri 
 |-  ( vol ` RR ) = +oo
204 198 203 eqtrdi 
 |-  ( U. A = RR -> ( vol ` U. A ) = +oo )
205 197 204 neeqtrrd 
 |-  ( U. A = RR -> 0 =/= ( vol ` U. A ) )
206 205 necon2i 
 |-  ( 0 = ( vol ` U. A ) -> U. A =/= RR )
207 195 206 syl 
 |-  ( ( A ~<_ NN /\ ( A. x e. A x ~<_ NN /\ U. A C_ RR ) ) -> U. A =/= RR )
208 207 expr 
 |-  ( ( A ~<_ NN /\ A. x e. A x ~<_ NN ) -> ( U. A C_ RR -> U. A =/= RR ) )
209 eqimss 
 |-  ( U. A = RR -> U. A C_ RR )
210 209 necon3bi 
 |-  ( -. U. A C_ RR -> U. A =/= RR )
211 208 210 pm2.61d1 
 |-  ( ( A ~<_ NN /\ A. x e. A x ~<_ NN ) -> U. A =/= RR )