i0oii

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

		Ref	Expression
	Assertion	i0oii	$⊢ A \leq 1 \to [0, A) \in II$

Proof

Step	Hyp	Ref	Expression
1		anandi3r	$⊢ (x \in ℝ \land A \leq 1 \land x < A) \leftrightarrow ((x \in ℝ \land A \leq 1) \land (x < A \land A \leq 1))$
2		rexr	$⊢ x \in ℝ \to x \in ℝ^{*}$
3		lerelxr	$⊢ \leq \subseteq ℝ^{} \times ℝ^{}$
4	3	brel	$⊢ A \leq 1 \to (A \in ℝ^{} \land 1 \in ℝ^{})$
5	4	simpld	$⊢ A \leq 1 \to A \in ℝ^{*}$
6		1xr	$⊢ 1 \in ℝ^{*}$
7		xrltletr	$⊢ (x \in ℝ^{} \land A \in ℝ^{} \land 1 \in ℝ^{*}) \to ((x < A \land A \leq 1) \to x < 1)$
8		xrltle	$⊢ (x \in ℝ^{} \land 1 \in ℝ^{}) \to (x < 1 \to x \leq 1)$
9	8	3adant2	$⊢ (x \in ℝ^{} \land A \in ℝ^{} \land 1 \in ℝ^{*}) \to (x < 1 \to x \leq 1)$
10	7 9	syld	$⊢ (x \in ℝ^{} \land A \in ℝ^{} \land 1 \in ℝ^{*}) \to ((x < A \land A \leq 1) \to x \leq 1)$
11	6 10	mp3an3	$⊢ (x \in ℝ^{} \land A \in ℝ^{}) \to ((x < A \land A \leq 1) \to x \leq 1)$
12	2 5 11	syl2an	$⊢ (x \in ℝ \land A \leq 1) \to ((x < A \land A \leq 1) \to x \leq 1)$
13	12	imp	$⊢ ((x \in ℝ \land A \leq 1) \land (x < A \land A \leq 1)) \to x \leq 1$
14	1 13	sylbi	$⊢ (x \in ℝ \land A \leq 1 \land x < A) \to x \leq 1$
15	14	3com12	$⊢ (A \leq 1 \land x \in ℝ \land x < A) \to x \leq 1$
16	15	3expib	$⊢ A \leq 1 \to ((x \in ℝ \land x < A) \to x \leq 1)$
17	16	pm4.71d	$⊢ A \leq 1 \to ((x \in ℝ \land x < A) \leftrightarrow ((x \in ℝ \land x < A) \land x \leq 1))$
18	17	anbi1d	$⊢ A \leq 1 \to (((x \in ℝ \land x < A) \land 0 \leq x) \leftrightarrow (((x \in ℝ \land x < A) \land x \leq 1) \land 0 \leq x))$
19		3anan32	$⊢ (x \in ℝ \land 0 \leq x \land x < A) \leftrightarrow ((x \in ℝ \land x < A) \land 0 \leq x)$
20		3anass	$⊢ (x \in ℝ \land 0 \leq x \land x \leq 1) \leftrightarrow (x \in ℝ \land (0 \leq x \land x \leq 1))$
21	20	anbi2i	$⊢ ((x \in ℝ \land x < A) \land (x \in ℝ \land 0 \leq x \land x \leq 1)) \leftrightarrow ((x \in ℝ \land x < A) \land (x \in ℝ \land (0 \leq x \land x \leq 1)))$
22		anandi	$⊢ (x \in ℝ \land (x < A \land (0 \leq x \land x \leq 1))) \leftrightarrow ((x \in ℝ \land x < A) \land (x \in ℝ \land (0 \leq x \land x \leq 1)))$
23		3anass	$⊢ ((x \in ℝ \land x < A) \land 0 \leq x \land x \leq 1) \leftrightarrow ((x \in ℝ \land x < A) \land (0 \leq x \land x \leq 1))$
24		3anan32	$⊢ ((x \in ℝ \land x < A) \land 0 \leq x \land x \leq 1) \leftrightarrow (((x \in ℝ \land x < A) \land x \leq 1) \land 0 \leq x)$
25		anass	$⊢ ((x \in ℝ \land x < A) \land (0 \leq x \land x \leq 1)) \leftrightarrow (x \in ℝ \land (x < A \land (0 \leq x \land x \leq 1)))$
26	23 24 25	3bitr3ri	$⊢ (x \in ℝ \land (x < A \land (0 \leq x \land x \leq 1))) \leftrightarrow (((x \in ℝ \land x < A) \land x \leq 1) \land 0 \leq x)$
27	21 22 26	3bitr2i	$⊢ ((x \in ℝ \land x < A) \land (x \in ℝ \land 0 \leq x \land x \leq 1)) \leftrightarrow (((x \in ℝ \land x < A) \land x \leq 1) \land 0 \leq x)$
28	18 19 27	3bitr4g	$⊢ A \leq 1 \to ((x \in ℝ \land 0 \leq x \land x < A) \leftrightarrow ((x \in ℝ \land x < A) \land (x \in ℝ \land 0 \leq x \land x \leq 1)))$
29		0re	$⊢ 0 \in ℝ$
30		elico2	$⊢ (0 \in ℝ \land A \in ℝ^{*}) \to (x \in [0, A) \leftrightarrow (x \in ℝ \land 0 \leq x \land x < A))$
31	29 5 30	sylancr	$⊢ A \leq 1 \to (x \in [0, A) \leftrightarrow (x \in ℝ \land 0 \leq x \land x < A))$
32		elin	$⊢ x \in ((−∞, A) \cap [0, 1]) \leftrightarrow (x \in (−∞, A) \land x \in [0, 1])$
33		elicc01	$⊢ x \in [0, 1] \leftrightarrow (x \in ℝ \land 0 \leq x \land x \leq 1)$
34	33	anbi2i	$⊢ (x \in (−∞, A) \land x \in [0, 1]) \leftrightarrow (x \in (−∞, A) \land (x \in ℝ \land 0 \leq x \land x \leq 1))$
35	32 34	bitri	$⊢ x \in ((−∞, A) \cap [0, 1]) \leftrightarrow (x \in (−∞, A) \land (x \in ℝ \land 0 \leq x \land x \leq 1))$
36		elioomnf	$⊢ A \in ℝ^{*} \to (x \in (−∞, A) \leftrightarrow (x \in ℝ \land x < A))$
37	5 36	syl	$⊢ A \leq 1 \to (x \in (−∞, A) \leftrightarrow (x \in ℝ \land x < A))$
38	37	anbi1d	$⊢ A \leq 1 \to ((x \in (−∞, A) \land (x \in ℝ \land 0 \leq x \land x \leq 1)) \leftrightarrow ((x \in ℝ \land x < A) \land (x \in ℝ \land 0 \leq x \land x \leq 1)))$
39	35 38	bitrid	$⊢ A \leq 1 \to (x \in ((−∞, A) \cap [0, 1]) \leftrightarrow ((x \in ℝ \land x < A) \land (x \in ℝ \land 0 \leq x \land x \leq 1)))$
40	28 31 39	3bitr4rd	$⊢ A \leq 1 \to (x \in ((−∞, A) \cap [0, 1]) \leftrightarrow x \in [0, A))$
41	40	eqrdv	$⊢ A \leq 1 \to (−∞, A) \cap [0, 1] = [0, A)$
42		fvex	$⊢ topGen (ran (.)) \in V$
43		ovex	$⊢ [0, 1] \in V$
44		iooretop	$⊢ (−∞, A) \in topGen (ran (.))$
45		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])$
46	42 43 44 45	mp3an	$⊢ (−∞, A) \cap [0, 1] \in (topGen (ran (.)) ↾_{𝑡} [0, 1])$
47		dfii2	$⊢ II = topGen (ran (.)) ↾_{𝑡} [0, 1]$
48	46 47	eleqtrri	$⊢ (−∞, A) \cap [0, 1] \in II$
49	41 48	eqeltrrdi	$⊢ A \leq 1 \to [0, A) \in II$

Metamath Proof Explorer

Theorem i0oii

Proof