icccld

Description: Closed intervals are closed sets of the standard topology on RR . (Contributed by FL, 14-Sep-2007)

		Ref	Expression
	Assertion	icccld	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \in Clsd (topGen (ran (.)))$

Step	Hyp	Ref	Expression
1		difreicc	$⊢ (A \in ℝ \land B \in ℝ) \to ℝ ∖ [A, B] = (−∞, A) \cup (B, +∞)$
2		retop	$⊢ topGen (ran (.)) \in Top$
3		iooretop	$⊢ (−∞, A) \in topGen (ran (.))$
4		iooretop	$⊢ (B, +∞) \in topGen (ran (.))$
5		unopn	$⊢ (topGen (ran (.)) \in Top \land (−∞, A) \in topGen (ran (.)) \land (B, +∞) \in topGen (ran (.))) \to (−∞, A) \cup (B, +∞) \in topGen (ran (.))$
6	2 3 4 5	mp3an	$⊢ (−∞, A) \cup (B, +∞) \in topGen (ran (.))$
7	1 6	eqeltrdi	$⊢ (A \in ℝ \land B \in ℝ) \to ℝ ∖ [A, B] \in topGen (ran (.))$
8		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
9		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
10	9	iscld2	$⊢ (topGen (ran (.)) \in Top \land [A, B] \subseteq ℝ) \to ([A, B] \in Clsd (topGen (ran (.))) \leftrightarrow ℝ ∖ [A, B] \in topGen (ran (.)))$
11	2 8 10	sylancr	$⊢ (A \in ℝ \land B \in ℝ) \to ([A, B] \in Clsd (topGen (ran (.))) \leftrightarrow ℝ ∖ [A, B] \in topGen (ran (.)))$
12	7 11	mpbird	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \in Clsd (topGen (ran (.)))$

Metamath Proof Explorer