Metamath Proof Explorer

Theorem reconnlem2

Description: Lemma for reconn . (Contributed by Jeff Hankins, 17-Aug-2009) (Proof shortened by Mario Carneiro, 9-Sep-2015)

Ref Expression
Hypotheses reconnlem2.1 ⊒ ( πœ‘ β†’ 𝐴 βŠ† ℝ )
reconnlem2.2 ⊒ ( πœ‘ β†’ π‘ˆ ∈ ( topGen β€˜ ran (,) ) )
reconnlem2.3 ⊒ ( πœ‘ β†’ 𝑉 ∈ ( topGen β€˜ ran (,) ) )
reconnlem2.4 ⊒ ( πœ‘ β†’ βˆ€ π‘₯ ∈ 𝐴 βˆ€ 𝑦 ∈ 𝐴 ( π‘₯ [,] 𝑦 ) βŠ† 𝐴 )
reconnlem2.5 ⊒ ( πœ‘ β†’ 𝐡 ∈ ( π‘ˆ ∩ 𝐴 ) )
reconnlem2.6 ⊒ ( πœ‘ β†’ 𝐢 ∈ ( 𝑉 ∩ 𝐴 ) )
reconnlem2.7 ⊒ ( πœ‘ β†’ ( π‘ˆ ∩ 𝑉 ) βŠ† ( ℝ βˆ– 𝐴 ) )
reconnlem2.8 ⊒ ( πœ‘ β†’ 𝐡 ≀ 𝐢 )
reconnlem2.9 ⊒ 𝑆 = sup ( ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) , ℝ , < )
Assertion reconnlem2 ( πœ‘ β†’ Β¬ 𝐴 βŠ† ( π‘ˆ βˆͺ 𝑉 ) )

Proof

Step Hyp Ref Expression
1 reconnlem2.1 ⊒ ( πœ‘ β†’ 𝐴 βŠ† ℝ )
2 reconnlem2.2 ⊒ ( πœ‘ β†’ π‘ˆ ∈ ( topGen β€˜ ran (,) ) )
3 reconnlem2.3 ⊒ ( πœ‘ β†’ 𝑉 ∈ ( topGen β€˜ ran (,) ) )
4 reconnlem2.4 ⊒ ( πœ‘ β†’ βˆ€ π‘₯ ∈ 𝐴 βˆ€ 𝑦 ∈ 𝐴 ( π‘₯ [,] 𝑦 ) βŠ† 𝐴 )
5 reconnlem2.5 ⊒ ( πœ‘ β†’ 𝐡 ∈ ( π‘ˆ ∩ 𝐴 ) )
6 reconnlem2.6 ⊒ ( πœ‘ β†’ 𝐢 ∈ ( 𝑉 ∩ 𝐴 ) )
7 reconnlem2.7 ⊒ ( πœ‘ β†’ ( π‘ˆ ∩ 𝑉 ) βŠ† ( ℝ βˆ– 𝐴 ) )
8 reconnlem2.8 ⊒ ( πœ‘ β†’ 𝐡 ≀ 𝐢 )
9 reconnlem2.9 ⊒ 𝑆 = sup ( ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) , ℝ , < )
10 inss2 ⊒ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) βŠ† ( 𝐡 [,] 𝐢 )
11 5 elin2d ⊒ ( πœ‘ β†’ 𝐡 ∈ 𝐴 )
12 6 elin2d ⊒ ( πœ‘ β†’ 𝐢 ∈ 𝐴 )
13 oveq1 ⊒ ( π‘₯ = 𝐡 β†’ ( π‘₯ [,] 𝑦 ) = ( 𝐡 [,] 𝑦 ) )
14 13 sseq1d ⊒ ( π‘₯ = 𝐡 β†’ ( ( π‘₯ [,] 𝑦 ) βŠ† 𝐴 ↔ ( 𝐡 [,] 𝑦 ) βŠ† 𝐴 ) )
15 oveq2 ⊒ ( 𝑦 = 𝐢 β†’ ( 𝐡 [,] 𝑦 ) = ( 𝐡 [,] 𝐢 ) )
16 15 sseq1d ⊒ ( 𝑦 = 𝐢 β†’ ( ( 𝐡 [,] 𝑦 ) βŠ† 𝐴 ↔ ( 𝐡 [,] 𝐢 ) βŠ† 𝐴 ) )
17 14 16 rspc2va ⊒ ( ( ( 𝐡 ∈ 𝐴 ∧ 𝐢 ∈ 𝐴 ) ∧ βˆ€ π‘₯ ∈ 𝐴 βˆ€ 𝑦 ∈ 𝐴 ( π‘₯ [,] 𝑦 ) βŠ† 𝐴 ) β†’ ( 𝐡 [,] 𝐢 ) βŠ† 𝐴 )
18 11 12 4 17 syl21anc ⊒ ( πœ‘ β†’ ( 𝐡 [,] 𝐢 ) βŠ† 𝐴 )
19 18 1 sstrd ⊒ ( πœ‘ β†’ ( 𝐡 [,] 𝐢 ) βŠ† ℝ )
20 10 19 sstrid ⊒ ( πœ‘ β†’ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) βŠ† ℝ )
21 5 elin1d ⊒ ( πœ‘ β†’ 𝐡 ∈ π‘ˆ )
22 1 11 sseldd ⊒ ( πœ‘ β†’ 𝐡 ∈ ℝ )
23 22 rexrd ⊒ ( πœ‘ β†’ 𝐡 ∈ ℝ* )
24 1 12 sseldd ⊒ ( πœ‘ β†’ 𝐢 ∈ ℝ )
25 24 rexrd ⊒ ( πœ‘ β†’ 𝐢 ∈ ℝ* )
26 lbicc2 ⊒ ( ( 𝐡 ∈ ℝ* ∧ 𝐢 ∈ ℝ* ∧ 𝐡 ≀ 𝐢 ) β†’ 𝐡 ∈ ( 𝐡 [,] 𝐢 ) )
27 23 25 8 26 syl3anc ⊒ ( πœ‘ β†’ 𝐡 ∈ ( 𝐡 [,] 𝐢 ) )
28 21 27 elind ⊒ ( πœ‘ β†’ 𝐡 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) )
29 28 ne0d ⊒ ( πœ‘ β†’ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) β‰  βˆ… )
30 elinel2 ⊒ ( 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) β†’ 𝑀 ∈ ( 𝐡 [,] 𝐢 ) )
31 elicc2 ⊒ ( ( 𝐡 ∈ ℝ ∧ 𝐢 ∈ ℝ ) β†’ ( 𝑀 ∈ ( 𝐡 [,] 𝐢 ) ↔ ( 𝑀 ∈ ℝ ∧ 𝐡 ≀ 𝑀 ∧ 𝑀 ≀ 𝐢 ) ) )
32 22 24 31 syl2anc ⊒ ( πœ‘ β†’ ( 𝑀 ∈ ( 𝐡 [,] 𝐢 ) ↔ ( 𝑀 ∈ ℝ ∧ 𝐡 ≀ 𝑀 ∧ 𝑀 ≀ 𝐢 ) ) )
33 simp3 ⊒ ( ( 𝑀 ∈ ℝ ∧ 𝐡 ≀ 𝑀 ∧ 𝑀 ≀ 𝐢 ) β†’ 𝑀 ≀ 𝐢 )
34 32 33 syl6bi ⊒ ( πœ‘ β†’ ( 𝑀 ∈ ( 𝐡 [,] 𝐢 ) β†’ 𝑀 ≀ 𝐢 ) )
35 30 34 syl5 ⊒ ( πœ‘ β†’ ( 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) β†’ 𝑀 ≀ 𝐢 ) )
36 35 ralrimiv ⊒ ( πœ‘ β†’ βˆ€ 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) 𝑀 ≀ 𝐢 )
37 brralrspcev ⊒ ( ( 𝐢 ∈ ℝ ∧ βˆ€ 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) 𝑀 ≀ 𝐢 ) β†’ βˆƒ 𝑧 ∈ ℝ βˆ€ 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) 𝑀 ≀ 𝑧 )
38 24 36 37 syl2anc ⊒ ( πœ‘ β†’ βˆƒ 𝑧 ∈ ℝ βˆ€ 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) 𝑀 ≀ 𝑧 )
39 20 29 38 suprcld ⊒ ( πœ‘ β†’ sup ( ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) , ℝ , < ) ∈ ℝ )
40 9 39 eqeltrid ⊒ ( πœ‘ β†’ 𝑆 ∈ ℝ )
41 rphalfcl ⊒ ( π‘Ÿ ∈ ℝ+ β†’ ( π‘Ÿ / 2 ) ∈ ℝ+ )
42 ltaddrp ⊒ ( ( 𝑆 ∈ ℝ ∧ ( π‘Ÿ / 2 ) ∈ ℝ+ ) β†’ 𝑆 < ( 𝑆 + ( π‘Ÿ / 2 ) ) )
43 40 41 42 syl2an ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ 𝑆 < ( 𝑆 + ( π‘Ÿ / 2 ) ) )
44 40 adantr ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ 𝑆 ∈ ℝ )
45 41 rpred ⊒ ( π‘Ÿ ∈ ℝ+ β†’ ( π‘Ÿ / 2 ) ∈ ℝ )
46 readdcl ⊒ ( ( 𝑆 ∈ ℝ ∧ ( π‘Ÿ / 2 ) ∈ ℝ ) β†’ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ℝ )
47 40 45 46 syl2an ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ℝ )
48 44 47 ltnled ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( 𝑆 < ( 𝑆 + ( π‘Ÿ / 2 ) ) ↔ Β¬ ( 𝑆 + ( π‘Ÿ / 2 ) ) ≀ 𝑆 ) )
49 43 48 mpbid ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ Β¬ ( 𝑆 + ( π‘Ÿ / 2 ) ) ≀ 𝑆 )
50 20 ad2antrr ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ) β†’ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) βŠ† ℝ )
51 29 ad2antrr ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ) β†’ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) β‰  βˆ… )
52 38 ad2antrr ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ) β†’ βˆƒ 𝑧 ∈ ℝ βˆ€ 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) 𝑀 ≀ 𝑧 )
53 simpr ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ) β†’ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) )
54 53 elin1d ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ) β†’ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ π‘ˆ )
55 47 adantr ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ) β†’ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ℝ )
56 22 ad2antrr ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ) β†’ 𝐡 ∈ ℝ )
57 40 ad2antrr ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ) β†’ 𝑆 ∈ ℝ )
58 20 29 38 28 suprubd ⊒ ( πœ‘ β†’ 𝐡 ≀ sup ( ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) , ℝ , < ) )
59 58 9 breqtrrdi ⊒ ( πœ‘ β†’ 𝐡 ≀ 𝑆 )
60 59 ad2antrr ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ) β†’ 𝐡 ≀ 𝑆 )
61 43 adantr ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ) β†’ 𝑆 < ( 𝑆 + ( π‘Ÿ / 2 ) ) )
62 57 55 61 ltled ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ) β†’ 𝑆 ≀ ( 𝑆 + ( π‘Ÿ / 2 ) ) )
63 56 57 55 60 62 letrd ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ) β†’ 𝐡 ≀ ( 𝑆 + ( π‘Ÿ / 2 ) ) )
64 24 ad2antrr ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ) β†’ 𝐢 ∈ ℝ )
65 53 elin2d ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ) β†’ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( -∞ (,) 𝐢 ) )
66 eliooord ⊒ ( ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( -∞ (,) 𝐢 ) β†’ ( -∞ < ( 𝑆 + ( π‘Ÿ / 2 ) ) ∧ ( 𝑆 + ( π‘Ÿ / 2 ) ) < 𝐢 ) )
67 66 simprd ⊒ ( ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( -∞ (,) 𝐢 ) β†’ ( 𝑆 + ( π‘Ÿ / 2 ) ) < 𝐢 )
68 65 67 syl ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ) β†’ ( 𝑆 + ( π‘Ÿ / 2 ) ) < 𝐢 )
69 55 64 68 ltled ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ) β†’ ( 𝑆 + ( π‘Ÿ / 2 ) ) ≀ 𝐢 )
70 elicc2 ⊒ ( ( 𝐡 ∈ ℝ ∧ 𝐢 ∈ ℝ ) β†’ ( ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( 𝐡 [,] 𝐢 ) ↔ ( ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ℝ ∧ 𝐡 ≀ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∧ ( 𝑆 + ( π‘Ÿ / 2 ) ) ≀ 𝐢 ) ) )
71 56 64 70 syl2anc ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ) β†’ ( ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( 𝐡 [,] 𝐢 ) ↔ ( ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ℝ ∧ 𝐡 ≀ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∧ ( 𝑆 + ( π‘Ÿ / 2 ) ) ≀ 𝐢 ) ) )
72 55 63 69 71 mpbir3and ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ) β†’ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( 𝐡 [,] 𝐢 ) )
73 54 72 elind ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ) β†’ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) )
74 50 51 52 73 suprubd ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ) β†’ ( 𝑆 + ( π‘Ÿ / 2 ) ) ≀ sup ( ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) , ℝ , < ) )
75 74 9 breqtrrdi ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ) β†’ ( 𝑆 + ( π‘Ÿ / 2 ) ) ≀ 𝑆 )
76 49 75 mtand ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ Β¬ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) )
77 eqid ⊒ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) = ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) )
78 77 remetdval ⊒ ( ( ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ℝ ∧ 𝑆 ∈ ℝ ) β†’ ( ( 𝑆 + ( π‘Ÿ / 2 ) ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) 𝑆 ) = ( abs β€˜ ( ( 𝑆 + ( π‘Ÿ / 2 ) ) βˆ’ 𝑆 ) ) )
79 47 44 78 syl2anc ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( 𝑆 + ( π‘Ÿ / 2 ) ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) 𝑆 ) = ( abs β€˜ ( ( 𝑆 + ( π‘Ÿ / 2 ) ) βˆ’ 𝑆 ) ) )
80 44 recnd ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ 𝑆 ∈ β„‚ )
81 45 adantl ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( π‘Ÿ / 2 ) ∈ ℝ )
82 81 recnd ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( π‘Ÿ / 2 ) ∈ β„‚ )
83 80 82 pncan2d ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( 𝑆 + ( π‘Ÿ / 2 ) ) βˆ’ 𝑆 ) = ( π‘Ÿ / 2 ) )
84 83 fveq2d ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( abs β€˜ ( ( 𝑆 + ( π‘Ÿ / 2 ) ) βˆ’ 𝑆 ) ) = ( abs β€˜ ( π‘Ÿ / 2 ) ) )
85 41 adantl ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( π‘Ÿ / 2 ) ∈ ℝ+ )
86 rpre ⊒ ( ( π‘Ÿ / 2 ) ∈ ℝ+ β†’ ( π‘Ÿ / 2 ) ∈ ℝ )
87 rpge0 ⊒ ( ( π‘Ÿ / 2 ) ∈ ℝ+ β†’ 0 ≀ ( π‘Ÿ / 2 ) )
88 86 87 absidd ⊒ ( ( π‘Ÿ / 2 ) ∈ ℝ+ β†’ ( abs β€˜ ( π‘Ÿ / 2 ) ) = ( π‘Ÿ / 2 ) )
89 85 88 syl ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( abs β€˜ ( π‘Ÿ / 2 ) ) = ( π‘Ÿ / 2 ) )
90 79 84 89 3eqtrd ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( 𝑆 + ( π‘Ÿ / 2 ) ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) 𝑆 ) = ( π‘Ÿ / 2 ) )
91 rphalflt ⊒ ( π‘Ÿ ∈ ℝ+ β†’ ( π‘Ÿ / 2 ) < π‘Ÿ )
92 91 adantl ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( π‘Ÿ / 2 ) < π‘Ÿ )
93 90 92 eqbrtrd ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( 𝑆 + ( π‘Ÿ / 2 ) ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) 𝑆 ) < π‘Ÿ )
94 77 rexmet ⊒ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ∈ ( ∞Met β€˜ ℝ )
95 94 a1i ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ∈ ( ∞Met β€˜ ℝ ) )
96 rpxr ⊒ ( π‘Ÿ ∈ ℝ+ β†’ π‘Ÿ ∈ ℝ* )
97 96 adantl ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ π‘Ÿ ∈ ℝ* )
98 elbl3 ⊒ ( ( ( ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ∈ ( ∞Met β€˜ ℝ ) ∧ π‘Ÿ ∈ ℝ* ) ∧ ( 𝑆 ∈ ℝ ∧ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ℝ ) ) β†’ ( ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( 𝑆 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) π‘Ÿ ) ↔ ( ( 𝑆 + ( π‘Ÿ / 2 ) ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) 𝑆 ) < π‘Ÿ ) )
99 95 97 44 47 98 syl22anc ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( 𝑆 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) π‘Ÿ ) ↔ ( ( 𝑆 + ( π‘Ÿ / 2 ) ) ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) 𝑆 ) < π‘Ÿ ) )
100 93 99 mpbird ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( 𝑆 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) π‘Ÿ ) )
101 ssel ⊒ ( ( 𝑆 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) π‘Ÿ ) βŠ† ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) β†’ ( ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( 𝑆 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) π‘Ÿ ) β†’ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ) )
102 100 101 syl5com ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( 𝑆 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) π‘Ÿ ) βŠ† ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) β†’ ( 𝑆 + ( π‘Ÿ / 2 ) ) ∈ ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ) )
103 76 102 mtod ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ Β¬ ( 𝑆 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) π‘Ÿ ) βŠ† ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) )
104 103 nrexdv ⊒ ( πœ‘ β†’ Β¬ βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑆 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) π‘Ÿ ) βŠ† ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) )
105 40 adantr ⊒ ( ( πœ‘ ∧ 𝑆 ∈ π‘ˆ ) β†’ 𝑆 ∈ ℝ )
106 105 mnfltd ⊒ ( ( πœ‘ ∧ 𝑆 ∈ π‘ˆ ) β†’ -∞ < 𝑆 )
107 suprleub ⊒ ( ( ( ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) βŠ† ℝ ∧ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) β‰  βˆ… ∧ βˆƒ 𝑧 ∈ ℝ βˆ€ 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) 𝑀 ≀ 𝑧 ) ∧ 𝐢 ∈ ℝ ) β†’ ( sup ( ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) , ℝ , < ) ≀ 𝐢 ↔ βˆ€ 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) 𝑀 ≀ 𝐢 ) )
108 20 29 38 24 107 syl31anc ⊒ ( πœ‘ β†’ ( sup ( ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) , ℝ , < ) ≀ 𝐢 ↔ βˆ€ 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) 𝑀 ≀ 𝐢 ) )
109 36 108 mpbird ⊒ ( πœ‘ β†’ sup ( ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) , ℝ , < ) ≀ 𝐢 )
110 9 109 eqbrtrid ⊒ ( πœ‘ β†’ 𝑆 ≀ 𝐢 )
111 40 24 leloed ⊒ ( πœ‘ β†’ ( 𝑆 ≀ 𝐢 ↔ ( 𝑆 < 𝐢 ∨ 𝑆 = 𝐢 ) ) )
112 110 111 mpbid ⊒ ( πœ‘ β†’ ( 𝑆 < 𝐢 ∨ 𝑆 = 𝐢 ) )
113 112 ord ⊒ ( πœ‘ β†’ ( Β¬ 𝑆 < 𝐢 β†’ 𝑆 = 𝐢 ) )
114 elndif ⊒ ( 𝐢 ∈ 𝐴 β†’ Β¬ 𝐢 ∈ ( ℝ βˆ– 𝐴 ) )
115 12 114 syl ⊒ ( πœ‘ β†’ Β¬ 𝐢 ∈ ( ℝ βˆ– 𝐴 ) )
116 6 elin1d ⊒ ( πœ‘ β†’ 𝐢 ∈ 𝑉 )
117 elin ⊒ ( 𝐢 ∈ ( π‘ˆ ∩ 𝑉 ) ↔ ( 𝐢 ∈ π‘ˆ ∧ 𝐢 ∈ 𝑉 ) )
118 7 sseld ⊒ ( πœ‘ β†’ ( 𝐢 ∈ ( π‘ˆ ∩ 𝑉 ) β†’ 𝐢 ∈ ( ℝ βˆ– 𝐴 ) ) )
119 117 118 biimtrrid ⊒ ( πœ‘ β†’ ( ( 𝐢 ∈ π‘ˆ ∧ 𝐢 ∈ 𝑉 ) β†’ 𝐢 ∈ ( ℝ βˆ– 𝐴 ) ) )
120 116 119 mpan2d ⊒ ( πœ‘ β†’ ( 𝐢 ∈ π‘ˆ β†’ 𝐢 ∈ ( ℝ βˆ– 𝐴 ) ) )
121 115 120 mtod ⊒ ( πœ‘ β†’ Β¬ 𝐢 ∈ π‘ˆ )
122 eleq1 ⊒ ( 𝑆 = 𝐢 β†’ ( 𝑆 ∈ π‘ˆ ↔ 𝐢 ∈ π‘ˆ ) )
123 122 notbid ⊒ ( 𝑆 = 𝐢 β†’ ( Β¬ 𝑆 ∈ π‘ˆ ↔ Β¬ 𝐢 ∈ π‘ˆ ) )
124 121 123 syl5ibrcom ⊒ ( πœ‘ β†’ ( 𝑆 = 𝐢 β†’ Β¬ 𝑆 ∈ π‘ˆ ) )
125 113 124 syld ⊒ ( πœ‘ β†’ ( Β¬ 𝑆 < 𝐢 β†’ Β¬ 𝑆 ∈ π‘ˆ ) )
126 125 con4d ⊒ ( πœ‘ β†’ ( 𝑆 ∈ π‘ˆ β†’ 𝑆 < 𝐢 ) )
127 126 imp ⊒ ( ( πœ‘ ∧ 𝑆 ∈ π‘ˆ ) β†’ 𝑆 < 𝐢 )
128 mnfxr ⊒ -∞ ∈ ℝ*
129 elioo2 ⊒ ( ( -∞ ∈ ℝ* ∧ 𝐢 ∈ ℝ* ) β†’ ( 𝑆 ∈ ( -∞ (,) 𝐢 ) ↔ ( 𝑆 ∈ ℝ ∧ -∞ < 𝑆 ∧ 𝑆 < 𝐢 ) ) )
130 128 25 129 sylancr ⊒ ( πœ‘ β†’ ( 𝑆 ∈ ( -∞ (,) 𝐢 ) ↔ ( 𝑆 ∈ ℝ ∧ -∞ < 𝑆 ∧ 𝑆 < 𝐢 ) ) )
131 130 adantr ⊒ ( ( πœ‘ ∧ 𝑆 ∈ π‘ˆ ) β†’ ( 𝑆 ∈ ( -∞ (,) 𝐢 ) ↔ ( 𝑆 ∈ ℝ ∧ -∞ < 𝑆 ∧ 𝑆 < 𝐢 ) ) )
132 105 106 127 131 mpbir3and ⊒ ( ( πœ‘ ∧ 𝑆 ∈ π‘ˆ ) β†’ 𝑆 ∈ ( -∞ (,) 𝐢 ) )
133 132 ex ⊒ ( πœ‘ β†’ ( 𝑆 ∈ π‘ˆ β†’ 𝑆 ∈ ( -∞ (,) 𝐢 ) ) )
134 133 ancld ⊒ ( πœ‘ β†’ ( 𝑆 ∈ π‘ˆ β†’ ( 𝑆 ∈ π‘ˆ ∧ 𝑆 ∈ ( -∞ (,) 𝐢 ) ) ) )
135 elin ⊒ ( 𝑆 ∈ ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ↔ ( 𝑆 ∈ π‘ˆ ∧ 𝑆 ∈ ( -∞ (,) 𝐢 ) ) )
136 retop ⊒ ( topGen β€˜ ran (,) ) ∈ Top
137 iooretop ⊒ ( -∞ (,) 𝐢 ) ∈ ( topGen β€˜ ran (,) )
138 inopn ⊒ ( ( ( topGen β€˜ ran (,) ) ∈ Top ∧ π‘ˆ ∈ ( topGen β€˜ ran (,) ) ∧ ( -∞ (,) 𝐢 ) ∈ ( topGen β€˜ ran (,) ) ) β†’ ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ∈ ( topGen β€˜ ran (,) ) )
139 136 137 138 mp3an13 ⊒ ( π‘ˆ ∈ ( topGen β€˜ ran (,) ) β†’ ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ∈ ( topGen β€˜ ran (,) ) )
140 eqid ⊒ ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) = ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) )
141 77 140 tgioo ⊒ ( topGen β€˜ ran (,) ) = ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) )
142 141 mopni2 ⊒ ( ( ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ∈ ( ∞Met β€˜ ℝ ) ∧ ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ∈ ( topGen β€˜ ran (,) ) ∧ 𝑆 ∈ ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ) β†’ βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑆 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) π‘Ÿ ) βŠ† ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) )
143 94 142 mp3an1 ⊒ ( ( ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ∈ ( topGen β€˜ ran (,) ) ∧ 𝑆 ∈ ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ) β†’ βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑆 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) π‘Ÿ ) βŠ† ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) )
144 143 ex ⊒ ( ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ∈ ( topGen β€˜ ran (,) ) β†’ ( 𝑆 ∈ ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) β†’ βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑆 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) π‘Ÿ ) βŠ† ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ) )
145 2 139 144 3syl ⊒ ( πœ‘ β†’ ( 𝑆 ∈ ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) β†’ βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑆 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) π‘Ÿ ) βŠ† ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ) )
146 135 145 biimtrrid ⊒ ( πœ‘ β†’ ( ( 𝑆 ∈ π‘ˆ ∧ 𝑆 ∈ ( -∞ (,) 𝐢 ) ) β†’ βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑆 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) π‘Ÿ ) βŠ† ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ) )
147 134 146 syld ⊒ ( πœ‘ β†’ ( 𝑆 ∈ π‘ˆ β†’ βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑆 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) π‘Ÿ ) βŠ† ( π‘ˆ ∩ ( -∞ (,) 𝐢 ) ) ) )
148 104 147 mtod ⊒ ( πœ‘ β†’ Β¬ 𝑆 ∈ π‘ˆ )
149 ltsubrp ⊒ ( ( 𝑆 ∈ ℝ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( 𝑆 βˆ’ π‘Ÿ ) < 𝑆 )
150 40 149 sylan ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( 𝑆 βˆ’ π‘Ÿ ) < 𝑆 )
151 rpre ⊒ ( π‘Ÿ ∈ ℝ+ β†’ π‘Ÿ ∈ ℝ )
152 resubcl ⊒ ( ( 𝑆 ∈ ℝ ∧ π‘Ÿ ∈ ℝ ) β†’ ( 𝑆 βˆ’ π‘Ÿ ) ∈ ℝ )
153 40 151 152 syl2an ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( 𝑆 βˆ’ π‘Ÿ ) ∈ ℝ )
154 153 44 ltnled ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( 𝑆 βˆ’ π‘Ÿ ) < 𝑆 ↔ Β¬ 𝑆 ≀ ( 𝑆 βˆ’ π‘Ÿ ) ) )
155 150 154 mpbid ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ Β¬ 𝑆 ≀ ( 𝑆 βˆ’ π‘Ÿ ) )
156 77 bl2ioo ⊒ ( ( 𝑆 ∈ ℝ ∧ π‘Ÿ ∈ ℝ ) β†’ ( 𝑆 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) π‘Ÿ ) = ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) )
157 40 151 156 syl2an ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( 𝑆 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) π‘Ÿ ) = ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) )
158 157 sseq1d ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( 𝑆 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) π‘Ÿ ) βŠ† 𝑉 ↔ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) )
159 20 ad3antrrr ⊒ ( ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) ∧ 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) ) β†’ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) βŠ† ℝ )
160 simpr ⊒ ( ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) ∧ 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) ) β†’ 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) )
161 159 160 sseldd ⊒ ( ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) ∧ 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) ) β†’ 𝑀 ∈ ℝ )
162 153 ad2antrr ⊒ ( ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) ∧ 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) ) β†’ ( 𝑆 βˆ’ π‘Ÿ ) ∈ ℝ )
163 18 ad2antrr ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) β†’ ( 𝐡 [,] 𝐢 ) βŠ† 𝐴 )
164 10 163 sstrid ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) β†’ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) βŠ† 𝐴 )
165 164 sselda ⊒ ( ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) ∧ 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) ) β†’ 𝑀 ∈ 𝐴 )
166 elndif ⊒ ( 𝑀 ∈ 𝐴 β†’ Β¬ 𝑀 ∈ ( ℝ βˆ– 𝐴 ) )
167 165 166 syl ⊒ ( ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) ∧ 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) ) β†’ Β¬ 𝑀 ∈ ( ℝ βˆ– 𝐴 ) )
168 7 ad3antrrr ⊒ ( ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) ∧ ( 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) ∧ ( 𝑆 βˆ’ π‘Ÿ ) < 𝑀 ) ) β†’ ( π‘ˆ ∩ 𝑉 ) βŠ† ( ℝ βˆ– 𝐴 ) )
169 simprl ⊒ ( ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) ∧ ( 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) ∧ ( 𝑆 βˆ’ π‘Ÿ ) < 𝑀 ) ) β†’ 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) )
170 169 elin1d ⊒ ( ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) ∧ ( 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) ∧ ( 𝑆 βˆ’ π‘Ÿ ) < 𝑀 ) ) β†’ 𝑀 ∈ π‘ˆ )
171 simplr ⊒ ( ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) ∧ ( 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) ∧ ( 𝑆 βˆ’ π‘Ÿ ) < 𝑀 ) ) β†’ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 )
172 161 adantrr ⊒ ( ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) ∧ ( 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) ∧ ( 𝑆 βˆ’ π‘Ÿ ) < 𝑀 ) ) β†’ 𝑀 ∈ ℝ )
173 simprr ⊒ ( ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) ∧ ( 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) ∧ ( 𝑆 βˆ’ π‘Ÿ ) < 𝑀 ) ) β†’ ( 𝑆 βˆ’ π‘Ÿ ) < 𝑀 )
174 44 ad2antrr ⊒ ( ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) ∧ ( 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) ∧ ( 𝑆 βˆ’ π‘Ÿ ) < 𝑀 ) ) β†’ 𝑆 ∈ ℝ )
175 simpllr ⊒ ( ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) ∧ ( 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) ∧ ( 𝑆 βˆ’ π‘Ÿ ) < 𝑀 ) ) β†’ π‘Ÿ ∈ ℝ+ )
176 175 rpred ⊒ ( ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) ∧ ( 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) ∧ ( 𝑆 βˆ’ π‘Ÿ ) < 𝑀 ) ) β†’ π‘Ÿ ∈ ℝ )
177 174 176 readdcld ⊒ ( ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) ∧ ( 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) ∧ ( 𝑆 βˆ’ π‘Ÿ ) < 𝑀 ) ) β†’ ( 𝑆 + π‘Ÿ ) ∈ ℝ )
178 159 adantrr ⊒ ( ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) ∧ ( 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) ∧ ( 𝑆 βˆ’ π‘Ÿ ) < 𝑀 ) ) β†’ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) βŠ† ℝ )
179 29 ad3antrrr ⊒ ( ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) ∧ ( 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) ∧ ( 𝑆 βˆ’ π‘Ÿ ) < 𝑀 ) ) β†’ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) β‰  βˆ… )
180 38 ad3antrrr ⊒ ( ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) ∧ ( 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) ∧ ( 𝑆 βˆ’ π‘Ÿ ) < 𝑀 ) ) β†’ βˆƒ 𝑧 ∈ ℝ βˆ€ 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) 𝑀 ≀ 𝑧 )
181 178 179 180 169 suprubd ⊒ ( ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) ∧ ( 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) ∧ ( 𝑆 βˆ’ π‘Ÿ ) < 𝑀 ) ) β†’ 𝑀 ≀ sup ( ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) , ℝ , < ) )
182 181 9 breqtrrdi ⊒ ( ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) ∧ ( 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) ∧ ( 𝑆 βˆ’ π‘Ÿ ) < 𝑀 ) ) β†’ 𝑀 ≀ 𝑆 )
183 174 175 ltaddrpd ⊒ ( ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) ∧ ( 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) ∧ ( 𝑆 βˆ’ π‘Ÿ ) < 𝑀 ) ) β†’ 𝑆 < ( 𝑆 + π‘Ÿ ) )
184 172 174 177 182 183 lelttrd ⊒ ( ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) ∧ ( 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) ∧ ( 𝑆 βˆ’ π‘Ÿ ) < 𝑀 ) ) β†’ 𝑀 < ( 𝑆 + π‘Ÿ ) )
185 153 ad2antrr ⊒ ( ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) ∧ ( 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) ∧ ( 𝑆 βˆ’ π‘Ÿ ) < 𝑀 ) ) β†’ ( 𝑆 βˆ’ π‘Ÿ ) ∈ ℝ )
186 rexr ⊒ ( ( 𝑆 βˆ’ π‘Ÿ ) ∈ ℝ β†’ ( 𝑆 βˆ’ π‘Ÿ ) ∈ ℝ* )
187 rexr ⊒ ( ( 𝑆 + π‘Ÿ ) ∈ ℝ β†’ ( 𝑆 + π‘Ÿ ) ∈ ℝ* )
188 elioo2 ⊒ ( ( ( 𝑆 βˆ’ π‘Ÿ ) ∈ ℝ* ∧ ( 𝑆 + π‘Ÿ ) ∈ ℝ* ) β†’ ( 𝑀 ∈ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) ↔ ( 𝑀 ∈ ℝ ∧ ( 𝑆 βˆ’ π‘Ÿ ) < 𝑀 ∧ 𝑀 < ( 𝑆 + π‘Ÿ ) ) ) )
189 186 187 188 syl2an ⊒ ( ( ( 𝑆 βˆ’ π‘Ÿ ) ∈ ℝ ∧ ( 𝑆 + π‘Ÿ ) ∈ ℝ ) β†’ ( 𝑀 ∈ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) ↔ ( 𝑀 ∈ ℝ ∧ ( 𝑆 βˆ’ π‘Ÿ ) < 𝑀 ∧ 𝑀 < ( 𝑆 + π‘Ÿ ) ) ) )
190 185 177 189 syl2anc ⊒ ( ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) ∧ ( 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) ∧ ( 𝑆 βˆ’ π‘Ÿ ) < 𝑀 ) ) β†’ ( 𝑀 ∈ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) ↔ ( 𝑀 ∈ ℝ ∧ ( 𝑆 βˆ’ π‘Ÿ ) < 𝑀 ∧ 𝑀 < ( 𝑆 + π‘Ÿ ) ) ) )
191 172 173 184 190 mpbir3and ⊒ ( ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) ∧ ( 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) ∧ ( 𝑆 βˆ’ π‘Ÿ ) < 𝑀 ) ) β†’ 𝑀 ∈ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) )
192 171 191 sseldd ⊒ ( ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) ∧ ( 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) ∧ ( 𝑆 βˆ’ π‘Ÿ ) < 𝑀 ) ) β†’ 𝑀 ∈ 𝑉 )
193 170 192 elind ⊒ ( ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) ∧ ( 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) ∧ ( 𝑆 βˆ’ π‘Ÿ ) < 𝑀 ) ) β†’ 𝑀 ∈ ( π‘ˆ ∩ 𝑉 ) )
194 168 193 sseldd ⊒ ( ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) ∧ ( 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) ∧ ( 𝑆 βˆ’ π‘Ÿ ) < 𝑀 ) ) β†’ 𝑀 ∈ ( ℝ βˆ– 𝐴 ) )
195 194 expr ⊒ ( ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) ∧ 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) ) β†’ ( ( 𝑆 βˆ’ π‘Ÿ ) < 𝑀 β†’ 𝑀 ∈ ( ℝ βˆ– 𝐴 ) ) )
196 167 195 mtod ⊒ ( ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) ∧ 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) ) β†’ Β¬ ( 𝑆 βˆ’ π‘Ÿ ) < 𝑀 )
197 161 162 196 nltled ⊒ ( ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) ∧ 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) ) β†’ 𝑀 ≀ ( 𝑆 βˆ’ π‘Ÿ ) )
198 197 ralrimiva ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) β†’ βˆ€ 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) 𝑀 ≀ ( 𝑆 βˆ’ π‘Ÿ ) )
199 20 ad2antrr ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) β†’ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) βŠ† ℝ )
200 29 ad2antrr ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) β†’ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) β‰  βˆ… )
201 38 ad2antrr ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) β†’ βˆƒ 𝑧 ∈ ℝ βˆ€ 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) 𝑀 ≀ 𝑧 )
202 153 adantr ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) β†’ ( 𝑆 βˆ’ π‘Ÿ ) ∈ ℝ )
203 suprleub ⊒ ( ( ( ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) βŠ† ℝ ∧ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) β‰  βˆ… ∧ βˆƒ 𝑧 ∈ ℝ βˆ€ 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) 𝑀 ≀ 𝑧 ) ∧ ( 𝑆 βˆ’ π‘Ÿ ) ∈ ℝ ) β†’ ( sup ( ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) , ℝ , < ) ≀ ( 𝑆 βˆ’ π‘Ÿ ) ↔ βˆ€ 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) 𝑀 ≀ ( 𝑆 βˆ’ π‘Ÿ ) ) )
204 199 200 201 202 203 syl31anc ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) β†’ ( sup ( ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) , ℝ , < ) ≀ ( 𝑆 βˆ’ π‘Ÿ ) ↔ βˆ€ 𝑀 ∈ ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) 𝑀 ≀ ( 𝑆 βˆ’ π‘Ÿ ) ) )
205 198 204 mpbird ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) β†’ sup ( ( π‘ˆ ∩ ( 𝐡 [,] 𝐢 ) ) , ℝ , < ) ≀ ( 𝑆 βˆ’ π‘Ÿ ) )
206 9 205 eqbrtrid ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 ) β†’ 𝑆 ≀ ( 𝑆 βˆ’ π‘Ÿ ) )
207 206 ex ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( ( 𝑆 βˆ’ π‘Ÿ ) (,) ( 𝑆 + π‘Ÿ ) ) βŠ† 𝑉 β†’ 𝑆 ≀ ( 𝑆 βˆ’ π‘Ÿ ) ) )
208 158 207 sylbid ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( 𝑆 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) π‘Ÿ ) βŠ† 𝑉 β†’ 𝑆 ≀ ( 𝑆 βˆ’ π‘Ÿ ) ) )
209 155 208 mtod ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ Β¬ ( 𝑆 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) π‘Ÿ ) βŠ† 𝑉 )
210 209 nrexdv ⊒ ( πœ‘ β†’ Β¬ βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑆 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) π‘Ÿ ) βŠ† 𝑉 )
211 141 mopni2 ⊒ ( ( ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ∈ ( ∞Met β€˜ ℝ ) ∧ 𝑉 ∈ ( topGen β€˜ ran (,) ) ∧ 𝑆 ∈ 𝑉 ) β†’ βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑆 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) π‘Ÿ ) βŠ† 𝑉 )
212 94 211 mp3an1 ⊒ ( ( 𝑉 ∈ ( topGen β€˜ ran (,) ) ∧ 𝑆 ∈ 𝑉 ) β†’ βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑆 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) π‘Ÿ ) βŠ† 𝑉 )
213 212 ex ⊒ ( 𝑉 ∈ ( topGen β€˜ ran (,) ) β†’ ( 𝑆 ∈ 𝑉 β†’ βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑆 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) π‘Ÿ ) βŠ† 𝑉 ) )
214 3 213 syl ⊒ ( πœ‘ β†’ ( 𝑆 ∈ 𝑉 β†’ βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑆 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) π‘Ÿ ) βŠ† 𝑉 ) )
215 210 214 mtod ⊒ ( πœ‘ β†’ Β¬ 𝑆 ∈ 𝑉 )
216 ioran ⊒ ( Β¬ ( 𝑆 ∈ π‘ˆ ∨ 𝑆 ∈ 𝑉 ) ↔ ( Β¬ 𝑆 ∈ π‘ˆ ∧ Β¬ 𝑆 ∈ 𝑉 ) )
217 148 215 216 sylanbrc ⊒ ( πœ‘ β†’ Β¬ ( 𝑆 ∈ π‘ˆ ∨ 𝑆 ∈ 𝑉 ) )
218 elun ⊒ ( 𝑆 ∈ ( π‘ˆ βˆͺ 𝑉 ) ↔ ( 𝑆 ∈ π‘ˆ ∨ 𝑆 ∈ 𝑉 ) )
219 217 218 sylnibr ⊒ ( πœ‘ β†’ Β¬ 𝑆 ∈ ( π‘ˆ βˆͺ 𝑉 ) )
220 elicc2 ⊒ ( ( 𝐡 ∈ ℝ ∧ 𝐢 ∈ ℝ ) β†’ ( 𝑆 ∈ ( 𝐡 [,] 𝐢 ) ↔ ( 𝑆 ∈ ℝ ∧ 𝐡 ≀ 𝑆 ∧ 𝑆 ≀ 𝐢 ) ) )
221 22 24 220 syl2anc ⊒ ( πœ‘ β†’ ( 𝑆 ∈ ( 𝐡 [,] 𝐢 ) ↔ ( 𝑆 ∈ ℝ ∧ 𝐡 ≀ 𝑆 ∧ 𝑆 ≀ 𝐢 ) ) )
222 40 59 110 221 mpbir3and ⊒ ( πœ‘ β†’ 𝑆 ∈ ( 𝐡 [,] 𝐢 ) )
223 18 222 sseldd ⊒ ( πœ‘ β†’ 𝑆 ∈ 𝐴 )
224 ssel ⊒ ( 𝐴 βŠ† ( π‘ˆ βˆͺ 𝑉 ) β†’ ( 𝑆 ∈ 𝐴 β†’ 𝑆 ∈ ( π‘ˆ βˆͺ 𝑉 ) ) )
225 223 224 syl5com ⊒ ( πœ‘ β†’ ( 𝐴 βŠ† ( π‘ˆ βˆͺ 𝑉 ) β†’ 𝑆 ∈ ( π‘ˆ βˆͺ 𝑉 ) ) )
226 219 225 mtod ⊒ ( πœ‘ β†’ Β¬ 𝐴 βŠ† ( π‘ˆ βˆͺ 𝑉 ) )