icoopn

Description: A left-closed right-open interval is an open set of the standard topology restricted to an interval that contains the original interval and has the same lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	icoopn.a	$⊢ φ \to A \in ℝ$
	icoopn.c	$⊢ φ \to C \in ℝ^{*}$
	icoopn.b	$⊢ φ \to B \in ℝ^{*}$
	icoopn.k	$⊢ K = topGen (ran (.))$
	icoopn.j	$⊢ J = K ↾_{𝑡} [A, B)$
	icoopn.cleb	$⊢ φ \to C \leq B$
Assertion	icoopn	$⊢ φ \to [A, C) \in J$

Proof

Step	Hyp	Ref	Expression
1		icoopn.a	$⊢ φ \to A \in ℝ$
2		icoopn.c	$⊢ φ \to C \in ℝ^{*}$
3		icoopn.b	$⊢ φ \to B \in ℝ^{*}$
4		icoopn.k	$⊢ K = topGen (ran (.))$
5		icoopn.j	$⊢ J = K ↾_{𝑡} [A, B)$
6		icoopn.cleb	$⊢ φ \to C \leq B$
7		retop	$⊢ topGen (ran (.)) \in Top$
8	4 7	eqeltri	$⊢ K \in Top$
9	8	a1i	$⊢ φ \to K \in Top$
10		ovexd	$⊢ φ \to [A, B) \in V$
11		iooretop	$⊢ (−∞, C) \in topGen (ran (.))$
12	11 4	eleqtrri	$⊢ (−∞, C) \in K$
13	12	a1i	$⊢ φ \to (−∞, C) \in K$
14		elrestr	$⊢ (K \in Top \land [A, B) \in V \land (−∞, C) \in K) \to (−∞, C) \cap [A, B) \in (K ↾_{𝑡} [A, B))$
15	9 10 13 14	syl3anc	$⊢ φ \to (−∞, C) \cap [A, B) \in (K ↾_{𝑡} [A, B))$
16	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
17	16	adantr	$⊢ (φ \land x \in ((−∞, C) \cap [A, B))) \to A \in ℝ^{*}$
18	2	adantr	$⊢ (φ \land x \in ((−∞, C) \cap [A, B))) \to C \in ℝ^{*}$
19		elinel1	$⊢ x \in ((−∞, C) \cap [A, B)) \to x \in (−∞, C)$
20		elioore	$⊢ x \in (−∞, C) \to x \in ℝ$
21	19 20	syl	$⊢ x \in ((−∞, C) \cap [A, B)) \to x \in ℝ$
22	21	rexrd	$⊢ x \in ((−∞, C) \cap [A, B)) \to x \in ℝ^{*}$
23	22	adantl	$⊢ (φ \land x \in ((−∞, C) \cap [A, B))) \to x \in ℝ^{*}$
24	3	adantr	$⊢ (φ \land x \in ((−∞, C) \cap [A, B))) \to B \in ℝ^{*}$
25		elinel2	$⊢ x \in ((−∞, C) \cap [A, B)) \to x \in [A, B)$
26	25	adantl	$⊢ (φ \land x \in ((−∞, C) \cap [A, B))) \to x \in [A, B)$
27		icogelb	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land x \in [A, B)) \to A \leq x$
28	17 24 26 27	syl3anc	$⊢ (φ \land x \in ((−∞, C) \cap [A, B))) \to A \leq x$
29		mnfxr	$⊢ −∞ \in ℝ^{*}$
30	29	a1i	$⊢ (φ \land x \in ((−∞, C) \cap [A, B))) \to −∞ \in ℝ^{*}$
31	19	adantl	$⊢ (φ \land x \in ((−∞, C) \cap [A, B))) \to x \in (−∞, C)$
32		iooltub	$⊢ (−∞ \in ℝ^{} \land C \in ℝ^{} \land x \in (−∞, C)) \to x < C$
33	30 18 31 32	syl3anc	$⊢ (φ \land x \in ((−∞, C) \cap [A, B))) \to x < C$
34	17 18 23 28 33	elicod	$⊢ (φ \land x \in ((−∞, C) \cap [A, B))) \to x \in [A, C)$
35	29	a1i	$⊢ (φ \land x \in [A, C)) \to −∞ \in ℝ^{*}$
36	2	adantr	$⊢ (φ \land x \in [A, C)) \to C \in ℝ^{*}$
37		icossre	$⊢ (A \in ℝ \land C \in ℝ^{*}) \to [A, C) \subseteq ℝ$
38	1 2 37	syl2anc	$⊢ φ \to [A, C) \subseteq ℝ$
39	38	sselda	$⊢ (φ \land x \in [A, C)) \to x \in ℝ$
40	39	mnfltd	$⊢ (φ \land x \in [A, C)) \to −∞ < x$
41	16	adantr	$⊢ (φ \land x \in [A, C)) \to A \in ℝ^{*}$
42		simpr	$⊢ (φ \land x \in [A, C)) \to x \in [A, C)$
43		icoltub	$⊢ (A \in ℝ^{} \land C \in ℝ^{} \land x \in [A, C)) \to x < C$
44	41 36 42 43	syl3anc	$⊢ (φ \land x \in [A, C)) \to x < C$
45	35 36 39 40 44	eliood	$⊢ (φ \land x \in [A, C)) \to x \in (−∞, C)$
46	3	adantr	$⊢ (φ \land x \in [A, C)) \to B \in ℝ^{*}$
47	39	rexrd	$⊢ (φ \land x \in [A, C)) \to x \in ℝ^{*}$
48		icogelb	$⊢ (A \in ℝ^{} \land C \in ℝ^{} \land x \in [A, C)) \to A \leq x$
49	41 36 42 48	syl3anc	$⊢ (φ \land x \in [A, C)) \to A \leq x$
50	6	adantr	$⊢ (φ \land x \in [A, C)) \to C \leq B$
51	47 36 46 44 50	xrltletrd	$⊢ (φ \land x \in [A, C)) \to x < B$
52	41 46 47 49 51	elicod	$⊢ (φ \land x \in [A, C)) \to x \in [A, B)$
53	45 52	elind	$⊢ (φ \land x \in [A, C)) \to x \in ((−∞, C) \cap [A, B))$
54	34 53	impbida	$⊢ φ \to (x \in ((−∞, C) \cap [A, B)) \leftrightarrow x \in [A, C))$
55	54	eqrdv	$⊢ φ \to (−∞, C) \cap [A, B) = [A, C)$
56	5	eqcomi	$⊢ K ↾_{𝑡} [A, B) = J$
57	56	a1i	$⊢ φ \to K ↾_{𝑡} [A, B) = J$
58	15 55 57	3eltr3d	$⊢ φ \to [A, C) \in J$

Metamath Proof Explorer

Theorem icoopn

Proof