Metamath Proof Explorer


Theorem vitalilem5

Description: Lemma for vitali . (Contributed by Mario Carneiro, 16-Jun-2014)

Ref Expression
Hypotheses vitali.1 ˙ = x y | x 0 1 y 0 1 x y
vitali.2 S = 0 1 / ˙
vitali.3 φ F Fn S
vitali.4 φ z S z F z z
vitali.5 φ G : 1-1 onto 1 1
vitali.6 T = n s | s G n ran F
vitali.7 φ ¬ ran F 𝒫 dom vol
Assertion vitalilem5 ¬ φ

Proof

Step Hyp Ref Expression
1 vitali.1 ˙ = x y | x 0 1 y 0 1 x y
2 vitali.2 S = 0 1 / ˙
3 vitali.3 φ F Fn S
4 vitali.4 φ z S z F z z
5 vitali.5 φ G : 1-1 onto 1 1
6 vitali.6 T = n s | s G n ran F
7 vitali.7 φ ¬ ran F 𝒫 dom vol
8 0lt1 0 < 1
9 0re 0
10 1re 1
11 0le1 0 1
12 ovolicc 0 1 0 1 vol * 0 1 = 1 0
13 9 10 11 12 mp3an vol * 0 1 = 1 0
14 1m0e1 1 0 = 1
15 13 14 eqtri vol * 0 1 = 1
16 8 15 breqtrri 0 < vol * 0 1
17 15 10 eqeltri vol * 0 1
18 9 17 ltnlei 0 < vol * 0 1 ¬ vol * 0 1 0
19 16 18 mpbi ¬ vol * 0 1 0
20 1 2 3 4 5 6 7 vitalilem2 φ ran F 0 1 0 1 m T m m T m 1 2
21 20 simp2d φ 0 1 m T m
22 1 vitalilem1 ˙ Er 0 1
23 erdm ˙ Er 0 1 dom ˙ = 0 1
24 22 23 ax-mp dom ˙ = 0 1
25 simpr φ z S z S
26 25 2 eleqtrdi φ z S z 0 1 / ˙
27 elqsn0 dom ˙ = 0 1 z 0 1 / ˙ z
28 24 26 27 sylancr φ z S z
29 22 a1i φ ˙ Er 0 1
30 29 qsss φ 0 1 / ˙ 𝒫 0 1
31 2 30 eqsstrid φ S 𝒫 0 1
32 31 sselda φ z S z 𝒫 0 1
33 32 elpwid φ z S z 0 1
34 33 sseld φ z S F z z F z 0 1
35 28 34 embantd φ z S z F z z F z 0 1
36 35 ralimdva φ z S z F z z z S F z 0 1
37 4 36 mpd φ z S F z 0 1
38 ffnfv F : S 0 1 F Fn S z S F z 0 1
39 3 37 38 sylanbrc φ F : S 0 1
40 39 frnd φ ran F 0 1
41 unitssre 0 1
42 40 41 sstrdi φ ran F
43 reex V
44 43 elpw2 ran F 𝒫 ran F
45 42 44 sylibr φ ran F 𝒫
46 45 anim1i φ ¬ ran F dom vol ran F 𝒫 ¬ ran F dom vol
47 eldif ran F 𝒫 dom vol ran F 𝒫 ¬ ran F dom vol
48 46 47 sylibr φ ¬ ran F dom vol ran F 𝒫 dom vol
49 48 ex φ ¬ ran F dom vol ran F 𝒫 dom vol
50 7 49 mt3d φ ran F dom vol
51 f1of G : 1-1 onto 1 1 G : 1 1
52 5 51 syl φ G : 1 1
53 inss1 1 1
54 qssre
55 53 54 sstri 1 1
56 fss G : 1 1 1 1 G :
57 52 55 56 sylancl φ G :
58 57 ffvelrnda φ n G n
59 shftmbl ran F dom vol G n s | s G n ran F dom vol
60 50 58 59 syl2an2r φ n s | s G n ran F dom vol
61 60 6 fmptd φ T : dom vol
62 61 ffvelrnda φ m T m dom vol
63 62 ralrimiva φ m T m dom vol
64 iunmbl m T m dom vol m T m dom vol
65 63 64 syl φ m T m dom vol
66 mblss m T m dom vol m T m
67 65 66 syl φ m T m
68 ovolss 0 1 m T m m T m vol * 0 1 vol * m T m
69 21 67 68 syl2anc φ vol * 0 1 vol * m T m
70 eqid seq 1 + m vol * T m = seq 1 + m vol * T m
71 eqid m vol * T m = m vol * T m
72 mblss T m dom vol T m
73 62 72 syl φ m T m
74 1 2 3 4 5 6 7 vitalilem4 φ m vol * T m = 0
75 74 9 eqeltrdi φ m vol * T m
76 74 mpteq2dva φ m vol * T m = m 0
77 fconstmpt × 0 = m 0
78 nnuz = 1
79 78 xpeq1i × 0 = 1 × 0
80 77 79 eqtr3i m 0 = 1 × 0
81 76 80 eqtrdi φ m vol * T m = 1 × 0
82 81 seqeq3d φ seq 1 + m vol * T m = seq 1 + 1 × 0
83 1z 1
84 serclim0 1 seq 1 + 1 × 0 0
85 83 84 ax-mp seq 1 + 1 × 0 0
86 82 85 eqbrtrdi φ seq 1 + m vol * T m 0
87 seqex seq 1 + m vol * T m V
88 c0ex 0 V
89 87 88 breldm seq 1 + m vol * T m 0 seq 1 + m vol * T m dom
90 86 89 syl φ seq 1 + m vol * T m dom
91 70 71 73 75 90 ovoliun2 φ vol * m T m m vol * T m
92 74 sumeq2dv φ m vol * T m = m 0
93 78 eqimssi 1
94 93 orci 1 Fin
95 sumz 1 Fin m 0 = 0
96 94 95 ax-mp m 0 = 0
97 92 96 eqtrdi φ m vol * T m = 0
98 91 97 breqtrd φ vol * m T m 0
99 ovolge0 m T m 0 vol * m T m
100 67 99 syl φ 0 vol * m T m
101 ovolcl m T m vol * m T m *
102 67 101 syl φ vol * m T m *
103 0xr 0 *
104 xrletri3 vol * m T m * 0 * vol * m T m = 0 vol * m T m 0 0 vol * m T m
105 102 103 104 sylancl φ vol * m T m = 0 vol * m T m 0 0 vol * m T m
106 98 100 105 mpbir2and φ vol * m T m = 0
107 69 106 breqtrd φ vol * 0 1 0
108 19 107 mto ¬ φ