Metamath Proof Explorer

Theorem volsupnfl

Description: volsup is incompatible with the Feferman-Levy model. (Contributed by Brendan Leahy, 2-Jan-2018)

Ref Expression
Hypothesis volsupnfl.0 
|- ( ( f : NN --> dom vol /\ A. n e. NN ( f ` n ) C_ ( f ` ( n + 1 ) ) ) -> ( vol ` U. ran f ) = sup ( ( vol " ran f ) , RR* , < ) )
Assertion volsupnfl 
|- ( ( A ~<_ NN /\ A. x e. A x ~<_ NN ) -> U. A =/= RR )

Proof

Step Hyp Ref Expression
1 volsupnfl.0 
 |-  ( ( f : NN --> dom vol /\ A. n e. NN ( f ` n ) C_ ( f ` ( n + 1 ) ) ) -> ( vol ` U. ran f ) = sup ( ( vol " ran f ) , RR* , < ) )
2 unieq 
 |-  ( A = (/) -> U. A = U. (/) )
3 uni0 
 |-  U. (/) = (/)
4 2 3 eqtrdi 
 |-  ( A = (/) -> U. A = (/) )
5 4 fveq2d 
 |-  ( A = (/) -> ( vol ` U. A ) = ( vol ` (/) ) )
6 0mbl 
 |-  (/) e. dom vol
7 mblvol 
 |-  ( (/) e. dom vol -> ( vol ` (/) ) = ( vol* ` (/) ) )
8 6 7 ax-mp 
 |-  ( vol ` (/) ) = ( vol* ` (/) )
9 ovol0 
 |-  ( vol* ` (/) ) = 0
10 8 9 eqtri 
 |-  ( vol ` (/) ) = 0
11 5 10 eqtr2di 
 |-  ( A = (/) -> 0 = ( vol ` U. A ) )
12 11 a1d 
 |-  ( A = (/) -> ( ( A ~<_ NN /\ ( A. x e. A x ~<_ NN /\ U. A C_ RR ) ) -> 0 = ( vol ` U. A ) ) )
13 reldom 
 |-  Rel ~<_
14 13 brrelex1i 
 |-  ( A ~<_ NN -> A e. _V )
15 0sdomg 
 |-  ( A e. _V -> ( (/) ~< A <-> A =/= (/) ) )
16 14 15 syl 
 |-  ( A ~<_ NN -> ( (/) ~< A <-> A =/= (/) ) )
17 16 biimparc 
 |-  ( ( A =/= (/) /\ A ~<_ NN ) -> (/) ~< A )
18 fodomr 
 |-  ( ( (/) ~< A /\ A ~<_ NN ) -> E. g g : NN -onto-> A )
19 17 18 sylancom 
 |-  ( ( A =/= (/) /\ A ~<_ NN ) -> E. g g : NN -onto-> A )
20 unissb 
 |-  ( U. A C_ RR <-> A. x e. A x C_ RR )
21 20 anbi1i 
 |-  ( ( U. A C_ RR /\ A. x e. A x ~<_ NN ) <-> ( A. x e. A x C_ RR /\ A. x e. A x ~<_ NN ) )
22 r19.26 
 |-  ( A. x e. A ( x C_ RR /\ x ~<_ NN ) <-> ( A. x e. A x C_ RR /\ A. x e. A x ~<_ NN ) )
23 21 22 bitr4i 
 |-  ( ( U. A C_ RR /\ A. x e. A x ~<_ NN ) <-> A. x e. A ( x C_ RR /\ x ~<_ NN ) )
24 ovolctb2 
 |-  ( ( x C_ RR /\ x ~<_ NN ) -> ( vol* ` x ) = 0 )
25 nulmbl 
 |-  ( ( x C_ RR /\ ( vol* ` x ) = 0 ) -> x e. dom vol )
26 mblvol 
 |-  ( x e. dom vol -> ( vol ` x ) = ( vol* ` x ) )
27 eqtr 
 |-  ( ( ( vol ` x ) = ( vol* ` x ) /\ ( vol* ` x ) = 0 ) -> ( vol ` x ) = 0 )
28 27 expcom 
 |-  ( ( vol* ` x ) = 0 -> ( ( vol ` x ) = ( vol* ` x ) -> ( vol ` x ) = 0 ) )
29 26 28 syl5 
 |-  ( ( vol* ` x ) = 0 -> ( x e. dom vol -> ( vol ` x ) = 0 ) )
30 29 adantl 
 |-  ( ( x C_ RR /\ ( vol* ` x ) = 0 ) -> ( x e. dom vol -> ( vol ` x ) = 0 ) )
31 25 30 jcai 
 |-  ( ( x C_ RR /\ ( vol* ` x ) = 0 ) -> ( x e. dom vol /\ ( vol ` x ) = 0 ) )
32 24 31 syldan 
 |-  ( ( x C_ RR /\ x ~<_ NN ) -> ( x e. dom vol /\ ( vol ` x ) = 0 ) )
33 32 ralimi 
 |-  ( A. x e. A ( x C_ RR /\ x ~<_ NN ) -> A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) )
34 23 33 sylbi 
 |-  ( ( U. A C_ RR /\ A. x e. A x ~<_ NN ) -> A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) )
35 34 ancoms 
 |-  ( ( A. x e. A x ~<_ NN /\ U. A C_ RR ) -> A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) )
36 fzfi 
 |-  ( 1 ... m ) e. Fin
37 fzssuz 
 |-  ( 1 ... m ) C_ ( ZZ>= ` 1 )
38 nnuz 
 |-  NN = ( ZZ>= ` 1 )
39 37 38 sseqtrri 
 |-  ( 1 ... m ) C_ NN
40 fof 
 |-  ( g : NN -onto-> A -> g : NN --> A )
41 40 ffvelcdmda 
 |-  ( ( g : NN -onto-> A /\ l e. NN ) -> ( g ` l ) e. A )
42 eleq1 
 |-  ( x = ( g ` l ) -> ( x e. dom vol <-> ( g ` l ) e. dom vol ) )
43 fveqeq2 
 |-  ( x = ( g ` l ) -> ( ( vol ` x ) = 0 <-> ( vol ` ( g ` l ) ) = 0 ) )
44 42 43 anbi12d 
 |-  ( x = ( g ` l ) -> ( ( x e. dom vol /\ ( vol ` x ) = 0 ) <-> ( ( g ` l ) e. dom vol /\ ( vol ` ( g ` l ) ) = 0 ) ) )
45 44 rspccva 
 |-  ( ( A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) /\ ( g ` l ) e. A ) -> ( ( g ` l ) e. dom vol /\ ( vol ` ( g ` l ) ) = 0 ) )
46 45 simpld 
 |-  ( ( A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) /\ ( g ` l ) e. A ) -> ( g ` l ) e. dom vol )
47 46 ancoms 
 |-  ( ( ( g ` l ) e. A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) -> ( g ` l ) e. dom vol )
48 41 47 sylan 
 |-  ( ( ( g : NN -onto-> A /\ l e. NN ) /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) -> ( g ` l ) e. dom vol )
49 48 an32s 
 |-  ( ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) /\ l e. NN ) -> ( g ` l ) e. dom vol )
50 49 ralrimiva 
 |-  ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) -> A. l e. NN ( g ` l ) e. dom vol )
51 ssralv 
 |-  ( ( 1 ... m ) C_ NN -> ( A. l e. NN ( g ` l ) e. dom vol -> A. l e. ( 1 ... m ) ( g ` l ) e. dom vol ) )
52 39 50 51 mpsyl 
 |-  ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) -> A. l e. ( 1 ... m ) ( g ` l ) e. dom vol )
53 finiunmbl 
 |-  ( ( ( 1 ... m ) e. Fin /\ A. l e. ( 1 ... m ) ( g ` l ) e. dom vol ) -> U_ l e. ( 1 ... m ) ( g ` l ) e. dom vol )
54 36 52 53 sylancr 
 |-  ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) -> U_ l e. ( 1 ... m ) ( g ` l ) e. dom vol )
55 54 adantr 
 |-  ( ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) /\ m e. NN ) -> U_ l e. ( 1 ... m ) ( g ` l ) e. dom vol )
56 55 fmpttd 
 |-  ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) -> ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) : NN --> dom vol )
57 fzssp1 
 |-  ( 1 ... n ) C_ ( 1 ... ( n + 1 ) )
58 iunss1 
 |-  ( ( 1 ... n ) C_ ( 1 ... ( n + 1 ) ) -> U_ l e. ( 1 ... n ) ( g ` l ) C_ U_ l e. ( 1 ... ( n + 1 ) ) ( g ` l ) )
59 57 58 ax-mp 
 |-  U_ l e. ( 1 ... n ) ( g ` l ) C_ U_ l e. ( 1 ... ( n + 1 ) ) ( g ` l )
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 eqid 
 |-  ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) = ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) )
63 ovex 
 |-  ( 1 ... n ) e. _V
64 fvex 
 |-  ( g ` l ) e. _V
65 63 64 iunex 
 |-  U_ l e. ( 1 ... n ) ( g ` l ) e. _V
66 61 62 65 fvmpt 
 |-  ( n e. NN -> ( ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ` n ) = U_ l e. ( 1 ... n ) ( g ` l ) )
67 peano2nn 
 |-  ( n e. NN -> ( n + 1 ) e. NN )
68 oveq2 
 |-  ( m = ( n + 1 ) -> ( 1 ... m ) = ( 1 ... ( n + 1 ) ) )
69 68 iuneq1d 
 |-  ( m = ( n + 1 ) -> U_ l e. ( 1 ... m ) ( g ` l ) = U_ l e. ( 1 ... ( n + 1 ) ) ( g ` l ) )
70 ovex 
 |-  ( 1 ... ( n + 1 ) ) e. _V
71 70 64 iunex 
 |-  U_ l e. ( 1 ... ( n + 1 ) ) ( g ` l ) e. _V
72 69 62 71 fvmpt 
 |-  ( ( n + 1 ) e. NN -> ( ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ` ( n + 1 ) ) = U_ l e. ( 1 ... ( n + 1 ) ) ( g ` l ) )
73 67 72 syl 
 |-  ( n e. NN -> ( ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ` ( n + 1 ) ) = U_ l e. ( 1 ... ( n + 1 ) ) ( g ` l ) )
74 66 73 sseq12d 
 |-  ( n e. NN -> ( ( ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ` n ) C_ ( ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ` ( n + 1 ) ) <-> U_ l e. ( 1 ... n ) ( g ` l ) C_ U_ l e. ( 1 ... ( n + 1 ) ) ( g ` l ) ) )
75 59 74 mpbiri 
 |-  ( n e. NN -> ( ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ` n ) C_ ( ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ` ( n + 1 ) ) )
76 75 rgen 
 |-  A. n e. NN ( ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ` n ) C_ ( ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ` ( n + 1 ) )
77 nnex 
 |-  NN e. _V
78 77 mptex 
 |-  ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) e. _V
79 feq1 
 |-  ( f = ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) -> ( f : NN --> dom vol <-> ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) : NN --> dom vol ) )
80 fveq1 
 |-  ( f = ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) -> ( f ` n ) = ( ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ` n ) )
81 fveq1 
 |-  ( f = ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) -> ( f ` ( n + 1 ) ) = ( ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ` ( n + 1 ) ) )
82 80 81 sseq12d 
 |-  ( f = ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) -> ( ( f ` n ) C_ ( f ` ( n + 1 ) ) <-> ( ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ` n ) C_ ( ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ` ( n + 1 ) ) ) )
83 82 ralbidv 
 |-  ( f = ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) -> ( A. n e. NN ( f ` n ) C_ ( f ` ( n + 1 ) ) <-> A. n e. NN ( ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ` n ) C_ ( ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ` ( n + 1 ) ) ) )
84 79 83 anbi12d 
 |-  ( f = ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) -> ( ( f : NN --> dom vol /\ A. n e. NN ( f ` n ) C_ ( f ` ( n + 1 ) ) ) <-> ( ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) : NN --> dom vol /\ A. n e. NN ( ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ` n ) C_ ( ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ` ( n + 1 ) ) ) ) )
85 rneq 
 |-  ( f = ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) -> ran f = ran ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) )
86 85 unieqd 
 |-  ( f = ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) -> U. ran f = U. ran ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) )
87 86 fveq2d 
 |-  ( f = ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) -> ( vol ` U. ran f ) = ( vol ` U. ran ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ) )
88 85 imaeq2d 
 |-  ( f = ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) -> ( vol " ran f ) = ( vol " ran ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ) )
89 88 supeq1d 
 |-  ( f = ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) -> sup ( ( vol " ran f ) , RR* , < ) = sup ( ( vol " ran ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ) , RR* , < ) )
90 87 89 eqeq12d 
 |-  ( f = ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) -> ( ( vol ` U. ran f ) = sup ( ( vol " ran f ) , RR* , < ) <-> ( vol ` U. ran ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ) = sup ( ( vol " ran ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ) , RR* , < ) ) )
91 84 90 imbi12d 
 |-  ( f = ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) -> ( ( ( f : NN --> dom vol /\ A. n e. NN ( f ` n ) C_ ( f ` ( n + 1 ) ) ) -> ( vol ` U. ran f ) = sup ( ( vol " ran f ) , RR* , < ) ) <-> ( ( ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) : NN --> dom vol /\ A. n e. NN ( ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ` n ) C_ ( ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ` ( n + 1 ) ) ) -> ( vol ` U. ran ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ) = sup ( ( vol " ran ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ) , RR* , < ) ) ) )
92 78 91 1 vtocl 
 |-  ( ( ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) : NN --> dom vol /\ A. n e. NN ( ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ` n ) C_ ( ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ` ( n + 1 ) ) ) -> ( vol ` U. ran ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ) = sup ( ( vol " ran ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ) , RR* , < ) )
93 56 76 92 sylancl 
 |-  ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) -> ( vol ` U. ran ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ) = sup ( ( vol " ran ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ) , RR* , < ) )
94 df-iun 
 |-  U_ x e. NN ( g ` x ) = { n | E. x e. NN n e. ( g ` x ) }
95 eluzfz2 
 |-  ( x e. ( ZZ>= ` 1 ) -> x e. ( 1 ... x ) )
96 95 38 eleq2s 
 |-  ( x e. NN -> x e. ( 1 ... x ) )
97 fveq2 
 |-  ( l = x -> ( g ` l ) = ( g ` x ) )
98 97 eleq2d 
 |-  ( l = x -> ( n e. ( g ` l ) <-> n e. ( g ` x ) ) )
99 98 rspcev 
 |-  ( ( x e. ( 1 ... x ) /\ n e. ( g ` x ) ) -> E. l e. ( 1 ... x ) n e. ( g ` l ) )
100 96 99 sylan 
 |-  ( ( x e. NN /\ n e. ( g ` x ) ) -> E. l e. ( 1 ... x ) n e. ( g ` l ) )
101 oveq2 
 |-  ( m = x -> ( 1 ... m ) = ( 1 ... x ) )
102 101 rexeqdv 
 |-  ( m = x -> ( E. l e. ( 1 ... m ) n e. ( g ` l ) <-> E. l e. ( 1 ... x ) n e. ( g ` l ) ) )
103 102 rspcev 
 |-  ( ( x e. NN /\ E. l e. ( 1 ... x ) n e. ( g ` l ) ) -> E. m e. NN E. l e. ( 1 ... m ) n e. ( g ` l ) )
104 100 103 syldan 
 |-  ( ( x e. NN /\ n e. ( g ` x ) ) -> E. m e. NN E. l e. ( 1 ... m ) n e. ( g ` l ) )
105 104 rexlimiva 
 |-  ( E. x e. NN n e. ( g ` x ) -> E. m e. NN E. l e. ( 1 ... m ) n e. ( g ` l ) )
106 ssrexv 
 |-  ( ( 1 ... m ) C_ NN -> ( E. l e. ( 1 ... m ) n e. ( g ` l ) -> E. l e. NN n e. ( g ` l ) ) )
107 39 106 ax-mp 
 |-  ( E. l e. ( 1 ... m ) n e. ( g ` l ) -> E. l e. NN n e. ( g ` l ) )
108 98 cbvrexvw 
 |-  ( E. l e. NN n e. ( g ` l ) <-> E. x e. NN n e. ( g ` x ) )
109 107 108 sylib 
 |-  ( E. l e. ( 1 ... m ) n e. ( g ` l ) -> E. x e. NN n e. ( g ` x ) )
110 109 rexlimivw 
 |-  ( E. m e. NN E. l e. ( 1 ... m ) n e. ( g ` l ) -> E. x e. NN n e. ( g ` x ) )
111 105 110 impbii 
 |-  ( E. x e. NN n e. ( g ` x ) <-> E. m e. NN E. l e. ( 1 ... m ) n e. ( g ` l ) )
112 eliun 
 |-  ( n e. U_ l e. ( 1 ... m ) ( g ` l ) <-> E. l e. ( 1 ... m ) n e. ( g ` l ) )
113 112 rexbii 
 |-  ( E. m e. NN n e. U_ l e. ( 1 ... m ) ( g ` l ) <-> E. m e. NN E. l e. ( 1 ... m ) n e. ( g ` l ) )
114 111 113 bitr4i 
 |-  ( E. x e. NN n e. ( g ` x ) <-> E. m e. NN n e. U_ l e. ( 1 ... m ) ( g ` l ) )
115 114 abbii 
 |-  { n | E. x e. NN n e. ( g ` x ) } = { n | E. m e. NN n e. U_ l e. ( 1 ... m ) ( g ` l ) }
116 94 115 eqtri 
 |-  U_ x e. NN ( g ` x ) = { n | E. m e. NN n e. U_ l e. ( 1 ... m ) ( g ` l ) }
117 df-iun 
 |-  U_ m e. NN U_ l e. ( 1 ... m ) ( g ` l ) = { n | E. m e. NN n e. U_ l e. ( 1 ... m ) ( g ` l ) }
118 ovex 
 |-  ( 1 ... m ) e. _V
119 118 64 iunex 
 |-  U_ l e. ( 1 ... m ) ( g ` l ) e. _V
120 119 dfiun3 
 |-  U_ m e. NN U_ l e. ( 1 ... m ) ( g ` l ) = U. ran ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) )
121 116 117 120 3eqtr2i 
 |-  U_ x e. NN ( g ` x ) = U. ran ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) )
122 fofn 
 |-  ( g : NN -onto-> A -> g Fn NN )
123 fniunfv 
 |-  ( g Fn NN -> U_ x e. NN ( g ` x ) = U. ran g )
124 122 123 syl 
 |-  ( g : NN -onto-> A -> U_ x e. NN ( g ` x ) = U. ran g )
125 forn 
 |-  ( g : NN -onto-> A -> ran g = A )
126 125 unieqd 
 |-  ( g : NN -onto-> A -> U. ran g = U. A )
127 124 126 eqtrd 
 |-  ( g : NN -onto-> A -> U_ x e. NN ( g ` x ) = U. A )
128 121 127 eqtr3id 
 |-  ( g : NN -onto-> A -> U. ran ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) = U. A )
129 128 fveq2d 
 |-  ( g : NN -onto-> A -> ( vol ` U. ran ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ) = ( vol ` U. A ) )
130 129 adantr 
 |-  ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) -> ( vol ` U. ran ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ) = ( vol ` U. A ) )
131 rnco2 
 |-  ran ( vol o. ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ) = ( vol " ran ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) )
132 eqidd 
 |-  ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) -> ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) = ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) )
133 volf 
 |-  vol : dom vol --> ( 0 [,] +oo )
134 133 a1i 
 |-  ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) -> vol : dom vol --> ( 0 [,] +oo ) )
135 134 feqmptd 
 |-  ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) -> vol = ( n e. dom vol |-> ( vol ` n ) ) )
136 fveq2 
 |-  ( n = U_ l e. ( 1 ... m ) ( g ` l ) -> ( vol ` n ) = ( vol ` U_ l e. ( 1 ... m ) ( g ` l ) ) )
137 55 132 135 136 fmptco 
 |-  ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) -> ( vol o. ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ) = ( m e. NN |-> ( vol ` U_ l e. ( 1 ... m ) ( g ` l ) ) ) )
138 mblvol 
 |-  ( U_ l e. ( 1 ... m ) ( g ` l ) e. dom vol -> ( vol ` U_ l e. ( 1 ... m ) ( g ` l ) ) = ( vol* ` U_ l e. ( 1 ... m ) ( g ` l ) ) )
139 55 138 syl 
 |-  ( ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) /\ m e. NN ) -> ( vol ` U_ l e. ( 1 ... m ) ( g ` l ) ) = ( vol* ` U_ l e. ( 1 ... m ) ( g ` l ) ) )
140 mblss 
 |-  ( x e. dom vol -> x C_ RR )
141 140 adantr 
 |-  ( ( x e. dom vol /\ ( vol ` x ) = 0 ) -> x C_ RR )
142 26 eqeq1d 
 |-  ( x e. dom vol -> ( ( vol ` x ) = 0 <-> ( vol* ` x ) = 0 ) )
143 0re 
 |-  0 e. RR
144 eleq1a 
 |-  ( 0 e. RR -> ( ( vol* ` x ) = 0 -> ( vol* ` x ) e. RR ) )
145 143 144 ax-mp 
 |-  ( ( vol* ` x ) = 0 -> ( vol* ` x ) e. RR )
146 142 145 biimtrdi 
 |-  ( x e. dom vol -> ( ( vol ` x ) = 0 -> ( vol* ` x ) e. RR ) )
147 146 imp 
 |-  ( ( x e. dom vol /\ ( vol ` x ) = 0 ) -> ( vol* ` x ) e. RR )
148 141 147 jca 
 |-  ( ( x e. dom vol /\ ( vol ` x ) = 0 ) -> ( x C_ RR /\ ( vol* ` x ) e. RR ) )
149 148 ralimi 
 |-  ( A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) -> A. x e. A ( x C_ RR /\ ( vol* ` x ) e. RR ) )
150 149 adantl 
 |-  ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) -> A. x e. A ( x C_ RR /\ ( vol* ` x ) e. RR ) )
151 ssid 
 |-  NN C_ NN
152 sseq1 
 |-  ( x = ( g ` l ) -> ( x C_ RR <-> ( g ` l ) C_ RR ) )
153 fveq2 
 |-  ( x = ( g ` l ) -> ( vol* ` x ) = ( vol* ` ( g ` l ) ) )
154 153 eleq1d 
 |-  ( x = ( g ` l ) -> ( ( vol* ` x ) e. RR <-> ( vol* ` ( g ` l ) ) e. RR ) )
155 152 154 anbi12d 
 |-  ( x = ( g ` l ) -> ( ( x C_ RR /\ ( vol* ` x ) e. RR ) <-> ( ( g ` l ) C_ RR /\ ( vol* ` ( g ` l ) ) e. RR ) ) )
156 155 ralima 
 |-  ( ( g Fn NN /\ NN C_ NN ) -> ( A. x e. ( g " NN ) ( x C_ RR /\ ( vol* ` x ) e. RR ) <-> A. l e. NN ( ( g ` l ) C_ RR /\ ( vol* ` ( g ` l ) ) e. RR ) ) )
157 122 151 156 sylancl 
 |-  ( g : NN -onto-> A -> ( A. x e. ( g " NN ) ( x C_ RR /\ ( vol* ` x ) e. RR ) <-> A. l e. NN ( ( g ` l ) C_ RR /\ ( vol* ` ( g ` l ) ) e. RR ) ) )
158 foima 
 |-  ( g : NN -onto-> A -> ( g " NN ) = A )
159 158 raleqdv 
 |-  ( g : NN -onto-> A -> ( A. x e. ( g " NN ) ( x C_ RR /\ ( vol* ` x ) e. RR ) <-> A. x e. A ( x C_ RR /\ ( vol* ` x ) e. RR ) ) )
160 157 159 bitr3d 
 |-  ( g : NN -onto-> A -> ( A. l e. NN ( ( g ` l ) C_ RR /\ ( vol* ` ( g ` l ) ) e. RR ) <-> A. x e. A ( x C_ RR /\ ( vol* ` x ) e. RR ) ) )
161 160 adantr 
 |-  ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) -> ( A. l e. NN ( ( g ` l ) C_ RR /\ ( vol* ` ( g ` l ) ) e. RR ) <-> A. x e. A ( x C_ RR /\ ( vol* ` x ) e. RR ) ) )
162 150 161 mpbird 
 |-  ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) -> A. l e. NN ( ( g ` l ) C_ RR /\ ( vol* ` ( g ` l ) ) e. RR ) )
163 ssralv 
 |-  ( ( 1 ... m ) C_ NN -> ( A. l e. NN ( ( g ` l ) C_ RR /\ ( vol* ` ( g ` l ) ) e. RR ) -> A. l e. ( 1 ... m ) ( ( g ` l ) C_ RR /\ ( vol* ` ( g ` l ) ) e. RR ) ) )
164 39 162 163 mpsyl 
 |-  ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) -> A. l e. ( 1 ... m ) ( ( g ` l ) C_ RR /\ ( vol* ` ( g ` l ) ) e. RR ) )
165 164 adantr 
 |-  ( ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) /\ m e. NN ) -> A. l e. ( 1 ... m ) ( ( g ` l ) C_ RR /\ ( vol* ` ( g ` l ) ) e. RR ) )
166 ovolfiniun 
 |-  ( ( ( 1 ... m ) e. Fin /\ A. l e. ( 1 ... m ) ( ( g ` l ) C_ RR /\ ( vol* ` ( g ` l ) ) e. RR ) ) -> ( vol* ` U_ l e. ( 1 ... m ) ( g ` l ) ) <_ sum_ l e. ( 1 ... m ) ( vol* ` ( g ` l ) ) )
167 36 165 166 sylancr 
 |-  ( ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) /\ m e. NN ) -> ( vol* ` U_ l e. ( 1 ... m ) ( g ` l ) ) <_ sum_ l e. ( 1 ... m ) ( vol* ` ( g ` l ) ) )
168 mblvol 
 |-  ( ( g ` l ) e. dom vol -> ( vol ` ( g ` l ) ) = ( vol* ` ( g ` l ) ) )
169 49 168 syl 
 |-  ( ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) /\ l e. NN ) -> ( vol ` ( g ` l ) ) = ( vol* ` ( g ` l ) ) )
170 45 simprd 
 |-  ( ( A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) /\ ( g ` l ) e. A ) -> ( vol ` ( g ` l ) ) = 0 )
171 41 170 sylan2 
 |-  ( ( A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) /\ ( g : NN -onto-> A /\ l e. NN ) ) -> ( vol ` ( g ` l ) ) = 0 )
172 171 ancoms 
 |-  ( ( ( g : NN -onto-> A /\ l e. NN ) /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) -> ( vol ` ( g ` l ) ) = 0 )
173 172 an32s 
 |-  ( ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) /\ l e. NN ) -> ( vol ` ( g ` l ) ) = 0 )
174 169 173 eqtr3d 
 |-  ( ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) /\ l e. NN ) -> ( vol* ` ( g ` l ) ) = 0 )
175 174 ralrimiva 
 |-  ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) -> A. l e. NN ( vol* ` ( g ` l ) ) = 0 )
176 ssralv 
 |-  ( ( 1 ... m ) C_ NN -> ( A. l e. NN ( vol* ` ( g ` l ) ) = 0 -> A. l e. ( 1 ... m ) ( vol* ` ( g ` l ) ) = 0 ) )
177 39 175 176 mpsyl 
 |-  ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) -> A. l e. ( 1 ... m ) ( vol* ` ( g ` l ) ) = 0 )
178 177 adantr 
 |-  ( ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) /\ m e. NN ) -> A. l e. ( 1 ... m ) ( vol* ` ( g ` l ) ) = 0 )
179 178 sumeq2d 
 |-  ( ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) /\ m e. NN ) -> sum_ l e. ( 1 ... m ) ( vol* ` ( g ` l ) ) = sum_ l e. ( 1 ... m ) 0 )
180 36 olci 
 |-  ( ( 1 ... m ) C_ ( ZZ>= ` 1 ) \/ ( 1 ... m ) e. Fin )
181 sumz 
 |-  ( ( ( 1 ... m ) C_ ( ZZ>= ` 1 ) \/ ( 1 ... m ) e. Fin ) -> sum_ l e. ( 1 ... m ) 0 = 0 )
182 180 181 ax-mp 
 |-  sum_ l e. ( 1 ... m ) 0 = 0
183 179 182 eqtrdi 
 |-  ( ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) /\ m e. NN ) -> sum_ l e. ( 1 ... m ) ( vol* ` ( g ` l ) ) = 0 )
184 167 183 breqtrd 
 |-  ( ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) /\ m e. NN ) -> ( vol* ` U_ l e. ( 1 ... m ) ( g ` l ) ) <_ 0 )
185 mblss 
 |-  ( ( g ` l ) e. dom vol -> ( g ` l ) C_ RR )
186 185 ralimi 
 |-  ( A. l e. ( 1 ... m ) ( g ` l ) e. dom vol -> A. l e. ( 1 ... m ) ( g ` l ) C_ RR )
187 52 186 syl 
 |-  ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) -> A. l e. ( 1 ... m ) ( g ` l ) C_ RR )
188 iunss 
 |-  ( U_ l e. ( 1 ... m ) ( g ` l ) C_ RR <-> A. l e. ( 1 ... m ) ( g ` l ) C_ RR )
189 187 188 sylibr 
 |-  ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) -> U_ l e. ( 1 ... m ) ( g ` l ) C_ RR )
190 189 adantr 
 |-  ( ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) /\ m e. NN ) -> U_ l e. ( 1 ... m ) ( g ` l ) C_ RR )
191 ovolge0 
 |-  ( U_ l e. ( 1 ... m ) ( g ` l ) C_ RR -> 0 <_ ( vol* ` U_ l e. ( 1 ... m ) ( g ` l ) ) )
192 190 191 syl 
 |-  ( ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) /\ m e. NN ) -> 0 <_ ( vol* ` U_ l e. ( 1 ... m ) ( g ` l ) ) )
193 ovolcl 
 |-  ( U_ l e. ( 1 ... m ) ( g ` l ) C_ RR -> ( vol* ` U_ l e. ( 1 ... m ) ( g ` l ) ) e. RR* )
194 189 193 syl 
 |-  ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) -> ( vol* ` U_ l e. ( 1 ... m ) ( g ` l ) ) e. RR* )
195 194 adantr 
 |-  ( ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) /\ m e. NN ) -> ( vol* ` U_ l e. ( 1 ... m ) ( g ` l ) ) e. RR* )
196 0xr 
 |-  0 e. RR*
197 xrletri3 
 |-  ( ( ( vol* ` U_ l e. ( 1 ... m ) ( g ` l ) ) e. RR* /\ 0 e. RR* ) -> ( ( vol* ` U_ l e. ( 1 ... m ) ( g ` l ) ) = 0 <-> ( ( vol* ` U_ l e. ( 1 ... m ) ( g ` l ) ) <_ 0 /\ 0 <_ ( vol* ` U_ l e. ( 1 ... m ) ( g ` l ) ) ) ) )
198 195 196 197 sylancl 
 |-  ( ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) /\ m e. NN ) -> ( ( vol* ` U_ l e. ( 1 ... m ) ( g ` l ) ) = 0 <-> ( ( vol* ` U_ l e. ( 1 ... m ) ( g ` l ) ) <_ 0 /\ 0 <_ ( vol* ` U_ l e. ( 1 ... m ) ( g ` l ) ) ) ) )
199 184 192 198 mpbir2and 
 |-  ( ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) /\ m e. NN ) -> ( vol* ` U_ l e. ( 1 ... m ) ( g ` l ) ) = 0 )
200 139 199 eqtrd 
 |-  ( ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) /\ m e. NN ) -> ( vol ` U_ l e. ( 1 ... m ) ( g ` l ) ) = 0 )
201 200 mpteq2dva 
 |-  ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) -> ( m e. NN |-> ( vol ` U_ l e. ( 1 ... m ) ( g ` l ) ) ) = ( m e. NN |-> 0 ) )
202 fconstmpt 
 |-  ( NN X. { 0 } ) = ( m e. NN |-> 0 )
203 201 202 eqtr4di 
 |-  ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) -> ( m e. NN |-> ( vol ` U_ l e. ( 1 ... m ) ( g ` l ) ) ) = ( NN X. { 0 } ) )
204 137 203 eqtrd 
 |-  ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) -> ( vol o. ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ) = ( NN X. { 0 } ) )
205 frn 
 |-  ( ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) : NN --> dom vol -> ran ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) C_ dom vol )
206 ffn 
 |-  ( vol : dom vol --> ( 0 [,] +oo ) -> vol Fn dom vol )
207 133 206 ax-mp 
 |-  vol Fn dom vol
208 119 62 fnmpti 
 |-  ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) Fn NN
209 fnco 
 |-  ( ( vol Fn dom vol /\ ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) Fn NN /\ ran ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) C_ dom vol ) -> ( vol o. ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ) Fn NN )
210 207 208 209 mp3an12 
 |-  ( ran ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) C_ dom vol -> ( vol o. ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ) Fn NN )
211 56 205 210 3syl 
 |-  ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) -> ( vol o. ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ) Fn NN )
212 1nn 
 |-  1 e. NN
213 212 ne0ii 
 |-  NN =/= (/)
214 fconst5 
 |-  ( ( ( vol o. ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ) Fn NN /\ NN =/= (/) ) -> ( ( vol o. ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ) = ( NN X. { 0 } ) <-> ran ( vol o. ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ) = { 0 } ) )
215 211 213 214 sylancl 
 |-  ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) -> ( ( vol o. ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ) = ( NN X. { 0 } ) <-> ran ( vol o. ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ) = { 0 } ) )
216 204 215 mpbid 
 |-  ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) -> ran ( vol o. ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ) = { 0 } )
217 131 216 eqtr3id 
 |-  ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) -> ( vol " ran ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ) = { 0 } )
218 217 supeq1d 
 |-  ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) -> sup ( ( vol " ran ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ) , RR* , < ) = sup ( { 0 } , RR* , < ) )
219 xrltso 
 |-  < Or RR*
220 supsn 
 |-  ( ( < Or RR* /\ 0 e. RR* ) -> sup ( { 0 } , RR* , < ) = 0 )
221 219 196 220 mp2an 
 |-  sup ( { 0 } , RR* , < ) = 0
222 218 221 eqtrdi 
 |-  ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) -> sup ( ( vol " ran ( m e. NN |-> U_ l e. ( 1 ... m ) ( g ` l ) ) ) , RR* , < ) = 0 )
223 93 130 222 3eqtr3rd 
 |-  ( ( g : NN -onto-> A /\ A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) ) -> 0 = ( vol ` U. A ) )
224 223 ex 
 |-  ( g : NN -onto-> A -> ( A. x e. A ( x e. dom vol /\ ( vol ` x ) = 0 ) -> 0 = ( vol ` U. A ) ) )
225 35 224 syl5 
 |-  ( g : NN -onto-> A -> ( ( A. x e. A x ~<_ NN /\ U. A C_ RR ) -> 0 = ( vol ` U. A ) ) )
226 225 exlimiv 
 |-  ( E. g g : NN -onto-> A -> ( ( A. x e. A x ~<_ NN /\ U. A C_ RR ) -> 0 = ( vol ` U. A ) ) )
227 19 226 syl 
 |-  ( ( A =/= (/) /\ A ~<_ NN ) -> ( ( A. x e. A x ~<_ NN /\ U. A C_ RR ) -> 0 = ( vol ` U. A ) ) )
228 227 expimpd 
 |-  ( A =/= (/) -> ( ( A ~<_ NN /\ ( A. x e. A x ~<_ NN /\ U. A C_ RR ) ) -> 0 = ( vol ` U. A ) ) )
229 12 228 pm2.61ine 
 |-  ( ( A ~<_ NN /\ ( A. x e. A x ~<_ NN /\ U. A C_ RR ) ) -> 0 = ( vol ` U. A ) )
230 renepnf 
 |-  ( 0 e. RR -> 0 =/= +oo )
231 143 230 mp1i 
 |-  ( U. A = RR -> 0 =/= +oo )
232 fveq2 
 |-  ( U. A = RR -> ( vol ` U. A ) = ( vol ` RR ) )
233 rembl 
 |-  RR e. dom vol
234 mblvol 
 |-  ( RR e. dom vol -> ( vol ` RR ) = ( vol* ` RR ) )
235 233 234 ax-mp 
 |-  ( vol ` RR ) = ( vol* ` RR )
236 ovolre 
 |-  ( vol* ` RR ) = +oo
237 235 236 eqtri 
 |-  ( vol ` RR ) = +oo
238 232 237 eqtrdi 
 |-  ( U. A = RR -> ( vol ` U. A ) = +oo )
239 231 238 neeqtrrd 
 |-  ( U. A = RR -> 0 =/= ( vol ` U. A ) )
240 239 necon2i 
 |-  ( 0 = ( vol ` U. A ) -> U. A =/= RR )
241 229 240 syl 
 |-  ( ( A ~<_ NN /\ ( A. x e. A x ~<_ NN /\ U. A C_ RR ) ) -> U. A =/= RR )
242 241 expr 
 |-  ( ( A ~<_ NN /\ A. x e. A x ~<_ NN ) -> ( U. A C_ RR -> U. A =/= RR ) )
243 eqimss 
 |-  ( U. A = RR -> U. A C_ RR )
244 243 necon3bi 
 |-  ( -. U. A C_ RR -> U. A =/= RR )
245 242 244 pm2.61d1 
 |-  ( ( A ~<_ NN /\ A. x e. A x ~<_ NN ) -> U. A =/= RR )