Metamath Proof Explorer

Theorem mnfnei

Description: A neighborhood of -oo contains an unbounded interval based at a real number. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Assertion mnfnei ( ( 𝐴 ∈ ( ordTop ‘ ≤ ) ∧ -∞ ∈ 𝐴 ) → ∃ 𝑥 ∈ ℝ ( -∞ [,) 𝑥 ) ⊆ 𝐴 )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ran ( 𝑦 ∈ ℝ* ↦ ( 𝑦 (,] +∞ ) ) = ran ( 𝑦 ∈ ℝ* ↦ ( 𝑦 (,] +∞ ) )
2 eqid ⊢ ran ( 𝑦 ∈ ℝ* ↦ ( -∞ [,) 𝑦 ) ) = ran ( 𝑦 ∈ ℝ* ↦ ( -∞ [,) 𝑦 ) )
3 eqid ⊢ ran (,) = ran (,)
4 1 2 3 leordtval ⊢ ( ordTop ‘ ≤ ) = ( topGen ‘ ( ( ran ( 𝑦 ∈ ℝ* ↦ ( 𝑦 (,] +∞ ) ) ∪ ran ( 𝑦 ∈ ℝ* ↦ ( -∞ [,) 𝑦 ) ) ) ∪ ran (,) ) )
5 4 eleq2i ⊢ ( 𝐴 ∈ ( ordTop ‘ ≤ ) ↔ 𝐴 ∈ ( topGen ‘ ( ( ran ( 𝑦 ∈ ℝ* ↦ ( 𝑦 (,] +∞ ) ) ∪ ran ( 𝑦 ∈ ℝ* ↦ ( -∞ [,) 𝑦 ) ) ) ∪ ran (,) ) ) )
6 tg2 ⊢ ( ( 𝐴 ∈ ( topGen ‘ ( ( ran ( 𝑦 ∈ ℝ* ↦ ( 𝑦 (,] +∞ ) ) ∪ ran ( 𝑦 ∈ ℝ* ↦ ( -∞ [,) 𝑦 ) ) ) ∪ ran (,) ) ) ∧ -∞ ∈ 𝐴 ) → ∃ 𝑢 ∈ ( ( ran ( 𝑦 ∈ ℝ* ↦ ( 𝑦 (,] +∞ ) ) ∪ ran ( 𝑦 ∈ ℝ* ↦ ( -∞ [,) 𝑦 ) ) ) ∪ ran (,) ) ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) )
7 elun ⊢ ( 𝑢 ∈ ( ( ran ( 𝑦 ∈ ℝ* ↦ ( 𝑦 (,] +∞ ) ) ∪ ran ( 𝑦 ∈ ℝ* ↦ ( -∞ [,) 𝑦 ) ) ) ∪ ran (,) ) ↔ ( 𝑢 ∈ ( ran ( 𝑦 ∈ ℝ* ↦ ( 𝑦 (,] +∞ ) ) ∪ ran ( 𝑦 ∈ ℝ* ↦ ( -∞ [,) 𝑦 ) ) ) ∨ 𝑢 ∈ ran (,) ) )
8 elun ⊢ ( 𝑢 ∈ ( ran ( 𝑦 ∈ ℝ* ↦ ( 𝑦 (,] +∞ ) ) ∪ ran ( 𝑦 ∈ ℝ* ↦ ( -∞ [,) 𝑦 ) ) ) ↔ ( 𝑢 ∈ ran ( 𝑦 ∈ ℝ* ↦ ( 𝑦 (,] +∞ ) ) ∨ 𝑢 ∈ ran ( 𝑦 ∈ ℝ* ↦ ( -∞ [,) 𝑦 ) ) ) )
9 eqid ⊢ ( 𝑦 ∈ ℝ* ↦ ( 𝑦 (,] +∞ ) ) = ( 𝑦 ∈ ℝ* ↦ ( 𝑦 (,] +∞ ) )
10 9 elrnmpt ⊢ ( 𝑢 ∈ V → ( 𝑢 ∈ ran ( 𝑦 ∈ ℝ* ↦ ( 𝑦 (,] +∞ ) ) ↔ ∃ 𝑦 ∈ ℝ* 𝑢 = ( 𝑦 (,] +∞ ) ) )
11 10 elv ⊢ ( 𝑢 ∈ ran ( 𝑦 ∈ ℝ* ↦ ( 𝑦 (,] +∞ ) ) ↔ ∃ 𝑦 ∈ ℝ* 𝑢 = ( 𝑦 (,] +∞ ) )
12 nltmnf ⊢ ( 𝑦 ∈ ℝ* → ¬ 𝑦 < -∞ )
13 pnfxr ⊢ +∞ ∈ ℝ*
14 elioc1 ⊢ ( ( 𝑦 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( -∞ ∈ ( 𝑦 (,] +∞ ) ↔ ( -∞ ∈ ℝ* ∧ 𝑦 < -∞ ∧ -∞ ≤ +∞ ) ) )
15 13 14 mpan2 ⊢ ( 𝑦 ∈ ℝ* → ( -∞ ∈ ( 𝑦 (,] +∞ ) ↔ ( -∞ ∈ ℝ* ∧ 𝑦 < -∞ ∧ -∞ ≤ +∞ ) ) )
16 simp2 ⊢ ( ( -∞ ∈ ℝ* ∧ 𝑦 < -∞ ∧ -∞ ≤ +∞ ) → 𝑦 < -∞ )
17 15 16 syl6bi ⊢ ( 𝑦 ∈ ℝ* → ( -∞ ∈ ( 𝑦 (,] +∞ ) → 𝑦 < -∞ ) )
18 12 17 mtod ⊢ ( 𝑦 ∈ ℝ* → ¬ -∞ ∈ ( 𝑦 (,] +∞ ) )
19 eleq2 ⊢ ( 𝑢 = ( 𝑦 (,] +∞ ) → ( -∞ ∈ 𝑢 ↔ -∞ ∈ ( 𝑦 (,] +∞ ) ) )
20 19 notbid ⊢ ( 𝑢 = ( 𝑦 (,] +∞ ) → ( ¬ -∞ ∈ 𝑢 ↔ ¬ -∞ ∈ ( 𝑦 (,] +∞ ) ) )
21 18 20 syl5ibrcom ⊢ ( 𝑦 ∈ ℝ* → ( 𝑢 = ( 𝑦 (,] +∞ ) → ¬ -∞ ∈ 𝑢 ) )
22 21 rexlimiv ⊢ ( ∃ 𝑦 ∈ ℝ* 𝑢 = ( 𝑦 (,] +∞ ) → ¬ -∞ ∈ 𝑢 )
23 22 pm2.21d ⊢ ( ∃ 𝑦 ∈ ℝ* 𝑢 = ( 𝑦 (,] +∞ ) → ( -∞ ∈ 𝑢 → ∃ 𝑥 ∈ ℝ ( -∞ [,) 𝑥 ) ⊆ 𝐴 ) )
24 23 adantrd ⊢ ( ∃ 𝑦 ∈ ℝ* 𝑢 = ( 𝑦 (,] +∞ ) → ( ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) → ∃ 𝑥 ∈ ℝ ( -∞ [,) 𝑥 ) ⊆ 𝐴 ) )
25 11 24 sylbi ⊢ ( 𝑢 ∈ ran ( 𝑦 ∈ ℝ* ↦ ( 𝑦 (,] +∞ ) ) → ( ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) → ∃ 𝑥 ∈ ℝ ( -∞ [,) 𝑥 ) ⊆ 𝐴 ) )
26 eqid ⊢ ( 𝑦 ∈ ℝ* ↦ ( -∞ [,) 𝑦 ) ) = ( 𝑦 ∈ ℝ* ↦ ( -∞ [,) 𝑦 ) )
27 26 elrnmpt ⊢ ( 𝑢 ∈ V → ( 𝑢 ∈ ran ( 𝑦 ∈ ℝ* ↦ ( -∞ [,) 𝑦 ) ) ↔ ∃ 𝑦 ∈ ℝ* 𝑢 = ( -∞ [,) 𝑦 ) ) )
28 27 elv ⊢ ( 𝑢 ∈ ran ( 𝑦 ∈ ℝ* ↦ ( -∞ [,) 𝑦 ) ) ↔ ∃ 𝑦 ∈ ℝ* 𝑢 = ( -∞ [,) 𝑦 ) )
29 mnfxr ⊢ -∞ ∈ ℝ*
30 29 a1i ⊢ ( ( ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( -∞ [,) 𝑦 ) ) ) → -∞ ∈ ℝ* )
31 0xr ⊢ 0 ∈ ℝ*
32 simprl ⊢ ( ( ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( -∞ [,) 𝑦 ) ) ) → 𝑦 ∈ ℝ* )
33 ifcl ⊢ ( ( 0 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → if ( 0 ≤ 𝑦 , 0 , 𝑦 ) ∈ ℝ* )
34 31 32 33 sylancr ⊢ ( ( ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( -∞ [,) 𝑦 ) ) ) → if ( 0 ≤ 𝑦 , 0 , 𝑦 ) ∈ ℝ* )
35 13 a1i ⊢ ( ( ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( -∞ [,) 𝑦 ) ) ) → +∞ ∈ ℝ* )
36 mnflt0 ⊢ -∞ < 0
37 simpll ⊢ ( ( ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( -∞ [,) 𝑦 ) ) ) → -∞ ∈ 𝑢 )
38 simprr ⊢ ( ( ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( -∞ [,) 𝑦 ) ) ) → 𝑢 = ( -∞ [,) 𝑦 ) )
39 37 38 eleqtrd ⊢ ( ( ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( -∞ [,) 𝑦 ) ) ) → -∞ ∈ ( -∞ [,) 𝑦 ) )
40 elico1 ⊢ ( ( -∞ ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( -∞ ∈ ( -∞ [,) 𝑦 ) ↔ ( -∞ ∈ ℝ* ∧ -∞ ≤ -∞ ∧ -∞ < 𝑦 ) ) )
41 29 32 40 sylancr ⊢ ( ( ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( -∞ [,) 𝑦 ) ) ) → ( -∞ ∈ ( -∞ [,) 𝑦 ) ↔ ( -∞ ∈ ℝ* ∧ -∞ ≤ -∞ ∧ -∞ < 𝑦 ) ) )
42 39 41 mpbid ⊢ ( ( ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( -∞ [,) 𝑦 ) ) ) → ( -∞ ∈ ℝ* ∧ -∞ ≤ -∞ ∧ -∞ < 𝑦 ) )
43 42 simp3d ⊢ ( ( ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( -∞ [,) 𝑦 ) ) ) → -∞ < 𝑦 )
44 breq2 ⊢ ( 0 = if ( 0 ≤ 𝑦 , 0 , 𝑦 ) → ( -∞ < 0 ↔ -∞ < if ( 0 ≤ 𝑦 , 0 , 𝑦 ) ) )
45 breq2 ⊢ ( 𝑦 = if ( 0 ≤ 𝑦 , 0 , 𝑦 ) → ( -∞ < 𝑦 ↔ -∞ < if ( 0 ≤ 𝑦 , 0 , 𝑦 ) ) )
46 44 45 ifboth ⊢ ( ( -∞ < 0 ∧ -∞ < 𝑦 ) → -∞ < if ( 0 ≤ 𝑦 , 0 , 𝑦 ) )
47 36 43 46 sylancr ⊢ ( ( ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( -∞ [,) 𝑦 ) ) ) → -∞ < if ( 0 ≤ 𝑦 , 0 , 𝑦 ) )
48 31 a1i ⊢ ( ( ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( -∞ [,) 𝑦 ) ) ) → 0 ∈ ℝ* )
49 xrmin1 ⊢ ( ( 0 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → if ( 0 ≤ 𝑦 , 0 , 𝑦 ) ≤ 0 )
50 31 32 49 sylancr ⊢ ( ( ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( -∞ [,) 𝑦 ) ) ) → if ( 0 ≤ 𝑦 , 0 , 𝑦 ) ≤ 0 )
51 0re ⊢ 0 ∈ ℝ
52 ltpnf ⊢ ( 0 ∈ ℝ → 0 < +∞ )
53 51 52 mp1i ⊢ ( ( ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( -∞ [,) 𝑦 ) ) ) → 0 < +∞ )
54 34 48 35 50 53 xrlelttrd ⊢ ( ( ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( -∞ [,) 𝑦 ) ) ) → if ( 0 ≤ 𝑦 , 0 , 𝑦 ) < +∞ )
55 xrre2 ⊢ ( ( ( -∞ ∈ ℝ* ∧ if ( 0 ≤ 𝑦 , 0 , 𝑦 ) ∈ ℝ* ∧ +∞ ∈ ℝ* ) ∧ ( -∞ < if ( 0 ≤ 𝑦 , 0 , 𝑦 ) ∧ if ( 0 ≤ 𝑦 , 0 , 𝑦 ) < +∞ ) ) → if ( 0 ≤ 𝑦 , 0 , 𝑦 ) ∈ ℝ )
56 30 34 35 47 54 55 syl32anc ⊢ ( ( ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( -∞ [,) 𝑦 ) ) ) → if ( 0 ≤ 𝑦 , 0 , 𝑦 ) ∈ ℝ )
57 xrmin2 ⊢ ( ( 0 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → if ( 0 ≤ 𝑦 , 0 , 𝑦 ) ≤ 𝑦 )
58 31 32 57 sylancr ⊢ ( ( ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( -∞ [,) 𝑦 ) ) ) → if ( 0 ≤ 𝑦 , 0 , 𝑦 ) ≤ 𝑦 )
59 df-ico ⊢ [,) = ( 𝑎 ∈ ℝ* , 𝑏 ∈ ℝ* ↦ { 𝑐 ∈ ℝ* ∣ ( 𝑎 ≤ 𝑐 ∧ 𝑐 < 𝑏 ) } )
60 xrltletr ⊢ ( ( 𝑥 ∈ ℝ* ∧ if ( 0 ≤ 𝑦 , 0 , 𝑦 ) ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( ( 𝑥 < if ( 0 ≤ 𝑦 , 0 , 𝑦 ) ∧ if ( 0 ≤ 𝑦 , 0 , 𝑦 ) ≤ 𝑦 ) → 𝑥 < 𝑦 ) )
61 59 59 60 ixxss2 ⊢ ( ( 𝑦 ∈ ℝ* ∧ if ( 0 ≤ 𝑦 , 0 , 𝑦 ) ≤ 𝑦 ) → ( -∞ [,) if ( 0 ≤ 𝑦 , 0 , 𝑦 ) ) ⊆ ( -∞ [,) 𝑦 ) )
62 32 58 61 syl2anc ⊢ ( ( ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( -∞ [,) 𝑦 ) ) ) → ( -∞ [,) if ( 0 ≤ 𝑦 , 0 , 𝑦 ) ) ⊆ ( -∞ [,) 𝑦 ) )
63 simplr ⊢ ( ( ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( -∞ [,) 𝑦 ) ) ) → 𝑢 ⊆ 𝐴 )
64 38 63 eqsstrrd ⊢ ( ( ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( -∞ [,) 𝑦 ) ) ) → ( -∞ [,) 𝑦 ) ⊆ 𝐴 )
65 62 64 sstrd ⊢ ( ( ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( -∞ [,) 𝑦 ) ) ) → ( -∞ [,) if ( 0 ≤ 𝑦 , 0 , 𝑦 ) ) ⊆ 𝐴 )
66 oveq2 ⊢ ( 𝑥 = if ( 0 ≤ 𝑦 , 0 , 𝑦 ) → ( -∞ [,) 𝑥 ) = ( -∞ [,) if ( 0 ≤ 𝑦 , 0 , 𝑦 ) ) )
67 66 sseq1d ⊢ ( 𝑥 = if ( 0 ≤ 𝑦 , 0 , 𝑦 ) → ( ( -∞ [,) 𝑥 ) ⊆ 𝐴 ↔ ( -∞ [,) if ( 0 ≤ 𝑦 , 0 , 𝑦 ) ) ⊆ 𝐴 ) )
68 67 rspcev ⊢ ( ( if ( 0 ≤ 𝑦 , 0 , 𝑦 ) ∈ ℝ ∧ ( -∞ [,) if ( 0 ≤ 𝑦 , 0 , 𝑦 ) ) ⊆ 𝐴 ) → ∃ 𝑥 ∈ ℝ ( -∞ [,) 𝑥 ) ⊆ 𝐴 )
69 56 65 68 syl2anc ⊢ ( ( ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( -∞ [,) 𝑦 ) ) ) → ∃ 𝑥 ∈ ℝ ( -∞ [,) 𝑥 ) ⊆ 𝐴 )
70 69 rexlimdvaa ⊢ ( ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) → ( ∃ 𝑦 ∈ ℝ* 𝑢 = ( -∞ [,) 𝑦 ) → ∃ 𝑥 ∈ ℝ ( -∞ [,) 𝑥 ) ⊆ 𝐴 ) )
71 70 com12 ⊢ ( ∃ 𝑦 ∈ ℝ* 𝑢 = ( -∞ [,) 𝑦 ) → ( ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) → ∃ 𝑥 ∈ ℝ ( -∞ [,) 𝑥 ) ⊆ 𝐴 ) )
72 28 71 sylbi ⊢ ( 𝑢 ∈ ran ( 𝑦 ∈ ℝ* ↦ ( -∞ [,) 𝑦 ) ) → ( ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) → ∃ 𝑥 ∈ ℝ ( -∞ [,) 𝑥 ) ⊆ 𝐴 ) )
73 25 72 jaoi ⊢ ( ( 𝑢 ∈ ran ( 𝑦 ∈ ℝ* ↦ ( 𝑦 (,] +∞ ) ) ∨ 𝑢 ∈ ran ( 𝑦 ∈ ℝ* ↦ ( -∞ [,) 𝑦 ) ) ) → ( ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) → ∃ 𝑥 ∈ ℝ ( -∞ [,) 𝑥 ) ⊆ 𝐴 ) )
74 8 73 sylbi ⊢ ( 𝑢 ∈ ( ran ( 𝑦 ∈ ℝ* ↦ ( 𝑦 (,] +∞ ) ) ∪ ran ( 𝑦 ∈ ℝ* ↦ ( -∞ [,) 𝑦 ) ) ) → ( ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) → ∃ 𝑥 ∈ ℝ ( -∞ [,) 𝑥 ) ⊆ 𝐴 ) )
75 mnfnre ⊢ -∞ ∉ ℝ
76 75 neli ⊢ ¬ -∞ ∈ ℝ
77 elssuni ⊢ ( 𝑢 ∈ ran (,) → 𝑢 ⊆ ∪ ran (,) )
78 unirnioo ⊢ ℝ = ∪ ran (,)
79 77 78 sseqtrrdi ⊢ ( 𝑢 ∈ ran (,) → 𝑢 ⊆ ℝ )
80 79 sseld ⊢ ( 𝑢 ∈ ran (,) → ( -∞ ∈ 𝑢 → -∞ ∈ ℝ ) )
81 76 80 mtoi ⊢ ( 𝑢 ∈ ran (,) → ¬ -∞ ∈ 𝑢 )
82 81 pm2.21d ⊢ ( 𝑢 ∈ ran (,) → ( -∞ ∈ 𝑢 → ∃ 𝑥 ∈ ℝ ( -∞ [,) 𝑥 ) ⊆ 𝐴 ) )
83 82 adantrd ⊢ ( 𝑢 ∈ ran (,) → ( ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) → ∃ 𝑥 ∈ ℝ ( -∞ [,) 𝑥 ) ⊆ 𝐴 ) )
84 74 83 jaoi ⊢ ( ( 𝑢 ∈ ( ran ( 𝑦 ∈ ℝ* ↦ ( 𝑦 (,] +∞ ) ) ∪ ran ( 𝑦 ∈ ℝ* ↦ ( -∞ [,) 𝑦 ) ) ) ∨ 𝑢 ∈ ran (,) ) → ( ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) → ∃ 𝑥 ∈ ℝ ( -∞ [,) 𝑥 ) ⊆ 𝐴 ) )
85 7 84 sylbi ⊢ ( 𝑢 ∈ ( ( ran ( 𝑦 ∈ ℝ* ↦ ( 𝑦 (,] +∞ ) ) ∪ ran ( 𝑦 ∈ ℝ* ↦ ( -∞ [,) 𝑦 ) ) ) ∪ ran (,) ) → ( ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) → ∃ 𝑥 ∈ ℝ ( -∞ [,) 𝑥 ) ⊆ 𝐴 ) )
86 85 rexlimiv ⊢ ( ∃ 𝑢 ∈ ( ( ran ( 𝑦 ∈ ℝ* ↦ ( 𝑦 (,] +∞ ) ) ∪ ran ( 𝑦 ∈ ℝ* ↦ ( -∞ [,) 𝑦 ) ) ) ∪ ran (,) ) ( -∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) → ∃ 𝑥 ∈ ℝ ( -∞ [,) 𝑥 ) ⊆ 𝐴 )
87 6 86 syl ⊢ ( ( 𝐴 ∈ ( topGen ‘ ( ( ran ( 𝑦 ∈ ℝ* ↦ ( 𝑦 (,] +∞ ) ) ∪ ran ( 𝑦 ∈ ℝ* ↦ ( -∞ [,) 𝑦 ) ) ) ∪ ran (,) ) ) ∧ -∞ ∈ 𝐴 ) → ∃ 𝑥 ∈ ℝ ( -∞ [,) 𝑥 ) ⊆ 𝐴 )
88 5 87 sylanb ⊢ ( ( 𝐴 ∈ ( ordTop ‘ ≤ ) ∧ -∞ ∈ 𝐴 ) → ∃ 𝑥 ∈ ℝ ( -∞ [,) 𝑥 ) ⊆ 𝐴 )