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	⊢ ( 𝜑 → 𝐴 ∈ ℝ^* )
	iocopn.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ^* )
	iocopn.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	iocopn.k	⊢ 𝐾 = ( topGen ‘ ran (,) )
	iocopn.j	⊢ 𝐽 = ( 𝐾 ↾_t ( 𝐴 (,] 𝐵 ) )
	iocopn.alec	⊢ ( 𝜑 → 𝐴 ≤ 𝐶 )
	iocopn.6	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
Assertion	iocopn	⊢ ( 𝜑 → ( 𝐶 (,] 𝐵 ) ∈ 𝐽 )

Proof

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

Metamath Proof Explorer

Theorem iocopn

Proof