Theorem 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	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	icoopn.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
	icoopn.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
	icoopn.k	⊢ 𝐾 = ( topGen ‘ ran (,) )
	icoopn.j	⊢ 𝐽 = ( 𝐾 ↾t ( 𝐴 [,) 𝐵 ) )
	icoopn.cleb	⊢ ( 𝜑 → 𝐶 ≤ 𝐵 )
Assertion	icoopn	⊢ ( 𝜑 → ( 𝐴 [,) 𝐶 ) ∈ 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		icoopn.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		icoopn.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
3		icoopn.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
4		icoopn.k	⊢ 𝐾 = ( topGen ‘ ran (,) )
5		icoopn.j	⊢ 𝐽 = ( 𝐾 ↾t ( 𝐴 [,) 𝐵 ) )
6		icoopn.cleb	⊢ ( 𝜑 → 𝐶 ≤ 𝐵 )
7		retop	⊢ ( topGen ‘ ran (,) ) ∈ Top
8	4 7	eqeltri	⊢ 𝐾 ∈ Top
9	8	a1i	⊢ ( 𝜑 → 𝐾 ∈ Top )
10		ovexd	⊢ ( 𝜑 → ( 𝐴 [,) 𝐵 ) ∈ V )
11		iooretop	⊢ ( -∞ (,) 𝐶 ) ∈ ( topGen ‘ ran (,) )
12	11 4	eleqtrri	⊢ ( -∞ (,) 𝐶 ) ∈ 𝐾
13	12	a1i	⊢ ( 𝜑 → ( -∞ (,) 𝐶 ) ∈ 𝐾 )
14		elrestr	⊢ ( ( 𝐾 ∈ Top ∧ ( 𝐴 [,) 𝐵 ) ∈ V ∧ ( -∞ (,) 𝐶 ) ∈ 𝐾 ) → ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) ∈ ( 𝐾 ↾t ( 𝐴 [,) 𝐵 ) ) )
15	9 10 13 14	syl3anc	⊢ ( 𝜑 → ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) ∈ ( 𝐾 ↾t ( 𝐴 [,) 𝐵 ) ) )
16	1	rexrd	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) ) → 𝐴 ∈ ℝ* )
18	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) ) → 𝐶 ∈ ℝ* )
19		elinel1	⊢ ( 𝑥 ∈ ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) → 𝑥 ∈ ( -∞ (,) 𝐶 ) )
20		elioore	⊢ ( 𝑥 ∈ ( -∞ (,) 𝐶 ) → 𝑥 ∈ ℝ )
21	19 20	syl	⊢ ( 𝑥 ∈ ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) → 𝑥 ∈ ℝ )
22	21	rexrd	⊢ ( 𝑥 ∈ ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) → 𝑥 ∈ ℝ* )
23	22	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) ) → 𝑥 ∈ ℝ* )
24	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) ) → 𝐵 ∈ ℝ* )
25		elinel2	⊢ ( 𝑥 ∈ ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) → 𝑥 ∈ ( 𝐴 [,) 𝐵 ) )
26	25	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) ) → 𝑥 ∈ ( 𝐴 [,) 𝐵 ) )
27		icogelb	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝐴 ≤ 𝑥 )
28	17 24 26 27	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) ) → 𝐴 ≤ 𝑥 )
29		mnfxr	⊢ -∞ ∈ ℝ*
30	29	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) ) → -∞ ∈ ℝ* )
31	19	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) ) → 𝑥 ∈ ( -∞ (,) 𝐶 ) )
32		iooltub	⊢ ( ( -∞ ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑥 ∈ ( -∞ (,) 𝐶 ) ) → 𝑥 < 𝐶 )
33	30 18 31 32	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) ) → 𝑥 < 𝐶 )
34	17 18 23 28 33	elicod	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) ) → 𝑥 ∈ ( 𝐴 [,) 𝐶 ) )
35	29	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → -∞ ∈ ℝ* )
36	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → 𝐶 ∈ ℝ* )
37		icossre	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ* ) → ( 𝐴 [,) 𝐶 ) ⊆ ℝ )
38	1 2 37	syl2anc	⊢ ( 𝜑 → ( 𝐴 [,) 𝐶 ) ⊆ ℝ )
39	38	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → 𝑥 ∈ ℝ )
40	39	mnfltd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → -∞ < 𝑥 )
41	16	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → 𝐴 ∈ ℝ* )
42		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → 𝑥 ∈ ( 𝐴 [,) 𝐶 ) )
43		icoltub	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → 𝑥 < 𝐶 )
44	41 36 42 43	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → 𝑥 < 𝐶 )
45	35 36 39 40 44	eliood	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → 𝑥 ∈ ( -∞ (,) 𝐶 ) )
46	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → 𝐵 ∈ ℝ* )
47	39	rexrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → 𝑥 ∈ ℝ* )
48		icogelb	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → 𝐴 ≤ 𝑥 )
49	41 36 42 48	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → 𝐴 ≤ 𝑥 )
50	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → 𝐶 ≤ 𝐵 )
51	47 36 46 44 50	xrltletrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → 𝑥 < 𝐵 )
52	41 46 47 49 51	elicod	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → 𝑥 ∈ ( 𝐴 [,) 𝐵 ) )
53	45 52	elind	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → 𝑥 ∈ ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) )
54	34 53	impbida	⊢ ( 𝜑 → ( 𝑥 ∈ ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) ↔ 𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) )
55	54	eqrdv	⊢ ( 𝜑 → ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) = ( 𝐴 [,) 𝐶 ) )
56	5	eqcomi	⊢ ( 𝐾 ↾t ( 𝐴 [,) 𝐵 ) ) = 𝐽
57	56	a1i	⊢ ( 𝜑 → ( 𝐾 ↾t ( 𝐴 [,) 𝐵 ) ) = 𝐽 )
58	15 55 57	3eltr3d	⊢ ( 𝜑 → ( 𝐴 [,) 𝐶 ) ∈ 𝐽 )