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	$⊢ (A \in ordTop (\leq) \land −∞ \in A) \to \exists x \in ℝ [−∞, x) \subseteq A$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ ran (y \in ℝ^{} ⟼ (y, +∞]) = ran (y \in ℝ^{} ⟼ (y, +∞])$
2		eqid	$⊢ ran (y \in ℝ^{} ⟼ [−∞, y)) = ran (y \in ℝ^{} ⟼ [−∞, y))$
3		eqid	$⊢ ran (.) = ran (.)$
4	1 2 3	leordtval	$⊢ ordTop (\leq) = topGen ((ran (y \in ℝ^{} ⟼ (y, +∞]) \cup ran (y \in ℝ^{} ⟼ [−∞, y))) \cup ran (.))$
5	4	eleq2i	$⊢ A \in ordTop (\leq) \leftrightarrow A \in topGen ((ran (y \in ℝ^{} ⟼ (y, +∞]) \cup ran (y \in ℝ^{} ⟼ [−∞, y))) \cup ran (.))$
6		tg2	$⊢ (A \in topGen ((ran (y \in ℝ^{} ⟼ (y, +∞]) \cup ran (y \in ℝ^{} ⟼ [−∞, y))) \cup ran (.)) \land −∞ \in A) \to \exists u \in ((ran (y \in ℝ^{} ⟼ (y, +∞]) \cup ran (y \in ℝ^{} ⟼ [−∞, y))) \cup ran (.)) (−∞ \in u \land u \subseteq A)$
7		elun	$⊢ u \in ((ran (y \in ℝ^{} ⟼ (y, +∞]) \cup ran (y \in ℝ^{} ⟼ [−∞, y))) \cup ran (.)) \leftrightarrow (u \in (ran (y \in ℝ^{} ⟼ (y, +∞]) \cup ran (y \in ℝ^{} ⟼ [−∞, y))) \lor u \in ran (.))$
8		elun	$⊢ u \in (ran (y \in ℝ^{} ⟼ (y, +∞]) \cup ran (y \in ℝ^{} ⟼ [−∞, y))) \leftrightarrow (u \in ran (y \in ℝ^{} ⟼ (y, +∞]) \lor u \in ran (y \in ℝ^{} ⟼ [−∞, y)))$
9		eqid	$⊢ (y \in ℝ^{} ⟼ (y, +∞]) = (y \in ℝ^{} ⟼ (y, +∞])$
10	9	elrnmpt	$⊢ u \in V \to (u \in ran (y \in ℝ^{} ⟼ (y, +∞]) \leftrightarrow \exists y \in ℝ^{} u = (y, +∞])$
11	10	elv	$⊢ u \in ran (y \in ℝ^{} ⟼ (y, +∞]) \leftrightarrow \exists y \in ℝ^{} u = (y, +∞]$
12		nltmnf	$⊢ y \in ℝ^{*} \to \neg y < −∞$
13		pnfxr	$⊢ +∞ \in ℝ^{*}$
14		elioc1	$⊢ (y \in ℝ^{} \land +∞ \in ℝ^{}) \to (−∞ \in (y, +∞] \leftrightarrow (−∞ \in ℝ^{*} \land y < −∞ \land −∞ \leq +∞))$
15	13 14	mpan2	$⊢ y \in ℝ^{} \to (−∞ \in (y, +∞] \leftrightarrow (−∞ \in ℝ^{} \land y < −∞ \land −∞ \leq +∞))$
16		simp2	$⊢ (−∞ \in ℝ^{*} \land y < −∞ \land −∞ \leq +∞) \to y < −∞$
17	15 16	syl6bi	$⊢ y \in ℝ^{*} \to (−∞ \in (y, +∞] \to y < −∞)$
18	12 17	mtod	$⊢ y \in ℝ^{*} \to \neg −∞ \in (y, +∞]$
19		eleq2	$⊢ u = (y, +∞] \to (−∞ \in u \leftrightarrow −∞ \in (y, +∞])$
20	19	notbid	$⊢ u = (y, +∞] \to (\neg −∞ \in u \leftrightarrow \neg −∞ \in (y, +∞])$
21	18 20	syl5ibrcom	$⊢ y \in ℝ^{*} \to (u = (y, +∞] \to \neg −∞ \in u)$
22	21	rexlimiv	$⊢ \exists y \in ℝ^{*} u = (y, +∞] \to \neg −∞ \in u$
23	22	pm2.21d	$⊢ \exists y \in ℝ^{*} u = (y, +∞] \to (−∞ \in u \to \exists x \in ℝ [−∞, x) \subseteq A)$
24	23	adantrd	$⊢ \exists y \in ℝ^{*} u = (y, +∞] \to ((−∞ \in u \land u \subseteq A) \to \exists x \in ℝ [−∞, x) \subseteq A)$
25	11 24	sylbi	$⊢ u \in ran (y \in ℝ^{*} ⟼ (y, +∞]) \to ((−∞ \in u \land u \subseteq A) \to \exists x \in ℝ [−∞, x) \subseteq A)$
26		eqid	$⊢ (y \in ℝ^{} ⟼ [−∞, y)) = (y \in ℝ^{} ⟼ [−∞, y))$
27	26	elrnmpt	$⊢ u \in V \to (u \in ran (y \in ℝ^{} ⟼ [−∞, y)) \leftrightarrow \exists y \in ℝ^{} u = [−∞, y))$
28	27	elv	$⊢ u \in ran (y \in ℝ^{} ⟼ [−∞, y)) \leftrightarrow \exists y \in ℝ^{} u = [−∞, y)$
29		mnfxr	$⊢ −∞ \in ℝ^{*}$
30	29	a1i	$⊢ ((−∞ \in u \land u \subseteq A) \land (y \in ℝ^{} \land u = [−∞, y))) \to −∞ \in ℝ^{}$
31		0xr	$⊢ 0 \in ℝ^{*}$
32		simprl	$⊢ ((−∞ \in u \land u \subseteq A) \land (y \in ℝ^{} \land u = [−∞, y))) \to y \in ℝ^{}$
33		ifcl	$⊢ (0 \in ℝ^{} \land y \in ℝ^{}) \to if (0 \leq y, 0, y) \in ℝ^{*}$
34	31 32 33	sylancr	$⊢ ((−∞ \in u \land u \subseteq A) \land (y \in ℝ^{} \land u = [−∞, y))) \to if (0 \leq y, 0, y) \in ℝ^{}$
35	13	a1i	$⊢ ((−∞ \in u \land u \subseteq A) \land (y \in ℝ^{} \land u = [−∞, y))) \to +∞ \in ℝ^{}$
36		mnflt0	$⊢ −∞ < 0$
37		simpll	$⊢ ((−∞ \in u \land u \subseteq A) \land (y \in ℝ^{*} \land u = [−∞, y))) \to −∞ \in u$
38		simprr	$⊢ ((−∞ \in u \land u \subseteq A) \land (y \in ℝ^{*} \land u = [−∞, y))) \to u = [−∞, y)$
39	37 38	eleqtrd	$⊢ ((−∞ \in u \land u \subseteq A) \land (y \in ℝ^{*} \land u = [−∞, y))) \to −∞ \in [−∞, y)$
40		elico1	$⊢ (−∞ \in ℝ^{} \land y \in ℝ^{}) \to (−∞ \in [−∞, y) \leftrightarrow (−∞ \in ℝ^{*} \land −∞ \leq −∞ \land −∞ < y))$
41	29 32 40	sylancr	$⊢ ((−∞ \in u \land u \subseteq A) \land (y \in ℝ^{} \land u = [−∞, y))) \to (−∞ \in [−∞, y) \leftrightarrow (−∞ \in ℝ^{} \land −∞ \leq −∞ \land −∞ < y))$
42	39 41	mpbid	$⊢ ((−∞ \in u \land u \subseteq A) \land (y \in ℝ^{} \land u = [−∞, y))) \to (−∞ \in ℝ^{} \land −∞ \leq −∞ \land −∞ < y)$
43	42	simp3d	$⊢ ((−∞ \in u \land u \subseteq A) \land (y \in ℝ^{*} \land u = [−∞, y))) \to −∞ < y$
44		breq2	$⊢ 0 = if (0 \leq y, 0, y) \to (−∞ < 0 \leftrightarrow −∞ < if (0 \leq y, 0, y))$
45		breq2	$⊢ y = if (0 \leq y, 0, y) \to (−∞ < y \leftrightarrow −∞ < if (0 \leq y, 0, y))$
46	44 45	ifboth	$⊢ (−∞ < 0 \land −∞ < y) \to −∞ < if (0 \leq y, 0, y)$
47	36 43 46	sylancr	$⊢ ((−∞ \in u \land u \subseteq A) \land (y \in ℝ^{*} \land u = [−∞, y))) \to −∞ < if (0 \leq y, 0, y)$
48	31	a1i	$⊢ ((−∞ \in u \land u \subseteq A) \land (y \in ℝ^{} \land u = [−∞, y))) \to 0 \in ℝ^{}$
49		xrmin1	$⊢ (0 \in ℝ^{} \land y \in ℝ^{}) \to if (0 \leq y, 0, y) \leq 0$
50	31 32 49	sylancr	$⊢ ((−∞ \in u \land u \subseteq A) \land (y \in ℝ^{*} \land u = [−∞, y))) \to if (0 \leq y, 0, y) \leq 0$
51		0re	$⊢ 0 \in ℝ$
52		ltpnf	$⊢ 0 \in ℝ \to 0 < +∞$
53	51 52	mp1i	$⊢ ((−∞ \in u \land u \subseteq A) \land (y \in ℝ^{*} \land u = [−∞, y))) \to 0 < +∞$
54	34 48 35 50 53	xrlelttrd	$⊢ ((−∞ \in u \land u \subseteq A) \land (y \in ℝ^{*} \land u = [−∞, y))) \to if (0 \leq y, 0, y) < +∞$
55		xrre2	$⊢ ((−∞ \in ℝ^{} \land if (0 \leq y, 0, y) \in ℝ^{} \land +∞ \in ℝ^{*}) \land (−∞ < if (0 \leq y, 0, y) \land if (0 \leq y, 0, y) < +∞)) \to if (0 \leq y, 0, y) \in ℝ$
56	30 34 35 47 54 55	syl32anc	$⊢ ((−∞ \in u \land u \subseteq A) \land (y \in ℝ^{*} \land u = [−∞, y))) \to if (0 \leq y, 0, y) \in ℝ$
57		xrmin2	$⊢ (0 \in ℝ^{} \land y \in ℝ^{}) \to if (0 \leq y, 0, y) \leq y$
58	31 32 57	sylancr	$⊢ ((−∞ \in u \land u \subseteq A) \land (y \in ℝ^{*} \land u = [−∞, y))) \to if (0 \leq y, 0, y) \leq y$
59		df-ico	$⊢ [.) = (a \in ℝ^{}, b \in ℝ^{} ⟼ \{c \in ℝ^{*} \| (a \leq c \land c < b)\})$
60		xrltletr	$⊢ (x \in ℝ^{} \land if (0 \leq y, 0, y) \in ℝ^{} \land y \in ℝ^{*}) \to ((x < if (0 \leq y, 0, y) \land if (0 \leq y, 0, y) \leq y) \to x < y)$
61	59 59 60	ixxss2	$⊢ (y \in ℝ^{*} \land if (0 \leq y, 0, y) \leq y) \to [−∞, if (0 \leq y, 0, y)) \subseteq [−∞, y)$
62	32 58 61	syl2anc	$⊢ ((−∞ \in u \land u \subseteq A) \land (y \in ℝ^{*} \land u = [−∞, y))) \to [−∞, if (0 \leq y, 0, y)) \subseteq [−∞, y)$
63		simplr	$⊢ ((−∞ \in u \land u \subseteq A) \land (y \in ℝ^{*} \land u = [−∞, y))) \to u \subseteq A$
64	38 63	eqsstrrd	$⊢ ((−∞ \in u \land u \subseteq A) \land (y \in ℝ^{*} \land u = [−∞, y))) \to [−∞, y) \subseteq A$
65	62 64	sstrd	$⊢ ((−∞ \in u \land u \subseteq A) \land (y \in ℝ^{*} \land u = [−∞, y))) \to [−∞, if (0 \leq y, 0, y)) \subseteq A$
66		oveq2	$⊢ x = if (0 \leq y, 0, y) \to [−∞, x) = [−∞, if (0 \leq y, 0, y))$
67	66	sseq1d	$⊢ x = if (0 \leq y, 0, y) \to ([−∞, x) \subseteq A \leftrightarrow [−∞, if (0 \leq y, 0, y)) \subseteq A)$
68	67	rspcev	$⊢ (if (0 \leq y, 0, y) \in ℝ \land [−∞, if (0 \leq y, 0, y)) \subseteq A) \to \exists x \in ℝ [−∞, x) \subseteq A$
69	56 65 68	syl2anc	$⊢ ((−∞ \in u \land u \subseteq A) \land (y \in ℝ^{*} \land u = [−∞, y))) \to \exists x \in ℝ [−∞, x) \subseteq A$
70	69	rexlimdvaa	$⊢ (−∞ \in u \land u \subseteq A) \to (\exists y \in ℝ^{*} u = [−∞, y) \to \exists x \in ℝ [−∞, x) \subseteq A)$
71	70	com12	$⊢ \exists y \in ℝ^{*} u = [−∞, y) \to ((−∞ \in u \land u \subseteq A) \to \exists x \in ℝ [−∞, x) \subseteq A)$
72	28 71	sylbi	$⊢ u \in ran (y \in ℝ^{*} ⟼ [−∞, y)) \to ((−∞ \in u \land u \subseteq A) \to \exists x \in ℝ [−∞, x) \subseteq A)$
73	25 72	jaoi	$⊢ (u \in ran (y \in ℝ^{} ⟼ (y, +∞]) \lor u \in ran (y \in ℝ^{} ⟼ [−∞, y))) \to ((−∞ \in u \land u \subseteq A) \to \exists x \in ℝ [−∞, x) \subseteq A)$
74	8 73	sylbi	$⊢ u \in (ran (y \in ℝ^{} ⟼ (y, +∞]) \cup ran (y \in ℝ^{} ⟼ [−∞, y))) \to ((−∞ \in u \land u \subseteq A) \to \exists x \in ℝ [−∞, x) \subseteq A)$
75		mnfnre	$⊢ −∞ \notin ℝ$
76	75	neli	$⊢ \neg −∞ \in ℝ$
77		elssuni	$⊢ u \in ran (.) \to u \subseteq ⋃ ran (.)$
78		unirnioo	$⊢ ℝ = ⋃ ran (.)$
79	77 78	sseqtrrdi	$⊢ u \in ran (.) \to u \subseteq ℝ$
80	79	sseld	$⊢ u \in ran (.) \to (−∞ \in u \to −∞ \in ℝ)$
81	76 80	mtoi	$⊢ u \in ran (.) \to \neg −∞ \in u$
82	81	pm2.21d	$⊢ u \in ran (.) \to (−∞ \in u \to \exists x \in ℝ [−∞, x) \subseteq A)$
83	82	adantrd	$⊢ u \in ran (.) \to ((−∞ \in u \land u \subseteq A) \to \exists x \in ℝ [−∞, x) \subseteq A)$
84	74 83	jaoi	$⊢ (u \in (ran (y \in ℝ^{} ⟼ (y, +∞]) \cup ran (y \in ℝ^{} ⟼ [−∞, y))) \lor u \in ran (.)) \to ((−∞ \in u \land u \subseteq A) \to \exists x \in ℝ [−∞, x) \subseteq A)$
85	7 84	sylbi	$⊢ u \in ((ran (y \in ℝ^{} ⟼ (y, +∞]) \cup ran (y \in ℝ^{} ⟼ [−∞, y))) \cup ran (.)) \to ((−∞ \in u \land u \subseteq A) \to \exists x \in ℝ [−∞, x) \subseteq A)$
86	85	rexlimiv	$⊢ \exists u \in ((ran (y \in ℝ^{} ⟼ (y, +∞]) \cup ran (y \in ℝ^{} ⟼ [−∞, y))) \cup ran (.)) (−∞ \in u \land u \subseteq A) \to \exists x \in ℝ [−∞, x) \subseteq A$
87	6 86	syl	$⊢ (A \in topGen ((ran (y \in ℝ^{} ⟼ (y, +∞]) \cup ran (y \in ℝ^{} ⟼ [−∞, y))) \cup ran (.)) \land −∞ \in A) \to \exists x \in ℝ [−∞, x) \subseteq A$
88	5 87	sylanb	$⊢ (A \in ordTop (\leq) \land −∞ \in A) \to \exists x \in ℝ [−∞, x) \subseteq A$

Metamath Proof Explorer

Theorem mnfnei

Proof