icopnfcld

Description: Right-unbounded closed intervals are closed sets of the standard topology on RR . (Contributed by Mario Carneiro, 17-Feb-2015)

		Ref	Expression
	Assertion	icopnfcld	$⊢ A \in ℝ \to [A, +∞) \in Clsd (topGen (ran (.)))$

Proof

Step	Hyp	Ref	Expression
1		mnfxr	$⊢ −∞ \in ℝ^{*}$
2	1	a1i	$⊢ A \in ℝ \to −∞ \in ℝ^{*}$
3		rexr	$⊢ A \in ℝ \to A \in ℝ^{*}$
4		pnfxr	$⊢ +∞ \in ℝ^{*}$
5	4	a1i	$⊢ A \in ℝ \to +∞ \in ℝ^{*}$
6		mnflt	$⊢ A \in ℝ \to −∞ < A$
7		ltpnf	$⊢ A \in ℝ \to A < +∞$
8		df-ioo	$⊢ (.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x < z \land z < y)\})$
9		df-ico	$⊢ [.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x \leq z \land z < y)\})$
10		xrlenlt	$⊢ (A \in ℝ^{} \land w \in ℝ^{}) \to (A \leq w \leftrightarrow \neg w < A)$
11		xrlttr	$⊢ (w \in ℝ^{} \land A \in ℝ^{} \land +∞ \in ℝ^{*}) \to ((w < A \land A < +∞) \to w < +∞)$
12		xrltletr	$⊢ (−∞ \in ℝ^{} \land A \in ℝ^{} \land w \in ℝ^{*}) \to ((−∞ < A \land A \leq w) \to −∞ < w)$
13	8 9 10 8 11 12	ixxun	$⊢ ((−∞ \in ℝ^{} \land A \in ℝ^{} \land +∞ \in ℝ^{*}) \land (−∞ < A \land A < +∞)) \to (−∞, A) \cup [A, +∞) = (−∞, +∞)$
14	2 3 5 6 7 13	syl32anc	$⊢ A \in ℝ \to (−∞, A) \cup [A, +∞) = (−∞, +∞)$
15		ioomax	$⊢ (−∞, +∞) = ℝ$
16	14 15	eqtrdi	$⊢ A \in ℝ \to (−∞, A) \cup [A, +∞) = ℝ$
17		ioossre	$⊢ (−∞, A) \subseteq ℝ$
18	8 9 10	ixxdisj	$⊢ (−∞ \in ℝ^{} \land A \in ℝ^{} \land +∞ \in ℝ^{*}) \to (−∞, A) \cap [A, +∞) = \emptyset$
19	1 3 5 18	mp3an2i	$⊢ A \in ℝ \to (−∞, A) \cap [A, +∞) = \emptyset$
20		uneqdifeq	$⊢ ((−∞, A) \subseteq ℝ \land (−∞, A) \cap [A, +∞) = \emptyset) \to ((−∞, A) \cup [A, +∞) = ℝ \leftrightarrow ℝ ∖ (−∞, A) = [A, +∞))$
21	17 19 20	sylancr	$⊢ A \in ℝ \to ((−∞, A) \cup [A, +∞) = ℝ \leftrightarrow ℝ ∖ (−∞, A) = [A, +∞))$
22	16 21	mpbid	$⊢ A \in ℝ \to ℝ ∖ (−∞, A) = [A, +∞)$
23		retop	$⊢ topGen (ran (.)) \in Top$
24		iooretop	$⊢ (−∞, A) \in topGen (ran (.))$
25		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
26	25	opncld	$⊢ (topGen (ran (.)) \in Top \land (−∞, A) \in topGen (ran (.))) \to ℝ ∖ (−∞, A) \in Clsd (topGen (ran (.)))$
27	23 24 26	mp2an	$⊢ ℝ ∖ (−∞, A) \in Clsd (topGen (ran (.)))$
28	22 27	eqeltrrdi	$⊢ A \in ℝ \to [A, +∞) \in Clsd (topGen (ran (.)))$

Metamath Proof Explorer

Theorem icopnfcld

Proof