Metamath Proof Explorer

Theorem pnfnei

Description: A neighborhood of +oo contains an unbounded interval based at a real number. Together with xrtgioo (which describes neighborhoods of RR ) and mnfnei , this gives all "negative" topological information ensuring that it is not too fine (and of course iooordt and similar ensure that it has all the sets we want). (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Assertion pnfnei ( ( 𝐴 ∈ ( 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 mnfxr ⊢ -∞ ∈ ℝ*
13 12 a1i ⊢ ( ( ( +∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( 𝑦 (,] +∞ ) ) ) → -∞ ∈ ℝ* )
14 simprl ⊢ ( ( ( +∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( 𝑦 (,] +∞ ) ) ) → 𝑦 ∈ ℝ* )
15 0xr ⊢ 0 ∈ ℝ*
16 ifcl ⊢ ( ( 𝑦 ∈ ℝ* ∧ 0 ∈ ℝ* ) → if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ∈ ℝ* )
17 14 15 16 sylancl ⊢ ( ( ( +∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( 𝑦 (,] +∞ ) ) ) → if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ∈ ℝ* )
18 pnfxr ⊢ +∞ ∈ ℝ*
19 18 a1i ⊢ ( ( ( +∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( 𝑦 (,] +∞ ) ) ) → +∞ ∈ ℝ* )
20 xrmax1 ⊢ ( ( 0 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → 0 ≤ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) )
21 15 14 20 sylancr ⊢ ( ( ( +∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( 𝑦 (,] +∞ ) ) ) → 0 ≤ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) )
22 ge0gtmnf ⊢ ( ( if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ∈ ℝ* ∧ 0 ≤ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) → -∞ < if ( 0 ≤ 𝑦 , 𝑦 , 0 ) )
23 17 21 22 syl2anc ⊢ ( ( ( +∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( 𝑦 (,] +∞ ) ) ) → -∞ < if ( 0 ≤ 𝑦 , 𝑦 , 0 ) )
24 simpll ⊢ ( ( ( +∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( 𝑦 (,] +∞ ) ) ) → +∞ ∈ 𝑢 )
25 simprr ⊢ ( ( ( +∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( 𝑦 (,] +∞ ) ) ) → 𝑢 = ( 𝑦 (,] +∞ ) )
26 24 25 eleqtrd ⊢ ( ( ( +∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( 𝑦 (,] +∞ ) ) ) → +∞ ∈ ( 𝑦 (,] +∞ ) )
27 elioc1 ⊢ ( ( 𝑦 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( +∞ ∈ ( 𝑦 (,] +∞ ) ↔ ( +∞ ∈ ℝ* ∧ 𝑦 < +∞ ∧ +∞ ≤ +∞ ) ) )
28 14 18 27 sylancl ⊢ ( ( ( +∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( 𝑦 (,] +∞ ) ) ) → ( +∞ ∈ ( 𝑦 (,] +∞ ) ↔ ( +∞ ∈ ℝ* ∧ 𝑦 < +∞ ∧ +∞ ≤ +∞ ) ) )
29 26 28 mpbid ⊢ ( ( ( +∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( 𝑦 (,] +∞ ) ) ) → ( +∞ ∈ ℝ* ∧ 𝑦 < +∞ ∧ +∞ ≤ +∞ ) )
30 29 simp2d ⊢ ( ( ( +∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( 𝑦 (,] +∞ ) ) ) → 𝑦 < +∞ )
31 0ltpnf ⊢ 0 < +∞
32 breq1 ⊢ ( 𝑦 = if ( 0 ≤ 𝑦 , 𝑦 , 0 ) → ( 𝑦 < +∞ ↔ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) < +∞ ) )
33 breq1 ⊢ ( 0 = if ( 0 ≤ 𝑦 , 𝑦 , 0 ) → ( 0 < +∞ ↔ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) < +∞ ) )
34 32 33 ifboth ⊢ ( ( 𝑦 < +∞ ∧ 0 < +∞ ) → if ( 0 ≤ 𝑦 , 𝑦 , 0 ) < +∞ )
35 30 31 34 sylancl ⊢ ( ( ( +∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( 𝑦 (,] +∞ ) ) ) → if ( 0 ≤ 𝑦 , 𝑦 , 0 ) < +∞ )
36 xrre2 ⊢ ( ( ( -∞ ∈ ℝ* ∧ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ∈ ℝ* ∧ +∞ ∈ ℝ* ) ∧ ( -∞ < if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ∧ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) < +∞ ) ) → if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ∈ ℝ )
37 13 17 19 23 35 36 syl32anc ⊢ ( ( ( +∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( 𝑦 (,] +∞ ) ) ) → if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ∈ ℝ )
38 xrmax2 ⊢ ( ( 0 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → 𝑦 ≤ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) )
39 15 14 38 sylancr ⊢ ( ( ( +∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( 𝑦 (,] +∞ ) ) ) → 𝑦 ≤ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) )
40 df-ioc ⊢ (,] = ( 𝑎 ∈ ℝ* , 𝑏 ∈ ℝ* ↦ { 𝑐 ∈ ℝ* ∣ ( 𝑎 < 𝑐 ∧ 𝑐 ≤ 𝑏 ) } )
41 xrlelttr ⊢ ( ( 𝑦 ∈ ℝ* ∧ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) → ( ( 𝑦 ≤ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ∧ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) < 𝑥 ) → 𝑦 < 𝑥 ) )
42 40 40 41 ixxss1 ⊢ ( ( 𝑦 ∈ ℝ* ∧ 𝑦 ≤ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) → ( if ( 0 ≤ 𝑦 , 𝑦 , 0 ) (,] +∞ ) ⊆ ( 𝑦 (,] +∞ ) )
43 14 39 42 syl2anc ⊢ ( ( ( +∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( 𝑦 (,] +∞ ) ) ) → ( if ( 0 ≤ 𝑦 , 𝑦 , 0 ) (,] +∞ ) ⊆ ( 𝑦 (,] +∞ ) )
44 simplr ⊢ ( ( ( +∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( 𝑦 (,] +∞ ) ) ) → 𝑢 ⊆ 𝐴 )
45 25 44 eqsstrrd ⊢ ( ( ( +∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( 𝑦 (,] +∞ ) ) ) → ( 𝑦 (,] +∞ ) ⊆ 𝐴 )
46 43 45 sstrd ⊢ ( ( ( +∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( 𝑦 (,] +∞ ) ) ) → ( if ( 0 ≤ 𝑦 , 𝑦 , 0 ) (,] +∞ ) ⊆ 𝐴 )
47 oveq1 ⊢ ( 𝑥 = if ( 0 ≤ 𝑦 , 𝑦 , 0 ) → ( 𝑥 (,] +∞ ) = ( if ( 0 ≤ 𝑦 , 𝑦 , 0 ) (,] +∞ ) )
48 47 sseq1d ⊢ ( 𝑥 = if ( 0 ≤ 𝑦 , 𝑦 , 0 ) → ( ( 𝑥 (,] +∞ ) ⊆ 𝐴 ↔ ( if ( 0 ≤ 𝑦 , 𝑦 , 0 ) (,] +∞ ) ⊆ 𝐴 ) )
49 48 rspcev ⊢ ( ( if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ∈ ℝ ∧ ( if ( 0 ≤ 𝑦 , 𝑦 , 0 ) (,] +∞ ) ⊆ 𝐴 ) → ∃ 𝑥 ∈ ℝ ( 𝑥 (,] +∞ ) ⊆ 𝐴 )
50 37 46 49 syl2anc ⊢ ( ( ( +∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) ∧ ( 𝑦 ∈ ℝ* ∧ 𝑢 = ( 𝑦 (,] +∞ ) ) ) → ∃ 𝑥 ∈ ℝ ( 𝑥 (,] +∞ ) ⊆ 𝐴 )
51 50 rexlimdvaa ⊢ ( ( +∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) → ( ∃ 𝑦 ∈ ℝ* 𝑢 = ( 𝑦 (,] +∞ ) → ∃ 𝑥 ∈ ℝ ( 𝑥 (,] +∞ ) ⊆ 𝐴 ) )
52 51 com12 ⊢ ( ∃ 𝑦 ∈ ℝ* 𝑢 = ( 𝑦 (,] +∞ ) → ( ( +∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) → ∃ 𝑥 ∈ ℝ ( 𝑥 (,] +∞ ) ⊆ 𝐴 ) )
53 11 52 sylbi ⊢ ( 𝑢 ∈ ran ( 𝑦 ∈ ℝ* ↦ ( 𝑦 (,] +∞ ) ) → ( ( +∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) → ∃ 𝑥 ∈ ℝ ( 𝑥 (,] +∞ ) ⊆ 𝐴 ) )
54 eqid ⊢ ( 𝑦 ∈ ℝ* ↦ ( -∞ [,) 𝑦 ) ) = ( 𝑦 ∈ ℝ* ↦ ( -∞ [,) 𝑦 ) )
55 54 elrnmpt ⊢ ( 𝑢 ∈ V → ( 𝑢 ∈ ran ( 𝑦 ∈ ℝ* ↦ ( -∞ [,) 𝑦 ) ) ↔ ∃ 𝑦 ∈ ℝ* 𝑢 = ( -∞ [,) 𝑦 ) ) )
56 55 elv ⊢ ( 𝑢 ∈ ran ( 𝑦 ∈ ℝ* ↦ ( -∞ [,) 𝑦 ) ) ↔ ∃ 𝑦 ∈ ℝ* 𝑢 = ( -∞ [,) 𝑦 ) )
57 pnfnlt ⊢ ( 𝑦 ∈ ℝ* → ¬ +∞ < 𝑦 )
58 elico1 ⊢ ( ( -∞ ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( +∞ ∈ ( -∞ [,) 𝑦 ) ↔ ( +∞ ∈ ℝ* ∧ -∞ ≤ +∞ ∧ +∞ < 𝑦 ) ) )
59 12 58 mpan ⊢ ( 𝑦 ∈ ℝ* → ( +∞ ∈ ( -∞ [,) 𝑦 ) ↔ ( +∞ ∈ ℝ* ∧ -∞ ≤ +∞ ∧ +∞ < 𝑦 ) ) )
60 simp3 ⊢ ( ( +∞ ∈ ℝ* ∧ -∞ ≤ +∞ ∧ +∞ < 𝑦 ) → +∞ < 𝑦 )
61 59 60 biimtrdi ⊢ ( 𝑦 ∈ ℝ* → ( +∞ ∈ ( -∞ [,) 𝑦 ) → +∞ < 𝑦 ) )
62 57 61 mtod ⊢ ( 𝑦 ∈ ℝ* → ¬ +∞ ∈ ( -∞ [,) 𝑦 ) )
63 eleq2 ⊢ ( 𝑢 = ( -∞ [,) 𝑦 ) → ( +∞ ∈ 𝑢 ↔ +∞ ∈ ( -∞ [,) 𝑦 ) ) )
64 63 notbid ⊢ ( 𝑢 = ( -∞ [,) 𝑦 ) → ( ¬ +∞ ∈ 𝑢 ↔ ¬ +∞ ∈ ( -∞ [,) 𝑦 ) ) )
65 62 64 syl5ibrcom ⊢ ( 𝑦 ∈ ℝ* → ( 𝑢 = ( -∞ [,) 𝑦 ) → ¬ +∞ ∈ 𝑢 ) )
66 65 rexlimiv ⊢ ( ∃ 𝑦 ∈ ℝ* 𝑢 = ( -∞ [,) 𝑦 ) → ¬ +∞ ∈ 𝑢 )
67 66 pm2.21d ⊢ ( ∃ 𝑦 ∈ ℝ* 𝑢 = ( -∞ [,) 𝑦 ) → ( +∞ ∈ 𝑢 → ∃ 𝑥 ∈ ℝ ( 𝑥 (,] +∞ ) ⊆ 𝐴 ) )
68 67 adantrd ⊢ ( ∃ 𝑦 ∈ ℝ* 𝑢 = ( -∞ [,) 𝑦 ) → ( ( +∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) → ∃ 𝑥 ∈ ℝ ( 𝑥 (,] +∞ ) ⊆ 𝐴 ) )
69 56 68 sylbi ⊢ ( 𝑢 ∈ ran ( 𝑦 ∈ ℝ* ↦ ( -∞ [,) 𝑦 ) ) → ( ( +∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) → ∃ 𝑥 ∈ ℝ ( 𝑥 (,] +∞ ) ⊆ 𝐴 ) )
70 53 69 jaoi ⊢ ( ( 𝑢 ∈ ran ( 𝑦 ∈ ℝ* ↦ ( 𝑦 (,] +∞ ) ) ∨ 𝑢 ∈ ran ( 𝑦 ∈ ℝ* ↦ ( -∞ [,) 𝑦 ) ) ) → ( ( +∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) → ∃ 𝑥 ∈ ℝ ( 𝑥 (,] +∞ ) ⊆ 𝐴 ) )
71 8 70 sylbi ⊢ ( 𝑢 ∈ ( ran ( 𝑦 ∈ ℝ* ↦ ( 𝑦 (,] +∞ ) ) ∪ ran ( 𝑦 ∈ ℝ* ↦ ( -∞ [,) 𝑦 ) ) ) → ( ( +∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) → ∃ 𝑥 ∈ ℝ ( 𝑥 (,] +∞ ) ⊆ 𝐴 ) )
72 pnfnre ⊢ +∞ ∉ ℝ
73 72 neli ⊢ ¬ +∞ ∈ ℝ
74 elssuni ⊢ ( 𝑢 ∈ ran (,) → 𝑢 ⊆ ∪ ran (,) )
75 unirnioo ⊢ ℝ = ∪ ran (,)
76 74 75 sseqtrrdi ⊢ ( 𝑢 ∈ ran (,) → 𝑢 ⊆ ℝ )
77 76 sseld ⊢ ( 𝑢 ∈ ran (,) → ( +∞ ∈ 𝑢 → +∞ ∈ ℝ ) )
78 73 77 mtoi ⊢ ( 𝑢 ∈ ran (,) → ¬ +∞ ∈ 𝑢 )
79 78 pm2.21d ⊢ ( 𝑢 ∈ ran (,) → ( +∞ ∈ 𝑢 → ∃ 𝑥 ∈ ℝ ( 𝑥 (,] +∞ ) ⊆ 𝐴 ) )
80 79 adantrd ⊢ ( 𝑢 ∈ ran (,) → ( ( +∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) → ∃ 𝑥 ∈ ℝ ( 𝑥 (,] +∞ ) ⊆ 𝐴 ) )
81 71 80 jaoi ⊢ ( ( 𝑢 ∈ ( ran ( 𝑦 ∈ ℝ* ↦ ( 𝑦 (,] +∞ ) ) ∪ ran ( 𝑦 ∈ ℝ* ↦ ( -∞ [,) 𝑦 ) ) ) ∨ 𝑢 ∈ ran (,) ) → ( ( +∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) → ∃ 𝑥 ∈ ℝ ( 𝑥 (,] +∞ ) ⊆ 𝐴 ) )
82 7 81 sylbi ⊢ ( 𝑢 ∈ ( ( ran ( 𝑦 ∈ ℝ* ↦ ( 𝑦 (,] +∞ ) ) ∪ ran ( 𝑦 ∈ ℝ* ↦ ( -∞ [,) 𝑦 ) ) ) ∪ ran (,) ) → ( ( +∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) → ∃ 𝑥 ∈ ℝ ( 𝑥 (,] +∞ ) ⊆ 𝐴 ) )
83 82 rexlimiv ⊢ ( ∃ 𝑢 ∈ ( ( ran ( 𝑦 ∈ ℝ* ↦ ( 𝑦 (,] +∞ ) ) ∪ ran ( 𝑦 ∈ ℝ* ↦ ( -∞ [,) 𝑦 ) ) ) ∪ ran (,) ) ( +∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴 ) → ∃ 𝑥 ∈ ℝ ( 𝑥 (,] +∞ ) ⊆ 𝐴 )
84 6 83 syl ⊢ ( ( 𝐴 ∈ ( topGen ‘ ( ( ran ( 𝑦 ∈ ℝ* ↦ ( 𝑦 (,] +∞ ) ) ∪ ran ( 𝑦 ∈ ℝ* ↦ ( -∞ [,) 𝑦 ) ) ) ∪ ran (,) ) ) ∧ +∞ ∈ 𝐴 ) → ∃ 𝑥 ∈ ℝ ( 𝑥 (,] +∞ ) ⊆ 𝐴 )
85 5 84 sylanb ⊢ ( ( 𝐴 ∈ ( ordTop ‘ ≤ ) ∧ +∞ ∈ 𝐴 ) → ∃ 𝑥 ∈ ℝ ( 𝑥 (,] +∞ ) ⊆ 𝐴 )