iinhoiicc

Description: A n-dimensional closed interval expressed as the indexed intersection of half-open intervals. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	iunhoiicc.k	$⊢ Ⅎ k φ$
	iunhoiicc.a	$⊢ (φ \land k \in X) \to A \in ℝ$
	iunhoiicc.b	$⊢ (φ \land k \in X) \to B \in ℝ$
Assertion	iinhoiicc	$⊢ φ \to ⋂_{n \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{n})) = \underset{k \in X}{⨉} [A, B]$

Proof

Step	Hyp	Ref	Expression
1		iunhoiicc.k	$⊢ Ⅎ k φ$
2		iunhoiicc.a	$⊢ (φ \land k \in X) \to A \in ℝ$
3		iunhoiicc.b	$⊢ (φ \land k \in X) \to B \in ℝ$
4		oveq2	$⊢ n = m \to \frac{1}{n} = \frac{1}{m}$
5	4	oveq2d	$⊢ n = m \to B + (\frac{1}{n}) = B + (\frac{1}{m})$
6	5	oveq2d	$⊢ n = m \to [A, B + (\frac{1}{n})) = [A, B + (\frac{1}{m}))$
7	6	ixpeq2dv	$⊢ n = m \to \underset{k \in X}{⨉} [A, B + (\frac{1}{n})) = \underset{k \in X}{⨉} [A, B + (\frac{1}{m}))$
8	7	cbviinv	$⊢ ⋂_{n \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{n})) = ⋂_{m \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{m}))$
9	8	eleq2i	$⊢ f \in ⋂_{n \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{n})) \leftrightarrow f \in ⋂_{m \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{m}))$
10	9	biimpi	$⊢ f \in ⋂_{n \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{n})) \to f \in ⋂_{m \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{m}))$
11	10	adantl	$⊢ (φ \land f \in ⋂_{n \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{n}))) \to f \in ⋂_{m \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{m}))$
12		nfcv	$⊢ \underline{Ⅎ} k f$
13		nfcv	$⊢ \underline{Ⅎ} k ℕ$
14		nfixp1	$⊢ \underline{Ⅎ} k \underset{k \in X}{⨉} [A, B + (\frac{1}{m}))$
15	13 14	nfiin	$⊢ \underline{Ⅎ} k ⋂_{m \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{m}))$
16	12 15	nfel	$⊢ Ⅎ k f \in ⋂_{m \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{m}))$
17	1 16	nfan	$⊢ Ⅎ k (φ \land f \in ⋂_{m \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{m})))$
18	2	adantlr	$⊢ ((φ \land f \in ⋂_{m \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{m}))) \land k \in X) \to A \in ℝ$
19	3	adantlr	$⊢ ((φ \land f \in ⋂_{m \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{m}))) \land k \in X) \to B \in ℝ$
20	9	biimpri	$⊢ f \in ⋂_{m \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{m})) \to f \in ⋂_{n \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{n}))$
21	20	adantl	$⊢ (φ \land f \in ⋂_{m \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{m}))) \to f \in ⋂_{n \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{n}))$
22	17 18 19 21	iinhoiicclem	$⊢ (φ \land f \in ⋂_{m \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{m}))) \to f \in \underset{k \in X}{⨉} [A, B]$
23	11 22	syldan	$⊢ (φ \land f \in ⋂_{n \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{n}))) \to f \in \underset{k \in X}{⨉} [A, B]$
24	23	ralrimiva	$⊢ φ \to \forall f \in ⋂_{n \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{n})) f \in \underset{k \in X}{⨉} [A, B]$
25		dfss3	$⊢ ⋂_{n \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{n})) \subseteq \underset{k \in X}{⨉} [A, B] \leftrightarrow \forall f \in ⋂_{n \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{n})) f \in \underset{k \in X}{⨉} [A, B]$
26	24 25	sylibr	$⊢ φ \to ⋂_{n \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{n})) \subseteq \underset{k \in X}{⨉} [A, B]$
27		nfv	$⊢ Ⅎ k n \in ℕ$
28	1 27	nfan	$⊢ Ⅎ k (φ \land n \in ℕ)$
29	2	rexrd	$⊢ (φ \land k \in X) \to A \in ℝ^{*}$
30	29	adantlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to A \in ℝ^{*}$
31	3	adantlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to B \in ℝ$
32		nnrp	$⊢ n \in ℕ \to n \in ℝ^{+}$
33	32	ad2antlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to n \in ℝ^{+}$
34	33	rpreccld	$⊢ ((φ \land n \in ℕ) \land k \in X) \to \frac{1}{n} \in ℝ^{+}$
35	34	rpred	$⊢ ((φ \land n \in ℕ) \land k \in X) \to \frac{1}{n} \in ℝ$
36	31 35	readdcld	$⊢ ((φ \land n \in ℕ) \land k \in X) \to B + (\frac{1}{n}) \in ℝ$
37	36	rexrd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to B + (\frac{1}{n}) \in ℝ^{*}$
38	2	adantlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to A \in ℝ$
39	38	leidd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to A \leq A$
40	31 34	ltaddrpd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to B < B + (\frac{1}{n})$
41		iccssico	$⊢ ((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}))$
42	30 37 39 40 41	syl22anc	$⊢ ((φ \land n \in ℕ) \land k \in X) \to [A, B] \subseteq [A, B + (\frac{1}{n}))$
43	28 42	ixpssixp	$⊢ (φ \land n \in ℕ) \to \underset{k \in X}{⨉} [A, B] \subseteq \underset{k \in X}{⨉} [A, B + (\frac{1}{n}))$
44	43	ralrimiva	$⊢ φ \to \forall n \in ℕ \underset{k \in X}{⨉} [A, B] \subseteq \underset{k \in X}{⨉} [A, B + (\frac{1}{n}))$
45		ssiin	$⊢ \underset{k \in X}{⨉} [A, B] \subseteq ⋂_{n \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{n})) \leftrightarrow \forall n \in ℕ \underset{k \in X}{⨉} [A, B] \subseteq \underset{k \in X}{⨉} [A, B + (\frac{1}{n}))$
46	44 45	sylibr	$⊢ φ \to \underset{k \in X}{⨉} [A, B] \subseteq ⋂_{n \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{n}))$
47	26 46	eqssd	$⊢ φ \to ⋂_{n \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{n})) = \underset{k \in X}{⨉} [A, B]$

Metamath Proof Explorer

Theorem iinhoiicc

Proof