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 ‘ ≤ ) ∧ +∞ ∈ 𝐴 ) → ∃ 𝑥 ∈ ℝ ( 𝑥 (,] +∞ ) ⊆ 𝐴 )

Metamath Proof Explorer

Theorem pnfnei

Proof