Metamath Proof Explorer

Theorem vitalilem3

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

Ref Expression
Hypotheses vitali.1 ⊢∼˙=xy|x∈01∧y∈01∧x−y∈ℚ
vitali.2 ⊢S=01/∼˙
vitali.3 ⊢φ→FFnS
vitali.4 ⊢φ→∀z∈Sz≠∅→F⁡z∈z
vitali.5 ⊢φ→G:ℕ⟶1-1 ontoℚ∩−11
vitali.6 ⊢T=n∈ℕ⟼s∈ℝ|s−G⁡n∈ran⁡F
vitali.7 ⊢φ→¬ran⁡F∈𝒫ℝ∖dom⁡vol
Assertion vitalilem3 ⊢φ→Disjm∈ℕT⁡m

Proof

Step Hyp Ref Expression
1 vitali.1 ⊢∼˙=xy|x∈01∧y∈01∧x−y∈ℚ
2 vitali.2 ⊢S=01/∼˙
3 vitali.3 ⊢φ→FFnS
4 vitali.4 ⊢φ→∀z∈Sz≠∅→F⁡z∈z
5 vitali.5 ⊢φ→G:ℕ⟶1-1 ontoℚ∩−11
6 vitali.6 ⊢T=n∈ℕ⟼s∈ℝ|s−G⁡n∈ran⁡F
7 vitali.7 ⊢φ→¬ran⁡F∈𝒫ℝ∖dom⁡vol
8 simprlr ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→w∈T⁡m
9 simprll ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→m∈ℕ
10 fveq2 ⊢n=m→G⁡n=G⁡m
11 10 oveq2d ⊢n=m→s−G⁡n=s−G⁡m
12 11 eleq1d ⊢n=m→s−G⁡n∈ran⁡F↔s−G⁡m∈ran⁡F
13 12 rabbidv ⊢n=m→s∈ℝ|s−G⁡n∈ran⁡F=s∈ℝ|s−G⁡m∈ran⁡F
14 reex ⊢ℝ∈V
15 14 rabex ⊢s∈ℝ|s−G⁡m∈ran⁡F∈V
16 13 6 15 fvmpt ⊢m∈ℕ→T⁡m=s∈ℝ|s−G⁡m∈ran⁡F
17 9 16 syl ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→T⁡m=s∈ℝ|s−G⁡m∈ran⁡F
18 8 17 eleqtrd ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→w∈s∈ℝ|s−G⁡m∈ran⁡F
19 oveq1 ⊢s=w→s−G⁡m=w−G⁡m
20 19 eleq1d ⊢s=w→s−G⁡m∈ran⁡F↔w−G⁡m∈ran⁡F
21 20 elrab ⊢w∈s∈ℝ|s−G⁡m∈ran⁡F↔w∈ℝ∧w−G⁡m∈ran⁡F
22 18 21 sylib ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→w∈ℝ∧w−G⁡m∈ran⁡F
23 22 simpld ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→w∈ℝ
24 23 recnd ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→w∈ℂ
25 f1of ⊢G:ℕ⟶1-1 ontoℚ∩−11→G:ℕ⟶ℚ∩−11
26 5 25 syl ⊢φ→G:ℕ⟶ℚ∩−11
27 inss1 ⊢ℚ∩−11⊆ℚ
28 fss ⊢G:ℕ⟶ℚ∩−11∧ℚ∩−11⊆ℚ→G:ℕ⟶ℚ
29 26 27 28 sylancl ⊢φ→G:ℕ⟶ℚ
30 29 adantr ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→G:ℕ⟶ℚ
31 30 9 ffvelcdmd ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→G⁡m∈ℚ
32 qcn ⊢G⁡m∈ℚ→G⁡m∈ℂ
33 31 32 syl ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→G⁡m∈ℂ
34 simprrl ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→k∈ℕ
35 30 34 ffvelcdmd ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→G⁡k∈ℚ
36 qcn ⊢G⁡k∈ℚ→G⁡k∈ℂ
37 35 36 syl ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→G⁡k∈ℂ
38 1 vitalilem1 ⊢∼˙Er01
39 38 a1i ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→∼˙Er01
40 1 2 3 4 5 6 7 vitalilem2 ⊢φ→ran⁡F⊆01∧01⊆⋃m∈ℕT⁡m∧⋃m∈ℕT⁡m⊆−12
41 40 simp1d ⊢φ→ran⁡F⊆01
42 41 adantr ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→ran⁡F⊆01
43 22 simprd ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→w−G⁡m∈ran⁡F
44 42 43 sseldd ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→w−G⁡m∈01
45 simprrr ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→w∈T⁡k
46 fveq2 ⊢n=k→G⁡n=G⁡k
47 46 oveq2d ⊢n=k→s−G⁡n=s−G⁡k
48 47 eleq1d ⊢n=k→s−G⁡n∈ran⁡F↔s−G⁡k∈ran⁡F
49 48 rabbidv ⊢n=k→s∈ℝ|s−G⁡n∈ran⁡F=s∈ℝ|s−G⁡k∈ran⁡F
50 14 rabex ⊢s∈ℝ|s−G⁡k∈ran⁡F∈V
51 49 6 50 fvmpt ⊢k∈ℕ→T⁡k=s∈ℝ|s−G⁡k∈ran⁡F
52 34 51 syl ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→T⁡k=s∈ℝ|s−G⁡k∈ran⁡F
53 45 52 eleqtrd ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→w∈s∈ℝ|s−G⁡k∈ran⁡F
54 oveq1 ⊢s=w→s−G⁡k=w−G⁡k
55 54 eleq1d ⊢s=w→s−G⁡k∈ran⁡F↔w−G⁡k∈ran⁡F
56 55 elrab ⊢w∈s∈ℝ|s−G⁡k∈ran⁡F↔w∈ℝ∧w−G⁡k∈ran⁡F
57 53 56 sylib ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→w∈ℝ∧w−G⁡k∈ran⁡F
58 57 simprd ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→w−G⁡k∈ran⁡F
59 42 58 sseldd ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→w−G⁡k∈01
60 24 33 37 nnncan1d ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→w-G⁡m-w−G⁡k=G⁡k−G⁡m
61 qsubcl ⊢G⁡k∈ℚ∧G⁡m∈ℚ→G⁡k−G⁡m∈ℚ
62 35 31 61 syl2anc ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→G⁡k−G⁡m∈ℚ
63 60 62 eqeltrd ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→w-G⁡m-w−G⁡k∈ℚ
64 oveq12 ⊢x=w−G⁡m∧y=w−G⁡k→x−y=w-G⁡m-w−G⁡k
65 64 eleq1d ⊢x=w−G⁡m∧y=w−G⁡k→x−y∈ℚ↔w-G⁡m-w−G⁡k∈ℚ
66 65 1 brab2a ⊢w−G⁡m∼˙w−G⁡k↔w−G⁡m∈01∧w−G⁡k∈01∧w-G⁡m-w−G⁡k∈ℚ
67 44 59 63 66 syl21anbrc ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→w−G⁡m∼˙w−G⁡k
68 39 67 erthi ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→w−G⁡m∼˙=w−G⁡k∼˙
69 68 fveq2d ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→F⁡w−G⁡m∼˙=F⁡w−G⁡k∼˙
70 eceq1 ⊢z=w−G⁡m→z∼˙=w−G⁡m∼˙
71 70 fveq2d ⊢z=w−G⁡m→F⁡z∼˙=F⁡w−G⁡m∼˙
72 id ⊢z=w−G⁡m→z=w−G⁡m
73 71 72 eqeq12d ⊢z=w−G⁡m→F⁡z∼˙=z↔F⁡w−G⁡m∼˙=w−G⁡m
74 fveq2 ⊢v∼˙=w→F⁡v∼˙=F⁡w
75 74 eceq1d ⊢v∼˙=w→F⁡v∼˙∼˙=F⁡w∼˙
76 75 fveq2d ⊢v∼˙=w→F⁡F⁡v∼˙∼˙=F⁡F⁡w∼˙
77 76 74 eqeq12d ⊢v∼˙=w→F⁡F⁡v∼˙∼˙=F⁡v∼˙↔F⁡F⁡w∼˙=F⁡w
78 38 a1i ⊢φ∧v∈01→∼˙Er01
79 simpr ⊢φ∧v∈01→v∈01
80 erdm ⊢∼˙Er01→dom⁡∼˙=01
81 38 80 ax-mp ⊢dom⁡∼˙=01
82 81 eleq2i ⊢v∈dom⁡∼˙↔v∈01
83 ecdmn0 ⊢v∈dom⁡∼˙↔v∼˙≠∅
84 82 83 bitr3i ⊢v∈01↔v∼˙≠∅
85 79 84 sylib ⊢φ∧v∈01→v∼˙≠∅
86 neeq1 ⊢z=v∼˙→z≠∅↔v∼˙≠∅
87 fveq2 ⊢z=v∼˙→F⁡z=F⁡v∼˙
88 id ⊢z=v∼˙→z=v∼˙
89 87 88 eleq12d ⊢z=v∼˙→F⁡z∈z↔F⁡v∼˙∈v∼˙
90 86 89 imbi12d ⊢z=v∼˙→z≠∅→F⁡z∈z↔v∼˙≠∅→F⁡v∼˙∈v∼˙
91 4 adantr ⊢φ∧v∈01→∀z∈Sz≠∅→F⁡z∈z
92 ovex ⊢01∈V
93 erex ⊢∼˙Er01→01∈V→∼˙∈V
94 38 92 93 mp2 ⊢∼˙∈V
95 94 ecelqsi ⊢v∈01→v∼˙∈01/∼˙
96 95 2 eleqtrrdi ⊢v∈01→v∼˙∈S
97 96 adantl ⊢φ∧v∈01→v∼˙∈S
98 90 91 97 rspcdva ⊢φ∧v∈01→v∼˙≠∅→F⁡v∼˙∈v∼˙
99 85 98 mpd ⊢φ∧v∈01→F⁡v∼˙∈v∼˙
100 fvex ⊢F⁡v∼˙∈V
101 vex ⊢v∈V
102 100 101 elec ⊢F⁡v∼˙∈v∼˙↔v∼˙F⁡v∼˙
103 99 102 sylib ⊢φ∧v∈01→v∼˙F⁡v∼˙
104 78 103 erthi ⊢φ∧v∈01→v∼˙=F⁡v∼˙∼˙
105 104 eqcomd ⊢φ∧v∈01→F⁡v∼˙∼˙=v∼˙
106 105 fveq2d ⊢φ∧v∈01→F⁡F⁡v∼˙∼˙=F⁡v∼˙
107 2 77 106 ectocld ⊢φ∧w∈S→F⁡F⁡w∼˙=F⁡w
108 107 ralrimiva ⊢φ→∀w∈SF⁡F⁡w∼˙=F⁡w
109 eceq1 ⊢z=F⁡w→z∼˙=F⁡w∼˙
110 109 fveq2d ⊢z=F⁡w→F⁡z∼˙=F⁡F⁡w∼˙
111 id ⊢z=F⁡w→z=F⁡w
112 110 111 eqeq12d ⊢z=F⁡w→F⁡z∼˙=z↔F⁡F⁡w∼˙=F⁡w
113 112 ralrn ⊢FFnS→∀z∈ran⁡FF⁡z∼˙=z↔∀w∈SF⁡F⁡w∼˙=F⁡w
114 3 113 syl ⊢φ→∀z∈ran⁡FF⁡z∼˙=z↔∀w∈SF⁡F⁡w∼˙=F⁡w
115 108 114 mpbird ⊢φ→∀z∈ran⁡FF⁡z∼˙=z
116 115 adantr ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→∀z∈ran⁡FF⁡z∼˙=z
117 73 116 43 rspcdva ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→F⁡w−G⁡m∼˙=w−G⁡m
118 eceq1 ⊢z=w−G⁡k→z∼˙=w−G⁡k∼˙
119 118 fveq2d ⊢z=w−G⁡k→F⁡z∼˙=F⁡w−G⁡k∼˙
120 id ⊢z=w−G⁡k→z=w−G⁡k
121 119 120 eqeq12d ⊢z=w−G⁡k→F⁡z∼˙=z↔F⁡w−G⁡k∼˙=w−G⁡k
122 121 116 58 rspcdva ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→F⁡w−G⁡k∼˙=w−G⁡k
123 69 117 122 3eqtr3d ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→w−G⁡m=w−G⁡k
124 24 33 37 123 subcand ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→G⁡m=G⁡k
125 5 adantr ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→G:ℕ⟶1-1 ontoℚ∩−11
126 f1of1 ⊢G:ℕ⟶1-1 ontoℚ∩−11→G:ℕ⟶1-1ℚ∩−11
127 125 126 syl ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→G:ℕ⟶1-1ℚ∩−11
128 f1fveq ⊢G:ℕ⟶1-1ℚ∩−11∧m∈ℕ∧k∈ℕ→G⁡m=G⁡k↔m=k
129 127 9 34 128 syl12anc ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→G⁡m=G⁡k↔m=k
130 124 129 mpbid ⊢φ∧m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→m=k
131 130 ex ⊢φ→m∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→m=k
132 131 alrimivv ⊢φ→∀m∀km∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→m=k
133 eleq1w ⊢m=k→m∈ℕ↔k∈ℕ
134 fveq2 ⊢m=k→T⁡m=T⁡k
135 134 eleq2d ⊢m=k→w∈T⁡m↔w∈T⁡k
136 133 135 anbi12d ⊢m=k→m∈ℕ∧w∈T⁡m↔k∈ℕ∧w∈T⁡k
137 136 mo4 ⊢∃*mm∈ℕ∧w∈T⁡m↔∀m∀km∈ℕ∧w∈T⁡m∧k∈ℕ∧w∈T⁡k→m=k
138 132 137 sylibr ⊢φ→∃*mm∈ℕ∧w∈T⁡m
139 138 alrimiv ⊢φ→∀w∃*mm∈ℕ∧w∈T⁡m
140 dfdisj2 ⊢Disjm∈ℕT⁡m↔∀w∃*mm∈ℕ∧w∈T⁡m
141 139 140 sylibr ⊢φ→Disjm∈ℕT⁡m