iooiinioc

Description: A left-open, right-closed interval expressed as the indexed intersection of open intervals. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	iooiinioc.1	$⊢ φ \to A \in ℝ^{*}$
	iooiinioc.2	$⊢ φ \to B \in ℝ$
Assertion	iooiinioc	$⊢ φ \to ⋂_{n \in ℕ} (A, B + (\frac{1}{n})) = (A, B]$

Proof

Step	Hyp	Ref	Expression
1		iooiinioc.1	$⊢ φ \to A \in ℝ^{*}$
2		iooiinioc.2	$⊢ φ \to B \in ℝ$
3	1	adantr	$⊢ (φ \land x \in ⋂_{n \in ℕ} (A, B + (\frac{1}{n}))) \to A \in ℝ^{*}$
4	2	adantr	$⊢ (φ \land x \in ⋂_{n \in ℕ} (A, B + (\frac{1}{n}))) \to B \in ℝ$
5	4	rexrd	$⊢ (φ \land x \in ⋂_{n \in ℕ} (A, B + (\frac{1}{n}))) \to B \in ℝ^{*}$
6		1nn	$⊢ 1 \in ℕ$
7		ioossre	$⊢ (A, B + (\frac{1}{1})) \subseteq ℝ$
8		oveq2	$⊢ n = 1 \to \frac{1}{n} = \frac{1}{1}$
9	8	oveq2d	$⊢ n = 1 \to B + (\frac{1}{n}) = B + (\frac{1}{1})$
10	9	oveq2d	$⊢ n = 1 \to (A, B + (\frac{1}{n})) = (A, B + (\frac{1}{1}))$
11	10	sseq1d	$⊢ n = 1 \to ((A, B + (\frac{1}{n})) \subseteq ℝ \leftrightarrow (A, B + (\frac{1}{1})) \subseteq ℝ)$
12	11	rspcev	$⊢ (1 \in ℕ \land (A, B + (\frac{1}{1})) \subseteq ℝ) \to \exists n \in ℕ (A, B + (\frac{1}{n})) \subseteq ℝ$
13	6 7 12	mp2an	$⊢ \exists n \in ℕ (A, B + (\frac{1}{n})) \subseteq ℝ$
14		iinss	$⊢ \exists n \in ℕ (A, B + (\frac{1}{n})) \subseteq ℝ \to ⋂_{n \in ℕ} (A, B + (\frac{1}{n})) \subseteq ℝ$
15	13 14	ax-mp	$⊢ ⋂_{n \in ℕ} (A, B + (\frac{1}{n})) \subseteq ℝ$
16	15	a1i	$⊢ (φ \land x \in ⋂_{n \in ℕ} (A, B + (\frac{1}{n}))) \to ⋂_{n \in ℕ} (A, B + (\frac{1}{n})) \subseteq ℝ$
17		simpr	$⊢ (φ \land x \in ⋂_{n \in ℕ} (A, B + (\frac{1}{n}))) \to x \in ⋂_{n \in ℕ} (A, B + (\frac{1}{n}))$
18	16 17	sseldd	$⊢ (φ \land x \in ⋂_{n \in ℕ} (A, B + (\frac{1}{n}))) \to x \in ℝ$
19	18	rexrd	$⊢ (φ \land x \in ⋂_{n \in ℕ} (A, B + (\frac{1}{n}))) \to x \in ℝ^{*}$
20		1red	$⊢ φ \to 1 \in ℝ$
21		ax-1ne0	$⊢ 1 \neq 0$
22	21	a1i	$⊢ φ \to 1 \neq 0$
23	20 20 22	redivcld	$⊢ φ \to \frac{1}{1} \in ℝ$
24	2 23	readdcld	$⊢ φ \to B + (\frac{1}{1}) \in ℝ$
25	24	rexrd	$⊢ φ \to B + (\frac{1}{1}) \in ℝ^{*}$
26	25	adantr	$⊢ (φ \land x \in ⋂_{n \in ℕ} (A, B + (\frac{1}{n}))) \to B + (\frac{1}{1}) \in ℝ^{*}$
27		id	$⊢ x \in ⋂_{n \in ℕ} (A, B + (\frac{1}{n})) \to x \in ⋂_{n \in ℕ} (A, B + (\frac{1}{n}))$
28	6	a1i	$⊢ x \in ⋂_{n \in ℕ} (A, B + (\frac{1}{n})) \to 1 \in ℕ$
29	10	eleq2d	$⊢ n = 1 \to (x \in (A, B + (\frac{1}{n})) \leftrightarrow x \in (A, B + (\frac{1}{1})))$
30	27 28 29	eliind	$⊢ x \in ⋂_{n \in ℕ} (A, B + (\frac{1}{n})) \to x \in (A, B + (\frac{1}{1}))$
31	30	adantl	$⊢ (φ \land x \in ⋂_{n \in ℕ} (A, B + (\frac{1}{n}))) \to x \in (A, B + (\frac{1}{1}))$
32		ioogtlb	$⊢ (A \in ℝ^{} \land B + (\frac{1}{1}) \in ℝ^{} \land x \in (A, B + (\frac{1}{1}))) \to A < x$
33	3 26 31 32	syl3anc	$⊢ (φ \land x \in ⋂_{n \in ℕ} (A, B + (\frac{1}{n}))) \to A < x$
34		nfv	$⊢ Ⅎ n φ$
35		nfcv	$⊢ \underline{Ⅎ} n x$
36		nfii1	$⊢ \underline{Ⅎ} n ⋂_{n \in ℕ} (A, B + (\frac{1}{n}))$
37	35 36	nfel	$⊢ Ⅎ n x \in ⋂_{n \in ℕ} (A, B + (\frac{1}{n}))$
38	34 37	nfan	$⊢ Ⅎ n (φ \land x \in ⋂_{n \in ℕ} (A, B + (\frac{1}{n})))$
39		simpll	$⊢ ((φ \land x \in ⋂_{n \in ℕ} (A, B + (\frac{1}{n}))) \land n \in ℕ) \to φ$
40		iinss2	$⊢ n \in ℕ \to ⋂_{n \in ℕ} (A, B + (\frac{1}{n})) \subseteq (A, B + (\frac{1}{n}))$
41	40	adantl	$⊢ (x \in ⋂_{n \in ℕ} (A, B + (\frac{1}{n})) \land n \in ℕ) \to ⋂_{n \in ℕ} (A, B + (\frac{1}{n})) \subseteq (A, B + (\frac{1}{n}))$
42		simpl	$⊢ (x \in ⋂_{n \in ℕ} (A, B + (\frac{1}{n})) \land n \in ℕ) \to x \in ⋂_{n \in ℕ} (A, B + (\frac{1}{n}))$
43	41 42	sseldd	$⊢ (x \in ⋂_{n \in ℕ} (A, B + (\frac{1}{n})) \land n \in ℕ) \to x \in (A, B + (\frac{1}{n}))$
44	43	adantll	$⊢ ((φ \land x \in ⋂_{n \in ℕ} (A, B + (\frac{1}{n}))) \land n \in ℕ) \to x \in (A, B + (\frac{1}{n}))$
45		simpr	$⊢ ((φ \land x \in ⋂_{n \in ℕ} (A, B + (\frac{1}{n}))) \land n \in ℕ) \to n \in ℕ$
46		elioore	$⊢ x \in (A, B + (\frac{1}{n})) \to x \in ℝ$
47	46	adantr	$⊢ (x \in (A, B + (\frac{1}{n})) \land n \in ℕ) \to x \in ℝ$
48	47	adantll	$⊢ ((φ \land x \in (A, B + (\frac{1}{n}))) \land n \in ℕ) \to x \in ℝ$
49	2	adantr	$⊢ (φ \land n \in ℕ) \to B \in ℝ$
50		nnrecre	$⊢ n \in ℕ \to \frac{1}{n} \in ℝ$
51	50	adantl	$⊢ (φ \land n \in ℕ) \to \frac{1}{n} \in ℝ$
52	49 51	readdcld	$⊢ (φ \land n \in ℕ) \to B + (\frac{1}{n}) \in ℝ$
53	52	adantlr	$⊢ ((φ \land x \in (A, B + (\frac{1}{n}))) \land n \in ℕ) \to B + (\frac{1}{n}) \in ℝ$
54	1	adantr	$⊢ (φ \land n \in ℕ) \to A \in ℝ^{*}$
55	54	adantlr	$⊢ ((φ \land x \in (A, B + (\frac{1}{n}))) \land n \in ℕ) \to A \in ℝ^{*}$
56	52	rexrd	$⊢ (φ \land n \in ℕ) \to B + (\frac{1}{n}) \in ℝ^{*}$
57	56	adantlr	$⊢ ((φ \land x \in (A, B + (\frac{1}{n}))) \land n \in ℕ) \to B + (\frac{1}{n}) \in ℝ^{*}$
58		simplr	$⊢ ((φ \land x \in (A, B + (\frac{1}{n}))) \land n \in ℕ) \to x \in (A, B + (\frac{1}{n}))$
59		iooltub	$⊢ (A \in ℝ^{} \land B + (\frac{1}{n}) \in ℝ^{} \land x \in (A, B + (\frac{1}{n}))) \to x < B + (\frac{1}{n})$
60	55 57 58 59	syl3anc	$⊢ ((φ \land x \in (A, B + (\frac{1}{n}))) \land n \in ℕ) \to x < B + (\frac{1}{n})$
61	48 53 60	ltled	$⊢ ((φ \land x \in (A, B + (\frac{1}{n}))) \land n \in ℕ) \to x \leq B + (\frac{1}{n})$
62	39 44 45 61	syl21anc	$⊢ ((φ \land x \in ⋂_{n \in ℕ} (A, B + (\frac{1}{n}))) \land n \in ℕ) \to x \leq B + (\frac{1}{n})$
63	62	ex	$⊢ (φ \land x \in ⋂_{n \in ℕ} (A, B + (\frac{1}{n}))) \to (n \in ℕ \to x \leq B + (\frac{1}{n}))$
64	38 63	ralrimi	$⊢ (φ \land x \in ⋂_{n \in ℕ} (A, B + (\frac{1}{n}))) \to \forall n \in ℕ x \leq B + (\frac{1}{n})$
65	38 19 4	xrralrecnnle	$⊢ (φ \land x \in ⋂_{n \in ℕ} (A, B + (\frac{1}{n}))) \to (x \leq B \leftrightarrow \forall n \in ℕ x \leq B + (\frac{1}{n}))$
66	64 65	mpbird	$⊢ (φ \land x \in ⋂_{n \in ℕ} (A, B + (\frac{1}{n}))) \to x \leq B$
67	3 5 19 33 66	eliocd	$⊢ (φ \land x \in ⋂_{n \in ℕ} (A, B + (\frac{1}{n}))) \to x \in (A, B]$
68	67	ralrimiva	$⊢ φ \to \forall x \in ⋂_{n \in ℕ} (A, B + (\frac{1}{n})) x \in (A, B]$
69		dfss3	$⊢ ⋂_{n \in ℕ} (A, B + (\frac{1}{n})) \subseteq (A, B] \leftrightarrow \forall x \in ⋂_{n \in ℕ} (A, B + (\frac{1}{n})) x \in (A, B]$
70	68 69	sylibr	$⊢ φ \to ⋂_{n \in ℕ} (A, B + (\frac{1}{n})) \subseteq (A, B]$
71	1	xrleidd	$⊢ φ \to A \leq A$
72	71	adantr	$⊢ (φ \land n \in ℕ) \to A \leq A$
73		1rp	$⊢ 1 \in ℝ^{+}$
74	73	a1i	$⊢ n \in ℕ \to 1 \in ℝ^{+}$
75		nnrp	$⊢ n \in ℕ \to n \in ℝ^{+}$
76	74 75	rpdivcld	$⊢ n \in ℕ \to \frac{1}{n} \in ℝ^{+}$
77	76	adantl	$⊢ (φ \land n \in ℕ) \to \frac{1}{n} \in ℝ^{+}$
78	49 77	ltaddrpd	$⊢ (φ \land n \in ℕ) \to B < B + (\frac{1}{n})$
79		iocssioo	$⊢ ((A \in ℝ^{} \land B + (\frac{1}{n}) \in ℝ^{}) \land (A \leq A \land B < B + (\frac{1}{n}))) \to (A, B] \subseteq (A, B + (\frac{1}{n}))$
80	54 56 72 78 79	syl22anc	$⊢ (φ \land n \in ℕ) \to (A, B] \subseteq (A, B + (\frac{1}{n}))$
81	80	ralrimiva	$⊢ φ \to \forall n \in ℕ (A, B] \subseteq (A, B + (\frac{1}{n}))$
82		ssiin	$⊢ (A, B] \subseteq ⋂_{n \in ℕ} (A, B + (\frac{1}{n})) \leftrightarrow \forall n \in ℕ (A, B] \subseteq (A, B + (\frac{1}{n}))$
83	81 82	sylibr	$⊢ φ \to (A, B] \subseteq ⋂_{n \in ℕ} (A, B + (\frac{1}{n}))$
84	70 83	eqssd	$⊢ φ \to ⋂_{n \in ℕ} (A, B + (\frac{1}{n})) = (A, B]$

Metamath Proof Explorer

Theorem iooiinioc

Proof