iocpnfordt

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	iocpnfordt	$⊢ (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		ssun1	$⊢ ran (x \in ℝ^{} ⟼ (x, +∞]) \subseteq ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{*} ⟼ [−∞, x))$
14		eqid	$⊢ (A, +∞] = (A, +∞]$
15		oveq1	$⊢ 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	adantr	$⊢ (A \in ℝ^{} \land +∞ \in ℝ^{}) \to (A, +∞] \in ordTop (\leq)$
26		df-ioc	$⊢ (.] = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x < z \land z \leq y)\})$
27	26	ixxf	$⊢ (.] : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$
28	27	fdmi	$⊢ dom (.] = ℝ^{} \times ℝ^{}$
29	28	ndmov	$⊢ \neg (A \in ℝ^{} \land +∞ \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 (A \in ℝ^{} \land +∞ \in ℝ^{}) \to (A, +∞] \in ordTop (\leq)$
33	25 32	pm2.61i	$⊢ (A, +∞] \in ordTop (\leq)$

Metamath Proof Explorer

Theorem iocpnfordt

Proof