Metamath Proof Explorer

Theorem icccmplem3

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

Ref Expression
Hypotheses icccmp.1 ⊢ 𝐽 = ( topGen ‘ ran (,) )
icccmp.2 ⊢ 𝑇 = ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) )
icccmp.3 ⊢ 𝐷 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
icccmp.4 ⊢ 𝑆 = { 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∣ ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑥 ) ⊆ ∪ 𝑧 }
icccmp.5 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
icccmp.6 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
icccmp.7 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
icccmp.8 ⊢ ( 𝜑 → 𝑈 ⊆ 𝐽 )
icccmp.9 ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑈 )
Assertion icccmplem3 ( 𝜑 → 𝐵 ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 icccmp.1 ⊢ 𝐽 = ( topGen ‘ ran (,) )
2 icccmp.2 ⊢ 𝑇 = ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) )
3 icccmp.3 ⊢ 𝐷 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
4 icccmp.4 ⊢ 𝑆 = { 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∣ ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑥 ) ⊆ ∪ 𝑧 }
5 icccmp.5 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
6 icccmp.6 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
7 icccmp.7 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
8 icccmp.8 ⊢ ( 𝜑 → 𝑈 ⊆ 𝐽 )
9 icccmp.9 ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑈 )
10 4 ssrab3 ⊢ 𝑆 ⊆ ( 𝐴 [,] 𝐵 )
11 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
12 5 6 11 syl2anc ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
13 10 12 sstrid ⊢ ( 𝜑 → 𝑆 ⊆ ℝ )
14 1 2 3 4 5 6 7 8 9 icccmplem1 ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝐵 ) )
15 14 simpld ⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
16 15 ne0d ⊢ ( 𝜑 → 𝑆 ≠ ∅ )
17 14 simprd ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝐵 )
18 brralrspcev ⊢ ( ( 𝐵 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝐵 ) → ∃ 𝑣 ∈ ℝ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑣 )
19 6 17 18 syl2anc ⊢ ( 𝜑 → ∃ 𝑣 ∈ ℝ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑣 )
20 13 16 19 suprcld ⊢ ( 𝜑 → sup ( 𝑆 , ℝ , < ) ∈ ℝ )
21 13 16 19 15 suprubd ⊢ ( 𝜑 → 𝐴 ≤ sup ( 𝑆 , ℝ , < ) )
22 suprleub ⊢ ( ( ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑣 ∈ ℝ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑣 ) ∧ 𝐵 ∈ ℝ ) → ( sup ( 𝑆 , ℝ , < ) ≤ 𝐵 ↔ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝐵 ) )
23 13 16 19 6 22 syl31anc ⊢ ( 𝜑 → ( sup ( 𝑆 , ℝ , < ) ≤ 𝐵 ↔ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝐵 ) )
24 17 23 mpbird ⊢ ( 𝜑 → sup ( 𝑆 , ℝ , < ) ≤ 𝐵 )
25 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( sup ( 𝑆 , ℝ , < ) ∈ ( 𝐴 [,] 𝐵 ) ↔ ( sup ( 𝑆 , ℝ , < ) ∈ ℝ ∧ 𝐴 ≤ sup ( 𝑆 , ℝ , < ) ∧ sup ( 𝑆 , ℝ , < ) ≤ 𝐵 ) ) )
26 5 6 25 syl2anc ⊢ ( 𝜑 → ( sup ( 𝑆 , ℝ , < ) ∈ ( 𝐴 [,] 𝐵 ) ↔ ( sup ( 𝑆 , ℝ , < ) ∈ ℝ ∧ 𝐴 ≤ sup ( 𝑆 , ℝ , < ) ∧ sup ( 𝑆 , ℝ , < ) ≤ 𝐵 ) ) )
27 20 21 24 26 mpbir3and ⊢ ( 𝜑 → sup ( 𝑆 , ℝ , < ) ∈ ( 𝐴 [,] 𝐵 ) )
28 9 27 sseldd ⊢ ( 𝜑 → sup ( 𝑆 , ℝ , < ) ∈ ∪ 𝑈 )
29 eluni2 ⊢ ( sup ( 𝑆 , ℝ , < ) ∈ ∪ 𝑈 ↔ ∃ 𝑢 ∈ 𝑈 sup ( 𝑆 , ℝ , < ) ∈ 𝑢 )
30 28 29 sylib ⊢ ( 𝜑 → ∃ 𝑢 ∈ 𝑈 sup ( 𝑆 , ℝ , < ) ∈ 𝑢 )
31 8 sselda ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ∈ 𝐽 )
32 3 rexmet ⊢ 𝐷 ∈ ( ∞Met ‘ ℝ )
33 eqid ⊢ ( MetOpen ‘ 𝐷 ) = ( MetOpen ‘ 𝐷 )
34 3 33 tgioo ⊢ ( topGen ‘ ran (,) ) = ( MetOpen ‘ 𝐷 )
35 1 34 eqtri ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
36 35 mopni2 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ ℝ ) ∧ 𝑢 ∈ 𝐽 ∧ sup ( 𝑆 , ℝ , < ) ∈ 𝑢 ) → ∃ 𝑤 ∈ ℝ+ ( sup ( 𝑆 , ℝ , < ) ( ball ‘ 𝐷 ) 𝑤 ) ⊆ 𝑢 )
37 32 36 mp3an1 ⊢ ( ( 𝑢 ∈ 𝐽 ∧ sup ( 𝑆 , ℝ , < ) ∈ 𝑢 ) → ∃ 𝑤 ∈ ℝ+ ( sup ( 𝑆 , ℝ , < ) ( ball ‘ 𝐷 ) 𝑤 ) ⊆ 𝑢 )
38 37 ex ⊢ ( 𝑢 ∈ 𝐽 → ( sup ( 𝑆 , ℝ , < ) ∈ 𝑢 → ∃ 𝑤 ∈ ℝ+ ( sup ( 𝑆 , ℝ , < ) ( ball ‘ 𝐷 ) 𝑤 ) ⊆ 𝑢 ) )
39 31 38 syl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( sup ( 𝑆 , ℝ , < ) ∈ 𝑢 → ∃ 𝑤 ∈ ℝ+ ( sup ( 𝑆 , ℝ , < ) ( ball ‘ 𝐷 ) 𝑤 ) ⊆ 𝑢 ) )
40 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑤 ∈ ℝ+ ∧ ( sup ( 𝑆 , ℝ , < ) ( ball ‘ 𝐷 ) 𝑤 ) ⊆ 𝑢 ) ) → 𝐴 ∈ ℝ )
41 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑤 ∈ ℝ+ ∧ ( sup ( 𝑆 , ℝ , < ) ( ball ‘ 𝐷 ) 𝑤 ) ⊆ 𝑢 ) ) → 𝐵 ∈ ℝ )
42 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑤 ∈ ℝ+ ∧ ( sup ( 𝑆 , ℝ , < ) ( ball ‘ 𝐷 ) 𝑤 ) ⊆ 𝑢 ) ) → 𝐴 ≤ 𝐵 )
43 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑤 ∈ ℝ+ ∧ ( sup ( 𝑆 , ℝ , < ) ( ball ‘ 𝐷 ) 𝑤 ) ⊆ 𝑢 ) ) → 𝑈 ⊆ 𝐽 )
44 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑤 ∈ ℝ+ ∧ ( sup ( 𝑆 , ℝ , < ) ( ball ‘ 𝐷 ) 𝑤 ) ⊆ 𝑢 ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑈 )
45 simplr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑤 ∈ ℝ+ ∧ ( sup ( 𝑆 , ℝ , < ) ( ball ‘ 𝐷 ) 𝑤 ) ⊆ 𝑢 ) ) → 𝑢 ∈ 𝑈 )
46 simprl ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑤 ∈ ℝ+ ∧ ( sup ( 𝑆 , ℝ , < ) ( ball ‘ 𝐷 ) 𝑤 ) ⊆ 𝑢 ) ) → 𝑤 ∈ ℝ+ )
47 simprr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑤 ∈ ℝ+ ∧ ( sup ( 𝑆 , ℝ , < ) ( ball ‘ 𝐷 ) 𝑤 ) ⊆ 𝑢 ) ) → ( sup ( 𝑆 , ℝ , < ) ( ball ‘ 𝐷 ) 𝑤 ) ⊆ 𝑢 )
48 eqid ⊢ sup ( 𝑆 , ℝ , < ) = sup ( 𝑆 , ℝ , < )
49 eqid ⊢ if ( ( sup ( 𝑆 , ℝ , < ) + ( 𝑤 / 2 ) ) ≤ 𝐵 , ( sup ( 𝑆 , ℝ , < ) + ( 𝑤 / 2 ) ) , 𝐵 ) = if ( ( sup ( 𝑆 , ℝ , < ) + ( 𝑤 / 2 ) ) ≤ 𝐵 , ( sup ( 𝑆 , ℝ , < ) + ( 𝑤 / 2 ) ) , 𝐵 )
50 1 2 3 4 40 41 42 43 44 45 46 47 48 49 icccmplem2 ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑤 ∈ ℝ+ ∧ ( sup ( 𝑆 , ℝ , < ) ( ball ‘ 𝐷 ) 𝑤 ) ⊆ 𝑢 ) ) → 𝐵 ∈ 𝑆 )
51 50 rexlimdvaa ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( ∃ 𝑤 ∈ ℝ+ ( sup ( 𝑆 , ℝ , < ) ( ball ‘ 𝐷 ) 𝑤 ) ⊆ 𝑢 → 𝐵 ∈ 𝑆 ) )
52 39 51 syld ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( sup ( 𝑆 , ℝ , < ) ∈ 𝑢 → 𝐵 ∈ 𝑆 ) )
53 52 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑢 ∈ 𝑈 sup ( 𝑆 , ℝ , < ) ∈ 𝑢 → 𝐵 ∈ 𝑆 ) )
54 30 53 mpd ⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )