Metamath Proof Explorer


Theorem icccmplem2

Description: Lemma for icccmp . (Contributed by Mario Carneiro, 13-Jun-2014)

Ref Expression
Hypotheses icccmp.1 J = topGen ran .
icccmp.2 T = J 𝑡 A B
icccmp.3 D = abs 2
icccmp.4 S = x A B | z 𝒫 U Fin A x z
icccmp.5 φ A
icccmp.6 φ B
icccmp.7 φ A B
icccmp.8 φ U J
icccmp.9 φ A B U
icccmp.10 φ V U
icccmp.11 φ C +
icccmp.12 φ G ball D C V
icccmp.13 G = sup S <
icccmp.14 R = if G + C 2 B G + C 2 B
Assertion icccmplem2 φ B S

Proof

Step Hyp Ref Expression
1 icccmp.1 J = topGen ran .
2 icccmp.2 T = J 𝑡 A B
3 icccmp.3 D = abs 2
4 icccmp.4 S = x A B | z 𝒫 U Fin A x z
5 icccmp.5 φ A
6 icccmp.6 φ B
7 icccmp.7 φ A B
8 icccmp.8 φ U J
9 icccmp.9 φ A B U
10 icccmp.10 φ V U
11 icccmp.11 φ C +
12 icccmp.12 φ G ball D C V
13 icccmp.13 G = sup S <
14 icccmp.14 R = if G + C 2 B G + C 2 B
15 4 ssrab3 S A B
16 iccssre A B A B
17 5 6 16 syl2anc φ A B
18 15 17 sstrid φ S
19 1 2 3 4 5 6 7 8 9 icccmplem1 φ A S y S y B
20 19 simpld φ A S
21 20 ne0d φ S
22 19 simprd φ y S y B
23 brralrspcev B y S y B n y S y n
24 6 22 23 syl2anc φ n y S y n
25 18 21 24 suprcld φ sup S <
26 13 25 eqeltrid φ G
27 11 rphalfcld φ C 2 +
28 26 27 ltaddrpd φ G < G + C 2
29 27 rpred φ C 2
30 26 29 readdcld φ G + C 2
31 26 30 ltnled φ G < G + C 2 ¬ G + C 2 G
32 28 31 mpbid φ ¬ G + C 2 G
33 30 6 ifcld φ if G + C 2 B G + C 2 B
34 14 33 eqeltrid φ R
35 18 21 24 20 suprubd φ A sup S <
36 35 13 breqtrrdi φ A G
37 26 30 28 ltled φ G G + C 2
38 5 26 30 36 37 letrd φ A G + C 2
39 breq2 G + C 2 = if G + C 2 B G + C 2 B A G + C 2 A if G + C 2 B G + C 2 B
40 breq2 B = if G + C 2 B G + C 2 B A B A if G + C 2 B G + C 2 B
41 39 40 ifboth A G + C 2 A B A if G + C 2 B G + C 2 B
42 38 7 41 syl2anc φ A if G + C 2 B G + C 2 B
43 42 14 breqtrrdi φ A R
44 min2 G + C 2 B if G + C 2 B G + C 2 B B
45 30 6 44 syl2anc φ if G + C 2 B G + C 2 B B
46 14 45 eqbrtrid φ R B
47 elicc2 A B R A B R A R R B
48 5 6 47 syl2anc φ R A B R A R R B
49 34 43 46 48 mpbir3and φ R A B
50 26 11 ltsubrpd φ G C < G
51 50 13 breqtrdi φ G C < sup S <
52 11 rpred φ C
53 26 52 resubcld φ G C
54 suprlub S S n y S y n G C G C < sup S < v S G C < v
55 18 21 24 53 54 syl31anc φ G C < sup S < v S G C < v
56 51 55 mpbid φ v S G C < v
57 oveq2 x = v A x = A v
58 57 sseq1d x = v A x z A v z
59 58 rexbidv x = v z 𝒫 U Fin A x z z 𝒫 U Fin A v z
60 59 4 elrab2 v S v A B z 𝒫 U Fin A v z
61 unieq z = w z = w
62 61 sseq2d z = w A v z A v w
63 62 cbvrexvw z 𝒫 U Fin A v z w 𝒫 U Fin A v w
64 simpr1 φ v A B w 𝒫 U Fin A v w G C < v w 𝒫 U Fin
65 elin w 𝒫 U Fin w 𝒫 U w Fin
66 64 65 sylib φ v A B w 𝒫 U Fin A v w G C < v w 𝒫 U w Fin
67 66 simpld φ v A B w 𝒫 U Fin A v w G C < v w 𝒫 U
68 67 elpwid φ v A B w 𝒫 U Fin A v w G C < v w U
69 simpll φ v A B w 𝒫 U Fin A v w G C < v φ
70 69 10 syl φ v A B w 𝒫 U Fin A v w G C < v V U
71 70 snssd φ v A B w 𝒫 U Fin A v w G C < v V U
72 68 71 unssd φ v A B w 𝒫 U Fin A v w G C < v w V U
73 vex w V
74 snex V V
75 73 74 unex w V V
76 75 elpw w V 𝒫 U w V U
77 72 76 sylibr φ v A B w 𝒫 U Fin A v w G C < v w V 𝒫 U
78 66 simprd φ v A B w 𝒫 U Fin A v w G C < v w Fin
79 snfi V Fin
80 unfi w Fin V Fin w V Fin
81 78 79 80 sylancl φ v A B w 𝒫 U Fin A v w G C < v w V Fin
82 77 81 elind φ v A B w 𝒫 U Fin A v w G C < v w V 𝒫 U Fin
83 simplr2 φ v A B w 𝒫 U Fin A v w G C < v t A R t v A v w
84 ssun1 w w V
85 83 84 sstrdi φ v A B w 𝒫 U Fin A v w G C < v t A R t v A v w V
86 69 5 syl φ v A B w 𝒫 U Fin A v w G C < v A
87 69 34 syl φ v A B w 𝒫 U Fin A v w G C < v R
88 elicc2 A R t A R t A t t R
89 86 87 88 syl2anc φ v A B w 𝒫 U Fin A v w G C < v t A R t A t t R
90 89 biimpa φ v A B w 𝒫 U Fin A v w G C < v t A R t A t t R
91 90 simp1d φ v A B w 𝒫 U Fin A v w G C < v t A R t
92 91 adantrr φ v A B w 𝒫 U Fin A v w G C < v t A R t v t
93 90 simp2d φ v A B w 𝒫 U Fin A v w G C < v t A R A t
94 93 adantrr φ v A B w 𝒫 U Fin A v w G C < v t A R t v A t
95 simprr φ v A B w 𝒫 U Fin A v w G C < v t A R t v t v
96 69 17 syl φ v A B w 𝒫 U Fin A v w G C < v A B
97 simplr φ v A B w 𝒫 U Fin A v w G C < v v A B
98 96 97 sseldd φ v A B w 𝒫 U Fin A v w G C < v v
99 elicc2 A v t A v t A t t v
100 86 98 99 syl2anc φ v A B w 𝒫 U Fin A v w G C < v t A v t A t t v
101 100 adantr φ v A B w 𝒫 U Fin A v w G C < v t A R t v t A v t A t t v
102 92 94 95 101 mpbir3and φ v A B w 𝒫 U Fin A v w G C < v t A R t v t A v
103 85 102 sseldd φ v A B w 𝒫 U Fin A v w G C < v t A R t v t w V
104 103 expr φ v A B w 𝒫 U Fin A v w G C < v t A R t v t w V
105 69 adantr φ v A B w 𝒫 U Fin A v w G C < v t A R v < t φ
106 105 12 syl φ v A B w 𝒫 U Fin A v w G C < v t A R v < t G ball D C V
107 91 adantrr φ v A B w 𝒫 U Fin A v w G C < v t A R v < t t
108 105 53 syl φ v A B w 𝒫 U Fin A v w G C < v t A R v < t G C
109 98 adantr φ v A B w 𝒫 U Fin A v w G C < v t A R v < t v
110 simplr3 φ v A B w 𝒫 U Fin A v w G C < v t A R v < t G C < v
111 simprr φ v A B w 𝒫 U Fin A v w G C < v t A R v < t v < t
112 108 109 107 110 111 lttrd φ v A B w 𝒫 U Fin A v w G C < v t A R v < t G C < t
113 105 34 syl φ v A B w 𝒫 U Fin A v w G C < v t A R v < t R
114 26 52 readdcld φ G + C
115 105 114 syl φ v A B w 𝒫 U Fin A v w G C < v t A R v < t G + C
116 90 simp3d φ v A B w 𝒫 U Fin A v w G C < v t A R t R
117 116 adantrr φ v A B w 𝒫 U Fin A v w G C < v t A R v < t t R
118 min1 G + C 2 B if G + C 2 B G + C 2 B G + C 2
119 30 6 118 syl2anc φ if G + C 2 B G + C 2 B G + C 2
120 14 119 eqbrtrid φ R G + C 2
121 rphalflt C + C 2 < C
122 11 121 syl φ C 2 < C
123 29 52 26 122 ltadd2dd φ G + C 2 < G + C
124 34 30 114 120 123 lelttrd φ R < G + C
125 105 124 syl φ v A B w 𝒫 U Fin A v w G C < v t A R v < t R < G + C
126 107 113 115 117 125 lelttrd φ v A B w 𝒫 U Fin A v w G C < v t A R v < t t < G + C
127 rexr G C G C *
128 rexr G + C G + C *
129 elioo2 G C * G + C * t G C G + C t G C < t t < G + C
130 127 128 129 syl2an G C G + C t G C G + C t G C < t t < G + C
131 108 115 130 syl2anc φ v A B w 𝒫 U Fin A v w G C < v t A R v < t t G C G + C t G C < t t < G + C
132 107 112 126 131 mpbir3and φ v A B w 𝒫 U Fin A v w G C < v t A R v < t t G C G + C
133 105 26 syl φ v A B w 𝒫 U Fin A v w G C < v t A R v < t G
134 105 11 syl φ v A B w 𝒫 U Fin A v w G C < v t A R v < t C +
135 134 rpred φ v A B w 𝒫 U Fin A v w G C < v t A R v < t C
136 3 bl2ioo G C G ball D C = G C G + C
137 133 135 136 syl2anc φ v A B w 𝒫 U Fin A v w G C < v t A R v < t G ball D C = G C G + C
138 132 137 eleqtrrd φ v A B w 𝒫 U Fin A v w G C < v t A R v < t t G ball D C
139 106 138 sseldd φ v A B w 𝒫 U Fin A v w G C < v t A R v < t t V
140 elun2 t V t w V
141 139 140 syl φ v A B w 𝒫 U Fin A v w G C < v t A R v < t t w V
142 141 expr φ v A B w 𝒫 U Fin A v w G C < v t A R v < t t w V
143 98 adantr φ v A B w 𝒫 U Fin A v w G C < v t A R v
144 lelttric t v t v v < t
145 91 143 144 syl2anc φ v A B w 𝒫 U Fin A v w G C < v t A R t v v < t
146 104 142 145 mpjaod φ v A B w 𝒫 U Fin A v w G C < v t A R t w V
147 146 ex φ v A B w 𝒫 U Fin A v w G C < v t A R t w V
148 147 ssrdv φ v A B w 𝒫 U Fin A v w G C < v A R w V
149 uniun w V = w V
150 unisng V U V = V
151 70 150 syl φ v A B w 𝒫 U Fin A v w G C < v V = V
152 151 uneq2d φ v A B w 𝒫 U Fin A v w G C < v w V = w V
153 149 152 syl5eq φ v A B w 𝒫 U Fin A v w G C < v w V = w V
154 148 153 sseqtrrd φ v A B w 𝒫 U Fin A v w G C < v A R w V
155 unieq y = w V y = w V
156 155 sseq2d y = w V A R y A R w V
157 156 rspcev w V 𝒫 U Fin A R w V y 𝒫 U Fin A R y
158 82 154 157 syl2anc φ v A B w 𝒫 U Fin A v w G C < v y 𝒫 U Fin A R y
159 158 3exp2 φ v A B w 𝒫 U Fin A v w G C < v y 𝒫 U Fin A R y
160 159 rexlimdv φ v A B w 𝒫 U Fin A v w G C < v y 𝒫 U Fin A R y
161 63 160 syl5bi φ v A B z 𝒫 U Fin A v z G C < v y 𝒫 U Fin A R y
162 161 expimpd φ v A B z 𝒫 U Fin A v z G C < v y 𝒫 U Fin A R y
163 60 162 syl5bi φ v S G C < v y 𝒫 U Fin A R y
164 163 rexlimdv φ v S G C < v y 𝒫 U Fin A R y
165 56 164 mpd φ y 𝒫 U Fin A R y
166 oveq2 v = R A v = A R
167 166 sseq1d v = R A v y A R y
168 167 rexbidv v = R y 𝒫 U Fin A v y y 𝒫 U Fin A R y
169 unieq z = y z = y
170 169 sseq2d z = y A v z A v y
171 170 cbvrexvw z 𝒫 U Fin A v z y 𝒫 U Fin A v y
172 59 171 bitrdi x = v z 𝒫 U Fin A x z y 𝒫 U Fin A v y
173 172 cbvrabv x A B | z 𝒫 U Fin A x z = v A B | y 𝒫 U Fin A v y
174 4 173 eqtri S = v A B | y 𝒫 U Fin A v y
175 168 174 elrab2 R S R A B y 𝒫 U Fin A R y
176 49 165 175 sylanbrc φ R S
177 18 21 24 176 suprubd φ R sup S <
178 177 13 breqtrrdi φ R G
179 iftrue G + C 2 B if G + C 2 B G + C 2 B = G + C 2
180 14 179 syl5eq G + C 2 B R = G + C 2
181 180 breq1d G + C 2 B R G G + C 2 G
182 178 181 syl5ibcom φ G + C 2 B G + C 2 G
183 32 182 mtod φ ¬ G + C 2 B
184 iffalse ¬ G + C 2 B if G + C 2 B G + C 2 B = B
185 14 184 syl5eq ¬ G + C 2 B R = B
186 183 185 syl φ R = B
187 186 176 eqeltrrd φ B S