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

Metamath Proof Explorer

Theorem mnfnei

Proof