io1ii

Description: ( A (,] 1 ) is open in II . (Contributed by Zhi Wang, 9-Sep-2024)

		Ref	Expression
	Assertion	io1ii	$⊢ 0 \leq A \to (A, 1] \in II$

Proof

Step	Hyp	Ref	Expression
1		0xr	$⊢ 0 \in ℝ^{*}$
2		lerelxr	$⊢ \leq \subseteq ℝ^{} \times ℝ^{}$
3	2	brel	$⊢ 0 \leq A \to (0 \in ℝ^{} \land A \in ℝ^{})$
4	3	simprd	$⊢ 0 \leq A \to A \in ℝ^{*}$
5		rexr	$⊢ x \in ℝ \to x \in ℝ^{*}$
6		xrlelttr	$⊢ (0 \in ℝ^{} \land A \in ℝ^{} \land x \in ℝ^{*}) \to ((0 \leq A \land A < x) \to 0 < x)$
7		xrltle	$⊢ (0 \in ℝ^{} \land x \in ℝ^{}) \to (0 < x \to 0 \leq x)$
8	7	3adant2	$⊢ (0 \in ℝ^{} \land A \in ℝ^{} \land x \in ℝ^{*}) \to (0 < x \to 0 \leq x)$
9	6 8	syld	$⊢ (0 \in ℝ^{} \land A \in ℝ^{} \land x \in ℝ^{*}) \to ((0 \leq A \land A < x) \to 0 \leq x)$
10	1 4 5 9	mp3an3an	$⊢ (0 \leq A \land x \in ℝ) \to ((0 \leq A \land A < x) \to 0 \leq x)$
11	10	imp	$⊢ ((0 \leq A \land x \in ℝ) \land (0 \leq A \land A < x)) \to 0 \leq x$
12	11	3impdi	$⊢ (0 \leq A \land x \in ℝ \land A < x) \to 0 \leq x$
13	12	3expib	$⊢ 0 \leq A \to ((x \in ℝ \land A < x) \to 0 \leq x)$
14	13	pm4.71d	$⊢ 0 \leq A \to ((x \in ℝ \land A < x) \leftrightarrow ((x \in ℝ \land A < x) \land 0 \leq x))$
15	14	anbi1d	$⊢ 0 \leq A \to (((x \in ℝ \land A < x) \land x \leq 1) \leftrightarrow (((x \in ℝ \land A < x) \land 0 \leq x) \land x \leq 1))$
16		df-3an	$⊢ (x \in ℝ \land A < x \land x \leq 1) \leftrightarrow ((x \in ℝ \land A < x) \land x \leq 1)$
17		3anass	$⊢ (x \in ℝ \land 0 \leq x \land x \leq 1) \leftrightarrow (x \in ℝ \land (0 \leq x \land x \leq 1))$
18	17	anbi2i	$⊢ ((x \in ℝ \land A < x) \land (x \in ℝ \land 0 \leq x \land x \leq 1)) \leftrightarrow ((x \in ℝ \land A < x) \land (x \in ℝ \land (0 \leq x \land x \leq 1)))$
19		anandi	$⊢ (x \in ℝ \land (A < x \land (0 \leq x \land x \leq 1))) \leftrightarrow ((x \in ℝ \land A < x) \land (x \in ℝ \land (0 \leq x \land x \leq 1)))$
20		anass	$⊢ (((x \in ℝ \land A < x) \land 0 \leq x) \land x \leq 1) \leftrightarrow ((x \in ℝ \land A < x) \land (0 \leq x \land x \leq 1))$
21		anass	$⊢ ((x \in ℝ \land A < x) \land (0 \leq x \land x \leq 1)) \leftrightarrow (x \in ℝ \land (A < x \land (0 \leq x \land x \leq 1)))$
22	20 21	bitr2i	$⊢ (x \in ℝ \land (A < x \land (0 \leq x \land x \leq 1))) \leftrightarrow (((x \in ℝ \land A < x) \land 0 \leq x) \land x \leq 1)$
23	18 19 22	3bitr2i	$⊢ ((x \in ℝ \land A < x) \land (x \in ℝ \land 0 \leq x \land x \leq 1)) \leftrightarrow (((x \in ℝ \land A < x) \land 0 \leq x) \land x \leq 1)$
24	15 16 23	3bitr4g	$⊢ 0 \leq A \to ((x \in ℝ \land A < x \land x \leq 1) \leftrightarrow ((x \in ℝ \land A < x) \land (x \in ℝ \land 0 \leq x \land x \leq 1)))$
25		1re	$⊢ 1 \in ℝ$
26		elioc2	$⊢ (A \in ℝ^{*} \land 1 \in ℝ) \to (x \in (A, 1] \leftrightarrow (x \in ℝ \land A < x \land x \leq 1))$
27	4 25 26	sylancl	$⊢ 0 \leq A \to (x \in (A, 1] \leftrightarrow (x \in ℝ \land A < x \land x \leq 1))$
28		elin	$⊢ x \in ((A, +∞) \cap [0, 1]) \leftrightarrow (x \in (A, +∞) \land x \in [0, 1])$
29		elicc01	$⊢ x \in [0, 1] \leftrightarrow (x \in ℝ \land 0 \leq x \land x \leq 1)$
30	29	anbi2i	$⊢ (x \in (A, +∞) \land x \in [0, 1]) \leftrightarrow (x \in (A, +∞) \land (x \in ℝ \land 0 \leq x \land x \leq 1))$
31	28 30	bitri	$⊢ x \in ((A, +∞) \cap [0, 1]) \leftrightarrow (x \in (A, +∞) \land (x \in ℝ \land 0 \leq x \land x \leq 1))$
32		elioopnf	$⊢ A \in ℝ^{*} \to (x \in (A, +∞) \leftrightarrow (x \in ℝ \land A < x))$
33	4 32	syl	$⊢ 0 \leq A \to (x \in (A, +∞) \leftrightarrow (x \in ℝ \land A < x))$
34	33	anbi1d	$⊢ 0 \leq A \to ((x \in (A, +∞) \land (x \in ℝ \land 0 \leq x \land x \leq 1)) \leftrightarrow ((x \in ℝ \land A < x) \land (x \in ℝ \land 0 \leq x \land x \leq 1)))$
35	31 34	syl5bb	$⊢ 0 \leq A \to (x \in ((A, +∞) \cap [0, 1]) \leftrightarrow ((x \in ℝ \land A < x) \land (x \in ℝ \land 0 \leq x \land x \leq 1)))$
36	24 27 35	3bitr4rd	$⊢ 0 \leq A \to (x \in ((A, +∞) \cap [0, 1]) \leftrightarrow x \in (A, 1])$
37	36	eqrdv	$⊢ 0 \leq A \to (A, +∞) \cap [0, 1] = (A, 1]$
38		fvex	$⊢ topGen (ran (.)) \in V$
39		ovex	$⊢ [0, 1] \in V$
40		iooretop	$⊢ (A, +∞) \in topGen (ran (.))$
41		elrestr	$⊢ (topGen (ran (.)) \in V \land [0, 1] \in V \land (A, +∞) \in topGen (ran (.))) \to (A, +∞) \cap [0, 1] \in (topGen (ran (.)) ↾_{𝑡} [0, 1])$
42	38 39 40 41	mp3an	$⊢ (A, +∞) \cap [0, 1] \in (topGen (ran (.)) ↾_{𝑡} [0, 1])$
43		dfii2	$⊢ II = topGen (ran (.)) ↾_{𝑡} [0, 1]$
44	42 43	eleqtrri	$⊢ (A, +∞) \cap [0, 1] \in II$
45	37 44	eqeltrrdi	$⊢ 0 \leq A \to (A, 1] \in II$

Metamath Proof Explorer

Theorem io1ii

Proof