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 ⊒ ( πœ‘ β†’ 𝐡 ∈ 𝑆 )