icomnfordt

Description: An unbounded above open interval is open in the order topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015)

		Ref	Expression
	Assertion	icomnfordt	$⊢ [−∞, A) \in ordTop (\leq)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ ran (x \in ℝ^{} ⟼ (x, +∞]) = ran (x \in ℝ^{} ⟼ (x, +∞])$
2		eqid	$⊢ ran (x \in ℝ^{} ⟼ [−∞, x)) = ran (x \in ℝ^{} ⟼ [−∞, x))$
3		eqid	$⊢ ran (.) = ran (.)$
4	1 2 3	leordtval	$⊢ ordTop (\leq) = topGen ((ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.))$
5		letop	$⊢ ordTop (\leq) \in Top$
6	4 5	eqeltrri	$⊢ topGen ((ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.)) \in Top$
7		tgclb	$⊢ (ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.) \in TopBases \leftrightarrow topGen ((ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.)) \in Top$
8	6 7	mpbir	$⊢ (ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.) \in TopBases$
9		bastg	$⊢ (ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.) \in TopBases \to (ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.) \subseteq topGen ((ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.))$
10	8 9	ax-mp	$⊢ (ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.) \subseteq topGen ((ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.))$
11	10 4	sseqtrri	$⊢ (ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.) \subseteq ordTop (\leq)$
12		ssun1	$⊢ ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x)) \subseteq (ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.)$
13		ssun2	$⊢ ran (x \in ℝ^{} ⟼ [−∞, x)) \subseteq ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{*} ⟼ [−∞, x))$
14		eqid	$⊢ [−∞, A) = [−∞, A)$
15		oveq2	$⊢ x = A \to [−∞, x) = [−∞, A)$
16	15	rspceeqv	$⊢ (A \in ℝ^{} \land [−∞, A) = [−∞, A)) \to \exists x \in ℝ^{} [−∞, A) = [−∞, x)$
17	14 16	mpan2	$⊢ A \in ℝ^{} \to \exists x \in ℝ^{} [−∞, A) = [−∞, x)$
18		eqid	$⊢ (x \in ℝ^{} ⟼ [−∞, x)) = (x \in ℝ^{} ⟼ [−∞, x))$
19		ovex	$⊢ [−∞, x) \in V$
20	18 19	elrnmpti	$⊢ [−∞, A) \in ran (x \in ℝ^{} ⟼ [−∞, x)) \leftrightarrow \exists x \in ℝ^{} [−∞, A) = [−∞, x)$
21	17 20	sylibr	$⊢ A \in ℝ^{} \to [−∞, A) \in ran (x \in ℝ^{} ⟼ [−∞, x))$
22	13 21	sseldi	$⊢ A \in ℝ^{} \to [−∞, A) \in (ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{*} ⟼ [−∞, x)))$
23	12 22	sseldi	$⊢ A \in ℝ^{} \to [−∞, A) \in ((ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{*} ⟼ [−∞, x))) \cup ran (.))$
24	11 23	sseldi	$⊢ A \in ℝ^{*} \to [−∞, A) \in ordTop (\leq)$
25	24	adantl	$⊢ (−∞ \in ℝ^{} \land A \in ℝ^{}) \to [−∞, A) \in ordTop (\leq)$
26		df-ico	$⊢ [.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x \leq z \land z < y)\})$
27	26	ixxf	$⊢ [.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$
28	27	fdmi	$⊢ dom [.) = ℝ^{} \times ℝ^{}$
29	28	ndmov	$⊢ \neg (−∞ \in ℝ^{} \land A \in ℝ^{}) \to [−∞, A) = \emptyset$
30		0opn	$⊢ ordTop (\leq) \in Top \to \emptyset \in ordTop (\leq)$
31	5 30	ax-mp	$⊢ \emptyset \in ordTop (\leq)$
32	29 31	eqeltrdi	$⊢ \neg (−∞ \in ℝ^{} \land A \in ℝ^{}) \to [−∞, A) \in ordTop (\leq)$
33	25 32	pm2.61i	$⊢ [−∞, A) \in ordTop (\leq)$

Metamath Proof Explorer

Theorem icomnfordt

Proof