iocopn

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

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

Proof

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

Metamath Proof Explorer

Theorem iocopn

Proof