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	bilani	$⊢ (φ \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}))$
11		nfcv	$⊢ \underline{Ⅎ} k f$
12		nfcv	$⊢ \underline{Ⅎ} k ℕ$
13		nfixp1	$⊢ \underline{Ⅎ} k \underset{k \in X}{⨉} [A, B + (\frac{1}{m}))$
14	12 13	nfiin	$⊢ \underline{Ⅎ} k ⋂_{m \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{m}))$
15	11 14	nfel	$⊢ Ⅎ k f \in ⋂_{m \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{m}))$
16	1 15	nfan	$⊢ Ⅎ k (φ \land f \in ⋂_{m \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{m})))$
17	2	adantlr	$⊢ ((φ \land f \in ⋂_{m \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{m}))) \land k \in X) \to A \in ℝ$
18	3	adantlr	$⊢ ((φ \land f \in ⋂_{m \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{m}))) \land k \in X) \to B \in ℝ$
19	9	bilanri	$⊢ (φ \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}))$
20	16 17 18 19	iinhoiicclem	$⊢ (φ \land f \in ⋂_{m \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{m}))) \to f \in \underset{k \in X}{⨉} [A, B]$
21	10 20	syldan	$⊢ (φ \land f \in ⋂_{n \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{n}))) \to f \in \underset{k \in X}{⨉} [A, B]$
22	21	ralrimiva	$⊢ φ \to \forall f \in ⋂_{n \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{n})) f \in \underset{k \in X}{⨉} [A, B]$
23		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]$
24	22 23	sylibr	$⊢ φ \to ⋂_{n \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{n})) \subseteq \underset{k \in X}{⨉} [A, B]$
25		nfv	$⊢ Ⅎ k n \in ℕ$
26	1 25	nfan	$⊢ Ⅎ k (φ \land n \in ℕ)$
27	2	rexrd	$⊢ (φ \land k \in X) \to A \in ℝ^{*}$
28	27	adantlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to A \in ℝ^{*}$
29	3	adantlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to B \in ℝ$
30		nnrp	$⊢ n \in ℕ \to n \in ℝ^{+}$
31	30	ad2antlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to n \in ℝ^{+}$
32	31	rpreccld	$⊢ ((φ \land n \in ℕ) \land k \in X) \to \frac{1}{n} \in ℝ^{+}$
33	32	rpred	$⊢ ((φ \land n \in ℕ) \land k \in X) \to \frac{1}{n} \in ℝ$
34	29 33	readdcld	$⊢ ((φ \land n \in ℕ) \land k \in X) \to B + (\frac{1}{n}) \in ℝ$
35	34	rexrd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to B + (\frac{1}{n}) \in ℝ^{*}$
36	2	adantlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to A \in ℝ$
37	36	leidd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to A \leq A$
38	29 32	ltaddrpd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to B < B + (\frac{1}{n})$
39		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}))$
40	28 35 37 38 39	syl22anc	$⊢ ((φ \land n \in ℕ) \land k \in X) \to [A, B] \subseteq [A, B + (\frac{1}{n}))$
41	26 40	ixpssixp	$⊢ (φ \land n \in ℕ) \to \underset{k \in X}{⨉} [A, B] \subseteq \underset{k \in X}{⨉} [A, B + (\frac{1}{n}))$
42	41	ralrimiva	$⊢ φ \to \forall n \in ℕ \underset{k \in X}{⨉} [A, B] \subseteq \underset{k \in X}{⨉} [A, B + (\frac{1}{n}))$
43		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}))$
44	42 43	sylibr	$⊢ φ \to \underset{k \in X}{⨉} [A, B] \subseteq ⋂_{n \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{n}))$
45	24 44	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