Metamath Proof Explorer

Theorem vitali

Description: If the reals can be well-ordered, then there are non-measurable sets. The proof uses "Vitali sets", named for Giuseppe Vitali (1905). (Contributed by Mario Carneiro, 16-Jun-2014)

Ref Expression
Assertion vitali 
|- ( .< We RR -> dom vol C. ~P RR )

Proof

Step Hyp Ref Expression
1 reex 
 |-  RR e. _V
2 1 pwex 
 |-  ~P RR e. _V
3 weinxp 
 |-  ( .< We RR <-> ( .< i^i ( RR X. RR ) ) We RR )
4 unipw 
 |-  U. ~P RR = RR
5 weeq2 
 |-  ( U. ~P RR = RR -> ( ( .< i^i ( RR X. RR ) ) We U. ~P RR <-> ( .< i^i ( RR X. RR ) ) We RR ) )
6 4 5 ax-mp 
 |-  ( ( .< i^i ( RR X. RR ) ) We U. ~P RR <-> ( .< i^i ( RR X. RR ) ) We RR )
7 3 6 bitr4i 
 |-  ( .< We RR <-> ( .< i^i ( RR X. RR ) ) We U. ~P RR )
8 1 1 xpex 
 |-  ( RR X. RR ) e. _V
9 8 inex2 
 |-  ( .< i^i ( RR X. RR ) ) e. _V
10 weeq1 
 |-  ( x = ( .< i^i ( RR X. RR ) ) -> ( x We U. ~P RR <-> ( .< i^i ( RR X. RR ) ) We U. ~P RR ) )
11 9 10 spcev 
 |-  ( ( .< i^i ( RR X. RR ) ) We U. ~P RR -> E. x x We U. ~P RR )
12 7 11 sylbi 
 |-  ( .< We RR -> E. x x We U. ~P RR )
13 dfac8c 
 |-  ( ~P RR e. _V -> ( E. x x We U. ~P RR -> E. f A. z e. ~P RR ( z =/= (/) -> ( f ` z ) e. z ) ) )
14 2 12 13 mpsyl 
 |-  ( .< We RR -> E. f A. z e. ~P RR ( z =/= (/) -> ( f ` z ) e. z ) )
15 qex 
 |-  QQ e. _V
16 15 inex1 
 |-  ( QQ i^i ( -u 1 [,] 1 ) ) e. _V
17 nnrecq 
 |-  ( x e. NN -> ( 1 / x ) e. QQ )
18 nnrecre 
 |-  ( x e. NN -> ( 1 / x ) e. RR )
19 neg1rr 
 |-  -u 1 e. RR
20 19 a1i 
 |-  ( x e. NN -> -u 1 e. RR )
21 0re 
 |-  0 e. RR
22 21 a1i 
 |-  ( x e. NN -> 0 e. RR )
23 neg1lt0 
 |-  -u 1 < 0
24 19 21 23 ltleii 
 |-  -u 1 <_ 0
25 24 a1i 
 |-  ( x e. NN -> -u 1 <_ 0 )
26 nnrp 
 |-  ( x e. NN -> x e. RR+ )
27 26 rpreccld 
 |-  ( x e. NN -> ( 1 / x ) e. RR+ )
28 27 rpge0d 
 |-  ( x e. NN -> 0 <_ ( 1 / x ) )
29 20 22 18 25 28 letrd 
 |-  ( x e. NN -> -u 1 <_ ( 1 / x ) )
30 nnge1 
 |-  ( x e. NN -> 1 <_ x )
31 nnre 
 |-  ( x e. NN -> x e. RR )
32 nngt0 
 |-  ( x e. NN -> 0 < x )
33 1re 
 |-  1 e. RR
34 0lt1 
 |-  0 < 1
35 lerec 
 |-  ( ( ( 1 e. RR /\ 0 < 1 ) /\ ( x e. RR /\ 0 < x ) ) -> ( 1 <_ x <-> ( 1 / x ) <_ ( 1 / 1 ) ) )
36 33 34 35 mpanl12 
 |-  ( ( x e. RR /\ 0 < x ) -> ( 1 <_ x <-> ( 1 / x ) <_ ( 1 / 1 ) ) )
37 31 32 36 syl2anc 
 |-  ( x e. NN -> ( 1 <_ x <-> ( 1 / x ) <_ ( 1 / 1 ) ) )
38 30 37 mpbid 
 |-  ( x e. NN -> ( 1 / x ) <_ ( 1 / 1 ) )
39 1div1e1 
 |-  ( 1 / 1 ) = 1
40 38 39 breqtrdi 
 |-  ( x e. NN -> ( 1 / x ) <_ 1 )
41 19 33 elicc2i 
 |-  ( ( 1 / x ) e. ( -u 1 [,] 1 ) <-> ( ( 1 / x ) e. RR /\ -u 1 <_ ( 1 / x ) /\ ( 1 / x ) <_ 1 ) )
42 18 29 40 41 syl3anbrc 
 |-  ( x e. NN -> ( 1 / x ) e. ( -u 1 [,] 1 ) )
43 17 42 elind 
 |-  ( x e. NN -> ( 1 / x ) e. ( QQ i^i ( -u 1 [,] 1 ) ) )
44 oveq2 
 |-  ( ( 1 / x ) = ( 1 / y ) -> ( 1 / ( 1 / x ) ) = ( 1 / ( 1 / y ) ) )
45 nncn 
 |-  ( x e. NN -> x e. CC )
46 nnne0 
 |-  ( x e. NN -> x =/= 0 )
47 45 46 recrecd 
 |-  ( x e. NN -> ( 1 / ( 1 / x ) ) = x )
48 nncn 
 |-  ( y e. NN -> y e. CC )
49 nnne0 
 |-  ( y e. NN -> y =/= 0 )
50 48 49 recrecd 
 |-  ( y e. NN -> ( 1 / ( 1 / y ) ) = y )
51 47 50 eqeqan12d 
 |-  ( ( x e. NN /\ y e. NN ) -> ( ( 1 / ( 1 / x ) ) = ( 1 / ( 1 / y ) ) <-> x = y ) )
52 44 51 syl5ib 
 |-  ( ( x e. NN /\ y e. NN ) -> ( ( 1 / x ) = ( 1 / y ) -> x = y ) )
53 oveq2 
 |-  ( x = y -> ( 1 / x ) = ( 1 / y ) )
54 52 53 impbid1 
 |-  ( ( x e. NN /\ y e. NN ) -> ( ( 1 / x ) = ( 1 / y ) <-> x = y ) )
55 43 54 dom2 
 |-  ( ( QQ i^i ( -u 1 [,] 1 ) ) e. _V -> NN ~<_ ( QQ i^i ( -u 1 [,] 1 ) ) )
56 16 55 ax-mp 
 |-  NN ~<_ ( QQ i^i ( -u 1 [,] 1 ) )
57 inss1 
 |-  ( QQ i^i ( -u 1 [,] 1 ) ) C_ QQ
58 ssdomg 
 |-  ( QQ e. _V -> ( ( QQ i^i ( -u 1 [,] 1 ) ) C_ QQ -> ( QQ i^i ( -u 1 [,] 1 ) ) ~<_ QQ ) )
59 15 57 58 mp2 
 |-  ( QQ i^i ( -u 1 [,] 1 ) ) ~<_ QQ
60 qnnen 
 |-  QQ ~~ NN
61 domentr 
 |-  ( ( ( QQ i^i ( -u 1 [,] 1 ) ) ~<_ QQ /\ QQ ~~ NN ) -> ( QQ i^i ( -u 1 [,] 1 ) ) ~<_ NN )
62 59 60 61 mp2an 
 |-  ( QQ i^i ( -u 1 [,] 1 ) ) ~<_ NN
63 sbth 
 |-  ( ( NN ~<_ ( QQ i^i ( -u 1 [,] 1 ) ) /\ ( QQ i^i ( -u 1 [,] 1 ) ) ~<_ NN ) -> NN ~~ ( QQ i^i ( -u 1 [,] 1 ) ) )
64 56 62 63 mp2an 
 |-  NN ~~ ( QQ i^i ( -u 1 [,] 1 ) )
65 bren 
 |-  ( NN ~~ ( QQ i^i ( -u 1 [,] 1 ) ) <-> E. g g : NN -1-1-onto-> ( QQ i^i ( -u 1 [,] 1 ) ) )
66 64 65 mpbi 
 |-  E. g g : NN -1-1-onto-> ( QQ i^i ( -u 1 [,] 1 ) )
67 eleq1w 
 |-  ( a = x -> ( a e. ( 0 [,] 1 ) <-> x e. ( 0 [,] 1 ) ) )
68 eleq1w 
 |-  ( b = y -> ( b e. ( 0 [,] 1 ) <-> y e. ( 0 [,] 1 ) ) )
69 67 68 bi2anan9 
 |-  ( ( a = x /\ b = y ) -> ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) <-> ( x e. ( 0 [,] 1 ) /\ y e. ( 0 [,] 1 ) ) ) )
70 oveq12 
 |-  ( ( a = x /\ b = y ) -> ( a - b ) = ( x - y ) )
71 70 eleq1d 
 |-  ( ( a = x /\ b = y ) -> ( ( a - b ) e. QQ <-> ( x - y ) e. QQ ) )
72 69 71 anbi12d 
 |-  ( ( a = x /\ b = y ) -> ( ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) <-> ( ( x e. ( 0 [,] 1 ) /\ y e. ( 0 [,] 1 ) ) /\ ( x - y ) e. QQ ) ) )
73 72 cbvopabv 
 |-  { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } = { <. x , y >. | ( ( x e. ( 0 [,] 1 ) /\ y e. ( 0 [,] 1 ) ) /\ ( x - y ) e. QQ ) }
74 eqid 
 |-  ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) = ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } )
75 fvex 
 |-  ( f ` c ) e. _V
76 eqid 
 |-  ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) = ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) )
77 75 76 fnmpti 
 |-  ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) Fn ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } )
78 77 a1i 
 |-  ( ( ( .< We RR /\ A. z e. ~P RR ( z =/= (/) -> ( f ` z ) e. z ) ) /\ ( g : NN -1-1-onto-> ( QQ i^i ( -u 1 [,] 1 ) ) /\ -. ran ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) e. ( ~P RR \ dom vol ) ) ) -> ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) Fn ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) )
79 neeq1 
 |-  ( z = w -> ( z =/= (/) <-> w =/= (/) ) )
80 fveq2 
 |-  ( z = w -> ( f ` z ) = ( f ` w ) )
81 id 
 |-  ( z = w -> z = w )
82 80 81 eleq12d 
 |-  ( z = w -> ( ( f ` z ) e. z <-> ( f ` w ) e. w ) )
83 79 82 imbi12d 
 |-  ( z = w -> ( ( z =/= (/) -> ( f ` z ) e. z ) <-> ( w =/= (/) -> ( f ` w ) e. w ) ) )
84 83 cbvralvw 
 |-  ( A. z e. ~P RR ( z =/= (/) -> ( f ` z ) e. z ) <-> A. w e. ~P RR ( w =/= (/) -> ( f ` w ) e. w ) )
85 73 vitalilem1 
 |-  { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } Er ( 0 [,] 1 )
86 85 a1i 
 |-  ( T. -> { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } Er ( 0 [,] 1 ) )
87 86 qsss 
 |-  ( T. -> ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) C_ ~P ( 0 [,] 1 ) )
88 87 mptru 
 |-  ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) C_ ~P ( 0 [,] 1 )
89 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
90 89 sspwi 
 |-  ~P ( 0 [,] 1 ) C_ ~P RR
91 88 90 sstri 
 |-  ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) C_ ~P RR
92 ssralv 
 |-  ( ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) C_ ~P RR -> ( A. w e. ~P RR ( w =/= (/) -> ( f ` w ) e. w ) -> A. w e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) ( w =/= (/) -> ( f ` w ) e. w ) ) )
93 91 92 ax-mp 
 |-  ( A. w e. ~P RR ( w =/= (/) -> ( f ` w ) e. w ) -> A. w e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) ( w =/= (/) -> ( f ` w ) e. w ) )
94 84 93 sylbi 
 |-  ( A. z e. ~P RR ( z =/= (/) -> ( f ` z ) e. z ) -> A. w e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) ( w =/= (/) -> ( f ` w ) e. w ) )
95 fveq2 
 |-  ( c = w -> ( f ` c ) = ( f ` w ) )
96 fvex 
 |-  ( f ` w ) e. _V
97 95 76 96 fvmpt 
 |-  ( w e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) -> ( ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) ` w ) = ( f ` w ) )
98 97 eleq1d 
 |-  ( w e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) -> ( ( ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) ` w ) e. w <-> ( f ` w ) e. w ) )
99 98 imbi2d 
 |-  ( w e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) -> ( ( w =/= (/) -> ( ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) ` w ) e. w ) <-> ( w =/= (/) -> ( f ` w ) e. w ) ) )
100 99 ralbiia 
 |-  ( A. w e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) ( w =/= (/) -> ( ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) ` w ) e. w ) <-> A. w e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) ( w =/= (/) -> ( f ` w ) e. w ) )
101 94 100 sylibr 
 |-  ( A. z e. ~P RR ( z =/= (/) -> ( f ` z ) e. z ) -> A. w e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) ( w =/= (/) -> ( ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) ` w ) e. w ) )
102 101 ad2antlr 
 |-  ( ( ( .< We RR /\ A. z e. ~P RR ( z =/= (/) -> ( f ` z ) e. z ) ) /\ ( g : NN -1-1-onto-> ( QQ i^i ( -u 1 [,] 1 ) ) /\ -. ran ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) e. ( ~P RR \ dom vol ) ) ) -> A. w e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) ( w =/= (/) -> ( ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) ` w ) e. w ) )
103 simprl 
 |-  ( ( ( .< We RR /\ A. z e. ~P RR ( z =/= (/) -> ( f ` z ) e. z ) ) /\ ( g : NN -1-1-onto-> ( QQ i^i ( -u 1 [,] 1 ) ) /\ -. ran ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) e. ( ~P RR \ dom vol ) ) ) -> g : NN -1-1-onto-> ( QQ i^i ( -u 1 [,] 1 ) ) )
104 oveq1 
 |-  ( t = s -> ( t - ( g ` m ) ) = ( s - ( g ` m ) ) )
105 104 eleq1d 
 |-  ( t = s -> ( ( t - ( g ` m ) ) e. ran ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) <-> ( s - ( g ` m ) ) e. ran ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) ) )
106 105 cbvrabv 
 |-  { t e. RR | ( t - ( g ` m ) ) e. ran ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) } = { s e. RR | ( s - ( g ` m ) ) e. ran ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) }
107 fveq2 
 |-  ( m = n -> ( g ` m ) = ( g ` n ) )
108 107 oveq2d 
 |-  ( m = n -> ( s - ( g ` m ) ) = ( s - ( g ` n ) ) )
109 108 eleq1d 
 |-  ( m = n -> ( ( s - ( g ` m ) ) e. ran ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) <-> ( s - ( g ` n ) ) e. ran ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) ) )
110 109 rabbidv 
 |-  ( m = n -> { s e. RR | ( s - ( g ` m ) ) e. ran ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) } = { s e. RR | ( s - ( g ` n ) ) e. ran ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) } )
111 106 110 syl5eq 
 |-  ( m = n -> { t e. RR | ( t - ( g ` m ) ) e. ran ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) } = { s e. RR | ( s - ( g ` n ) ) e. ran ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) } )
112 111 cbvmptv 
 |-  ( m e. NN |-> { t e. RR | ( t - ( g ` m ) ) e. ran ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) } ) = ( n e. NN |-> { s e. RR | ( s - ( g ` n ) ) e. ran ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) } )
113 simprr 
 |-  ( ( ( .< We RR /\ A. z e. ~P RR ( z =/= (/) -> ( f ` z ) e. z ) ) /\ ( g : NN -1-1-onto-> ( QQ i^i ( -u 1 [,] 1 ) ) /\ -. ran ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) e. ( ~P RR \ dom vol ) ) ) -> -. ran ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) e. ( ~P RR \ dom vol ) )
114 73 74 78 102 103 112 113 vitalilem5 
 |-  -. ( ( .< We RR /\ A. z e. ~P RR ( z =/= (/) -> ( f ` z ) e. z ) ) /\ ( g : NN -1-1-onto-> ( QQ i^i ( -u 1 [,] 1 ) ) /\ -. ran ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) e. ( ~P RR \ dom vol ) ) )
115 114 pm2.21i 
 |-  ( ( ( .< We RR /\ A. z e. ~P RR ( z =/= (/) -> ( f ` z ) e. z ) ) /\ ( g : NN -1-1-onto-> ( QQ i^i ( -u 1 [,] 1 ) ) /\ -. ran ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) e. ( ~P RR \ dom vol ) ) ) -> ran ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) e. ( ~P RR \ dom vol ) )
116 115 expr 
 |-  ( ( ( .< We RR /\ A. z e. ~P RR ( z =/= (/) -> ( f ` z ) e. z ) ) /\ g : NN -1-1-onto-> ( QQ i^i ( -u 1 [,] 1 ) ) ) -> ( -. ran ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) e. ( ~P RR \ dom vol ) -> ran ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) e. ( ~P RR \ dom vol ) ) )
117 116 pm2.18d 
 |-  ( ( ( .< We RR /\ A. z e. ~P RR ( z =/= (/) -> ( f ` z ) e. z ) ) /\ g : NN -1-1-onto-> ( QQ i^i ( -u 1 [,] 1 ) ) ) -> ran ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) e. ( ~P RR \ dom vol ) )
118 eldif 
 |-  ( ran ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) e. ( ~P RR \ dom vol ) <-> ( ran ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) e. ~P RR /\ -. ran ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) e. dom vol ) )
119 mblss 
 |-  ( x e. dom vol -> x C_ RR )
120 velpw 
 |-  ( x e. ~P RR <-> x C_ RR )
121 119 120 sylibr 
 |-  ( x e. dom vol -> x e. ~P RR )
122 121 ssriv 
 |-  dom vol C_ ~P RR
123 ssnelpss 
 |-  ( dom vol C_ ~P RR -> ( ( ran ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) e. ~P RR /\ -. ran ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) e. dom vol ) -> dom vol C. ~P RR ) )
124 122 123 ax-mp 
 |-  ( ( ran ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) e. ~P RR /\ -. ran ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) e. dom vol ) -> dom vol C. ~P RR )
125 118 124 sylbi 
 |-  ( ran ( c e. ( ( 0 [,] 1 ) /. { <. a , b >. | ( ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) /\ ( a - b ) e. QQ ) } ) |-> ( f ` c ) ) e. ( ~P RR \ dom vol ) -> dom vol C. ~P RR )
126 117 125 syl 
 |-  ( ( ( .< We RR /\ A. z e. ~P RR ( z =/= (/) -> ( f ` z ) e. z ) ) /\ g : NN -1-1-onto-> ( QQ i^i ( -u 1 [,] 1 ) ) ) -> dom vol C. ~P RR )
127 126 ex 
 |-  ( ( .< We RR /\ A. z e. ~P RR ( z =/= (/) -> ( f ` z ) e. z ) ) -> ( g : NN -1-1-onto-> ( QQ i^i ( -u 1 [,] 1 ) ) -> dom vol C. ~P RR ) )
128 127 exlimdv 
 |-  ( ( .< We RR /\ A. z e. ~P RR ( z =/= (/) -> ( f ` z ) e. z ) ) -> ( E. g g : NN -1-1-onto-> ( QQ i^i ( -u 1 [,] 1 ) ) -> dom vol C. ~P RR ) )
129 66 128 mpi 
 |-  ( ( .< We RR /\ A. z e. ~P RR ( z =/= (/) -> ( f ` z ) e. z ) ) -> dom vol C. ~P RR )
130 14 129 exlimddv 
 |-  ( .< We RR -> dom vol C. ~P RR )