Metamath Proof Explorer

Theorem ovoliunnfl

Description: ovoliun is incompatible with the Feferman-Levy model. (Contributed by Brendan Leahy, 21-Nov-2017)

Ref Expression
Hypothesis ovoliunnfl.0 
|- ( ( f Fn NN /\ A. n e. NN ( ( f ` n ) C_ RR /\ ( vol* ` ( f ` n ) ) e. RR ) ) -> ( vol* ` U_ m e. NN ( f ` m ) ) <_ sup ( ran seq 1 ( + , ( m e. NN |-> ( vol* ` ( f ` m ) ) ) ) , RR* , < ) )
Assertion ovoliunnfl 
|- ( ( A ~<_ NN /\ A. x e. A x ~<_ NN ) -> U. A =/= RR )

Proof

Step Hyp Ref Expression
1 ovoliunnfl.0 
 |-  ( ( f Fn NN /\ A. n e. NN ( ( f ` n ) C_ RR /\ ( vol* ` ( f ` n ) ) e. RR ) ) -> ( vol* ` U_ m e. NN ( f ` m ) ) <_ sup ( ran seq 1 ( + , ( m e. NN |-> ( vol* ` ( f ` m ) ) ) ) , 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 ovol0 
 |-  ( vol* ` (/) ) = 0
7 5 6 eqtr2di 
 |-  ( A = (/) -> 0 = ( vol* ` U. A ) )
8 7 a1d 
 |-  ( A = (/) -> ( ( A ~<_ NN /\ ( A. x e. A x ~<_ NN /\ U. A C_ RR ) ) -> 0 = ( vol* ` U. A ) ) )
9 ovolge0 
 |-  ( U. A C_ RR -> 0 <_ ( vol* ` U. A ) )
10 9 ad2antll 
 |-  ( ( ( A =/= (/) /\ A ~<_ NN ) /\ ( A. x e. A x ~<_ NN /\ U. A C_ RR ) ) -> 0 <_ ( vol* ` U. A ) )
11 reldom 
 |-  Rel ~<_
12 11 brrelex1i 
 |-  ( A ~<_ NN -> A e. _V )
13 0sdomg 
 |-  ( A e. _V -> ( (/) ~< A <-> A =/= (/) ) )
14 12 13 syl 
 |-  ( A ~<_ NN -> ( (/) ~< A <-> A =/= (/) ) )
15 14 biimparc 
 |-  ( ( A =/= (/) /\ A ~<_ NN ) -> (/) ~< A )
16 fodomr 
 |-  ( ( (/) ~< A /\ A ~<_ NN ) -> E. f f : NN -onto-> A )
17 15 16 sylancom 
 |-  ( ( A =/= (/) /\ A ~<_ NN ) -> E. f f : NN -onto-> A )
18 unissb 
 |-  ( U. A C_ RR <-> A. x e. A x C_ RR )
19 18 anbi1i 
 |-  ( ( U. A C_ RR /\ A. x e. A x ~<_ NN ) <-> ( A. x e. A x C_ RR /\ A. x e. A x ~<_ NN ) )
20 r19.26 
 |-  ( A. x e. A ( x C_ RR /\ x ~<_ NN ) <-> ( A. x e. A x C_ RR /\ A. x e. A x ~<_ NN ) )
21 19 20 bitr4i 
 |-  ( ( U. A C_ RR /\ A. x e. A x ~<_ NN ) <-> A. x e. A ( x C_ RR /\ x ~<_ NN ) )
22 brdom2 
 |-  ( x ~<_ NN <-> ( x ~< NN \/ x ~~ NN ) )
23 nnenom 
 |-  NN ~~ _om
24 sdomen2 
 |-  ( NN ~~ _om -> ( x ~< NN <-> x ~< _om ) )
25 23 24 ax-mp 
 |-  ( x ~< NN <-> x ~< _om )
26 isfinite 
 |-  ( x e. Fin <-> x ~< _om )
27 25 26 bitr4i 
 |-  ( x ~< NN <-> x e. Fin )
28 27 orbi1i 
 |-  ( ( x ~< NN \/ x ~~ NN ) <-> ( x e. Fin \/ x ~~ NN ) )
29 22 28 bitri 
 |-  ( x ~<_ NN <-> ( x e. Fin \/ x ~~ NN ) )
30 ovolfi 
 |-  ( ( x e. Fin /\ x C_ RR ) -> ( vol* ` x ) = 0 )
31 30 expcom 
 |-  ( x C_ RR -> ( x e. Fin -> ( vol* ` x ) = 0 ) )
32 ovolctb 
 |-  ( ( x C_ RR /\ x ~~ NN ) -> ( vol* ` x ) = 0 )
33 32 ex 
 |-  ( x C_ RR -> ( x ~~ NN -> ( vol* ` x ) = 0 ) )
34 31 33 jaod 
 |-  ( x C_ RR -> ( ( x e. Fin \/ x ~~ NN ) -> ( vol* ` x ) = 0 ) )
35 29 34 biimtrid 
 |-  ( x C_ RR -> ( x ~<_ NN -> ( vol* ` x ) = 0 ) )
36 35 imdistani 
 |-  ( ( x C_ RR /\ x ~<_ NN ) -> ( x C_ RR /\ ( vol* ` x ) = 0 ) )
37 36 ralimi 
 |-  ( A. x e. A ( x C_ RR /\ x ~<_ NN ) -> A. x e. A ( x C_ RR /\ ( vol* ` x ) = 0 ) )
38 21 37 sylbi 
 |-  ( ( U. A C_ RR /\ A. x e. A x ~<_ NN ) -> A. x e. A ( x C_ RR /\ ( vol* ` x ) = 0 ) )
39 38 ancoms 
 |-  ( ( A. x e. A x ~<_ NN /\ U. A C_ RR ) -> A. x e. A ( x C_ RR /\ ( vol* ` x ) = 0 ) )
40 foima 
 |-  ( f : NN -onto-> A -> ( f " NN ) = A )
41 40 raleqdv 
 |-  ( f : NN -onto-> A -> ( A. x e. ( f " NN ) ( x C_ RR /\ ( vol* ` x ) = 0 ) <-> A. x e. A ( x C_ RR /\ ( vol* ` x ) = 0 ) ) )
42 fofn 
 |-  ( f : NN -onto-> A -> f Fn NN )
43 ssid 
 |-  NN C_ NN
44 sseq1 
 |-  ( x = ( f ` l ) -> ( x C_ RR <-> ( f ` l ) C_ RR ) )
45 fveqeq2 
 |-  ( x = ( f ` l ) -> ( ( vol* ` x ) = 0 <-> ( vol* ` ( f ` l ) ) = 0 ) )
46 44 45 anbi12d 
 |-  ( x = ( f ` l ) -> ( ( x C_ RR /\ ( vol* ` x ) = 0 ) <-> ( ( f ` l ) C_ RR /\ ( vol* ` ( f ` l ) ) = 0 ) ) )
47 46 ralima 
 |-  ( ( f Fn NN /\ NN C_ NN ) -> ( A. x e. ( f " NN ) ( x C_ RR /\ ( vol* ` x ) = 0 ) <-> A. l e. NN ( ( f ` l ) C_ RR /\ ( vol* ` ( f ` l ) ) = 0 ) ) )
48 42 43 47 sylancl 
 |-  ( f : NN -onto-> A -> ( A. x e. ( f " NN ) ( x C_ RR /\ ( vol* ` x ) = 0 ) <-> A. l e. NN ( ( f ` l ) C_ RR /\ ( vol* ` ( f ` l ) ) = 0 ) ) )
49 41 48 bitr3d 
 |-  ( f : NN -onto-> A -> ( A. x e. A ( x C_ RR /\ ( vol* ` x ) = 0 ) <-> A. l e. NN ( ( f ` l ) C_ RR /\ ( vol* ` ( f ` l ) ) = 0 ) ) )
50 fveq2 
 |-  ( l = n -> ( f ` l ) = ( f ` n ) )
51 50 sseq1d 
 |-  ( l = n -> ( ( f ` l ) C_ RR <-> ( f ` n ) C_ RR ) )
52 2fveq3 
 |-  ( l = n -> ( vol* ` ( f ` l ) ) = ( vol* ` ( f ` n ) ) )
53 52 eqeq1d 
 |-  ( l = n -> ( ( vol* ` ( f ` l ) ) = 0 <-> ( vol* ` ( f ` n ) ) = 0 ) )
54 51 53 anbi12d 
 |-  ( l = n -> ( ( ( f ` l ) C_ RR /\ ( vol* ` ( f ` l ) ) = 0 ) <-> ( ( f ` n ) C_ RR /\ ( vol* ` ( f ` n ) ) = 0 ) ) )
55 54 cbvralvw 
 |-  ( A. l e. NN ( ( f ` l ) C_ RR /\ ( vol* ` ( f ` l ) ) = 0 ) <-> A. n e. NN ( ( f ` n ) C_ RR /\ ( vol* ` ( f ` n ) ) = 0 ) )
56 0re 
 |-  0 e. RR
57 eleq1a 
 |-  ( 0 e. RR -> ( ( vol* ` ( f ` n ) ) = 0 -> ( vol* ` ( f ` n ) ) e. RR ) )
58 56 57 ax-mp 
 |-  ( ( vol* ` ( f ` n ) ) = 0 -> ( vol* ` ( f ` n ) ) e. RR )
59 58 anim2i 
 |-  ( ( ( f ` n ) C_ RR /\ ( vol* ` ( f ` n ) ) = 0 ) -> ( ( f ` n ) C_ RR /\ ( vol* ` ( f ` n ) ) e. RR ) )
60 59 ralimi 
 |-  ( A. n e. NN ( ( f ` n ) C_ RR /\ ( vol* ` ( f ` n ) ) = 0 ) -> A. n e. NN ( ( f ` n ) C_ RR /\ ( vol* ` ( f ` n ) ) e. RR ) )
61 55 60 sylbi 
 |-  ( A. l e. NN ( ( f ` l ) C_ RR /\ ( vol* ` ( f ` l ) ) = 0 ) -> A. n e. NN ( ( f ` n ) C_ RR /\ ( vol* ` ( f ` n ) ) e. RR ) )
62 42 61 1 syl2an 
 |-  ( ( f : NN -onto-> A /\ A. l e. NN ( ( f ` l ) C_ RR /\ ( vol* ` ( f ` l ) ) = 0 ) ) -> ( vol* ` U_ m e. NN ( f ` m ) ) <_ sup ( ran seq 1 ( + , ( m e. NN |-> ( vol* ` ( f ` m ) ) ) ) , RR* , < ) )
63 fofun 
 |-  ( f : NN -onto-> A -> Fun f )
64 funiunfv 
 |-  ( Fun f -> U_ m e. NN ( f ` m ) = U. ( f " NN ) )
65 63 64 syl 
 |-  ( f : NN -onto-> A -> U_ m e. NN ( f ` m ) = U. ( f " NN ) )
66 40 unieqd 
 |-  ( f : NN -onto-> A -> U. ( f " NN ) = U. A )
67 65 66 eqtrd 
 |-  ( f : NN -onto-> A -> U_ m e. NN ( f ` m ) = U. A )
68 67 fveq2d 
 |-  ( f : NN -onto-> A -> ( vol* ` U_ m e. NN ( f ` m ) ) = ( vol* ` U. A ) )
69 68 adantr 
 |-  ( ( f : NN -onto-> A /\ A. l e. NN ( ( f ` l ) C_ RR /\ ( vol* ` ( f ` l ) ) = 0 ) ) -> ( vol* ` U_ m e. NN ( f ` m ) ) = ( vol* ` U. A ) )
70 fveq2 
 |-  ( l = m -> ( f ` l ) = ( f ` m ) )
71 70 sseq1d 
 |-  ( l = m -> ( ( f ` l ) C_ RR <-> ( f ` m ) C_ RR ) )
72 2fveq3 
 |-  ( l = m -> ( vol* ` ( f ` l ) ) = ( vol* ` ( f ` m ) ) )
73 72 eqeq1d 
 |-  ( l = m -> ( ( vol* ` ( f ` l ) ) = 0 <-> ( vol* ` ( f ` m ) ) = 0 ) )
74 71 73 anbi12d 
 |-  ( l = m -> ( ( ( f ` l ) C_ RR /\ ( vol* ` ( f ` l ) ) = 0 ) <-> ( ( f ` m ) C_ RR /\ ( vol* ` ( f ` m ) ) = 0 ) ) )
75 74 rspccva 
 |-  ( ( A. l e. NN ( ( f ` l ) C_ RR /\ ( vol* ` ( f ` l ) ) = 0 ) /\ m e. NN ) -> ( ( f ` m ) C_ RR /\ ( vol* ` ( f ` m ) ) = 0 ) )
76 75 simprd 
 |-  ( ( A. l e. NN ( ( f ` l ) C_ RR /\ ( vol* ` ( f ` l ) ) = 0 ) /\ m e. NN ) -> ( vol* ` ( f ` m ) ) = 0 )
77 76 mpteq2dva 
 |-  ( A. l e. NN ( ( f ` l ) C_ RR /\ ( vol* ` ( f ` l ) ) = 0 ) -> ( m e. NN |-> ( vol* ` ( f ` m ) ) ) = ( m e. NN |-> 0 ) )
78 77 seqeq3d 
 |-  ( A. l e. NN ( ( f ` l ) C_ RR /\ ( vol* ` ( f ` l ) ) = 0 ) -> seq 1 ( + , ( m e. NN |-> ( vol* ` ( f ` m ) ) ) ) = seq 1 ( + , ( m e. NN |-> 0 ) ) )
79 78 rneqd 
 |-  ( A. l e. NN ( ( f ` l ) C_ RR /\ ( vol* ` ( f ` l ) ) = 0 ) -> ran seq 1 ( + , ( m e. NN |-> ( vol* ` ( f ` m ) ) ) ) = ran seq 1 ( + , ( m e. NN |-> 0 ) ) )
80 79 supeq1d 
 |-  ( A. l e. NN ( ( f ` l ) C_ RR /\ ( vol* ` ( f ` l ) ) = 0 ) -> sup ( ran seq 1 ( + , ( m e. NN |-> ( vol* ` ( f ` m ) ) ) ) , RR* , < ) = sup ( ran seq 1 ( + , ( m e. NN |-> 0 ) ) , RR* , < ) )
81 0cn 
 |-  0 e. CC
82 ser1const 
 |-  ( ( 0 e. CC /\ l e. NN ) -> ( seq 1 ( + , ( NN X. { 0 } ) ) ` l ) = ( l x. 0 ) )
83 81 82 mpan 
 |-  ( l e. NN -> ( seq 1 ( + , ( NN X. { 0 } ) ) ` l ) = ( l x. 0 ) )
84 nncn 
 |-  ( l e. NN -> l e. CC )
85 84 mul01d 
 |-  ( l e. NN -> ( l x. 0 ) = 0 )
86 83 85 eqtrd 
 |-  ( l e. NN -> ( seq 1 ( + , ( NN X. { 0 } ) ) ` l ) = 0 )
87 86 mpteq2ia 
 |-  ( l e. NN |-> ( seq 1 ( + , ( NN X. { 0 } ) ) ` l ) ) = ( l e. NN |-> 0 )
88 fconstmpt 
 |-  ( NN X. { 0 } ) = ( m e. NN |-> 0 )
89 seqeq3 
 |-  ( ( NN X. { 0 } ) = ( m e. NN |-> 0 ) -> seq 1 ( + , ( NN X. { 0 } ) ) = seq 1 ( + , ( m e. NN |-> 0 ) ) )
90 88 89 ax-mp 
 |-  seq 1 ( + , ( NN X. { 0 } ) ) = seq 1 ( + , ( m e. NN |-> 0 ) )
91 1z 
 |-  1 e. ZZ
92 seqfn 
 |-  ( 1 e. ZZ -> seq 1 ( + , ( NN X. { 0 } ) ) Fn ( ZZ>= ` 1 ) )
93 91 92 ax-mp 
 |-  seq 1 ( + , ( NN X. { 0 } ) ) Fn ( ZZ>= ` 1 )
94 nnuz 
 |-  NN = ( ZZ>= ` 1 )
95 94 fneq2i 
 |-  ( seq 1 ( + , ( NN X. { 0 } ) ) Fn NN <-> seq 1 ( + , ( NN X. { 0 } ) ) Fn ( ZZ>= ` 1 ) )
96 dffn5 
 |-  ( seq 1 ( + , ( NN X. { 0 } ) ) Fn NN <-> seq 1 ( + , ( NN X. { 0 } ) ) = ( l e. NN |-> ( seq 1 ( + , ( NN X. { 0 } ) ) ` l ) ) )
97 95 96 bitr3i 
 |-  ( seq 1 ( + , ( NN X. { 0 } ) ) Fn ( ZZ>= ` 1 ) <-> seq 1 ( + , ( NN X. { 0 } ) ) = ( l e. NN |-> ( seq 1 ( + , ( NN X. { 0 } ) ) ` l ) ) )
98 93 97 mpbi 
 |-  seq 1 ( + , ( NN X. { 0 } ) ) = ( l e. NN |-> ( seq 1 ( + , ( NN X. { 0 } ) ) ` l ) )
99 90 98 eqtr3i 
 |-  seq 1 ( + , ( m e. NN |-> 0 ) ) = ( l e. NN |-> ( seq 1 ( + , ( NN X. { 0 } ) ) ` l ) )
100 fconstmpt 
 |-  ( NN X. { 0 } ) = ( l e. NN |-> 0 )
101 87 99 100 3eqtr4i 
 |-  seq 1 ( + , ( m e. NN |-> 0 ) ) = ( NN X. { 0 } )
102 101 rneqi 
 |-  ran seq 1 ( + , ( m e. NN |-> 0 ) ) = ran ( NN X. { 0 } )
103 1nn 
 |-  1 e. NN
104 ne0i 
 |-  ( 1 e. NN -> NN =/= (/) )
105 rnxp 
 |-  ( NN =/= (/) -> ran ( NN X. { 0 } ) = { 0 } )
106 103 104 105 mp2b 
 |-  ran ( NN X. { 0 } ) = { 0 }
107 102 106 eqtri 
 |-  ran seq 1 ( + , ( m e. NN |-> 0 ) ) = { 0 }
108 107 supeq1i 
 |-  sup ( ran seq 1 ( + , ( m e. NN |-> 0 ) ) , RR* , < ) = sup ( { 0 } , RR* , < )
109 xrltso 
 |-  < Or RR*
110 0xr 
 |-  0 e. RR*
111 supsn 
 |-  ( ( < Or RR* /\ 0 e. RR* ) -> sup ( { 0 } , RR* , < ) = 0 )
112 109 110 111 mp2an 
 |-  sup ( { 0 } , RR* , < ) = 0
113 108 112 eqtri 
 |-  sup ( ran seq 1 ( + , ( m e. NN |-> 0 ) ) , RR* , < ) = 0
114 80 113 eqtrdi 
 |-  ( A. l e. NN ( ( f ` l ) C_ RR /\ ( vol* ` ( f ` l ) ) = 0 ) -> sup ( ran seq 1 ( + , ( m e. NN |-> ( vol* ` ( f ` m ) ) ) ) , RR* , < ) = 0 )
115 114 adantl 
 |-  ( ( f : NN -onto-> A /\ A. l e. NN ( ( f ` l ) C_ RR /\ ( vol* ` ( f ` l ) ) = 0 ) ) -> sup ( ran seq 1 ( + , ( m e. NN |-> ( vol* ` ( f ` m ) ) ) ) , RR* , < ) = 0 )
116 62 69 115 3brtr3d 
 |-  ( ( f : NN -onto-> A /\ A. l e. NN ( ( f ` l ) C_ RR /\ ( vol* ` ( f ` l ) ) = 0 ) ) -> ( vol* ` U. A ) <_ 0 )
117 116 ex 
 |-  ( f : NN -onto-> A -> ( A. l e. NN ( ( f ` l ) C_ RR /\ ( vol* ` ( f ` l ) ) = 0 ) -> ( vol* ` U. A ) <_ 0 ) )
118 49 117 sylbid 
 |-  ( f : NN -onto-> A -> ( A. x e. A ( x C_ RR /\ ( vol* ` x ) = 0 ) -> ( vol* ` U. A ) <_ 0 ) )
119 118 exlimiv 
 |-  ( E. f f : NN -onto-> A -> ( A. x e. A ( x C_ RR /\ ( vol* ` x ) = 0 ) -> ( vol* ` U. A ) <_ 0 ) )
120 119 imp 
 |-  ( ( E. f f : NN -onto-> A /\ A. x e. A ( x C_ RR /\ ( vol* ` x ) = 0 ) ) -> ( vol* ` U. A ) <_ 0 )
121 17 39 120 syl2an 
 |-  ( ( ( A =/= (/) /\ A ~<_ NN ) /\ ( A. x e. A x ~<_ NN /\ U. A C_ RR ) ) -> ( vol* ` U. A ) <_ 0 )
122 ovolcl 
 |-  ( U. A C_ RR -> ( vol* ` U. A ) e. RR* )
123 xrletri3 
 |-  ( ( 0 e. RR* /\ ( vol* ` U. A ) e. RR* ) -> ( 0 = ( vol* ` U. A ) <-> ( 0 <_ ( vol* ` U. A ) /\ ( vol* ` U. A ) <_ 0 ) ) )
124 110 122 123 sylancr 
 |-  ( U. A C_ RR -> ( 0 = ( vol* ` U. A ) <-> ( 0 <_ ( vol* ` U. A ) /\ ( vol* ` U. A ) <_ 0 ) ) )
125 124 ad2antll 
 |-  ( ( ( A =/= (/) /\ A ~<_ NN ) /\ ( A. x e. A x ~<_ NN /\ U. A C_ RR ) ) -> ( 0 = ( vol* ` U. A ) <-> ( 0 <_ ( vol* ` U. A ) /\ ( vol* ` U. A ) <_ 0 ) ) )
126 10 121 125 mpbir2and 
 |-  ( ( ( A =/= (/) /\ A ~<_ NN ) /\ ( A. x e. A x ~<_ NN /\ U. A C_ RR ) ) -> 0 = ( vol* ` U. A ) )
127 126 expl 
 |-  ( A =/= (/) -> ( ( A ~<_ NN /\ ( A. x e. A x ~<_ NN /\ U. A C_ RR ) ) -> 0 = ( vol* ` U. A ) ) )
128 8 127 pm2.61ine 
 |-  ( ( A ~<_ NN /\ ( A. x e. A x ~<_ NN /\ U. A C_ RR ) ) -> 0 = ( vol* ` U. A ) )
129 renepnf 
 |-  ( 0 e. RR -> 0 =/= +oo )
130 56 129 mp1i 
 |-  ( U. A = RR -> 0 =/= +oo )
131 fveq2 
 |-  ( U. A = RR -> ( vol* ` U. A ) = ( vol* ` RR ) )
132 ovolre 
 |-  ( vol* ` RR ) = +oo
133 131 132 eqtrdi 
 |-  ( U. A = RR -> ( vol* ` U. A ) = +oo )
134 130 133 neeqtrrd 
 |-  ( U. A = RR -> 0 =/= ( vol* ` U. A ) )
135 134 necon2i 
 |-  ( 0 = ( vol* ` U. A ) -> U. A =/= RR )
136 128 135 syl 
 |-  ( ( A ~<_ NN /\ ( A. x e. A x ~<_ NN /\ U. A C_ RR ) ) -> U. A =/= RR )
137 136 expr 
 |-  ( ( A ~<_ NN /\ A. x e. A x ~<_ NN ) -> ( U. A C_ RR -> U. A =/= RR ) )
138 eqimss 
 |-  ( U. A = RR -> U. A C_ RR )
139 138 necon3bi 
 |-  ( -. U. A C_ RR -> U. A =/= RR )
140 137 139 pm2.61d1 
 |-  ( ( A ~<_ NN /\ A. x e. A x ~<_ NN ) -> U. A =/= RR )