iinhoiicclem

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

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

Proof

Step	Hyp	Ref	Expression
1		iinhoiicclem.k	$⊢ Ⅎ k φ$
2		iinhoiicclem.a	$⊢ (φ \land k \in X) \to A \in ℝ$
3		iinhoiicclem.b	$⊢ (φ \land k \in X) \to B \in ℝ$
4		iinhoiicclem.f	$⊢ φ \to F \in ⋂_{n \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{n}))$
5	4	elexd	$⊢ φ \to F \in V$
6		1nn	$⊢ 1 \in ℕ$
7	6	a1i	$⊢ φ \to 1 \in ℕ$
8		peano2re	$⊢ B \in ℝ \to B + 1 \in ℝ$
9	3 8	syl	$⊢ (φ \land k \in X) \to B + 1 \in ℝ$
10	9	rexrd	$⊢ (φ \land k \in X) \to B + 1 \in ℝ^{*}$
11		icossre	$⊢ (A \in ℝ \land B + 1 \in ℝ^{*}) \to [A, B + 1) \subseteq ℝ$
12	2 10 11	syl2anc	$⊢ (φ \land k \in X) \to [A, B + 1) \subseteq ℝ$
13	1 12	ixpssixp	$⊢ φ \to \underset{k \in X}{⨉} [A, B + 1) \subseteq \underset{k \in X}{⨉} ℝ$
14		oveq2	$⊢ n = 1 \to \frac{1}{n} = \frac{1}{1}$
15		1div1e1	$⊢ \frac{1}{1} = 1$
16	15	a1i	$⊢ n = 1 \to \frac{1}{1} = 1$
17	14 16	eqtrd	$⊢ n = 1 \to \frac{1}{n} = 1$
18	17	oveq2d	$⊢ n = 1 \to B + (\frac{1}{n}) = B + 1$
19	18	oveq2d	$⊢ n = 1 \to [A, B + (\frac{1}{n})) = [A, B + 1)$
20	19	ixpeq2dv	$⊢ n = 1 \to \underset{k \in X}{⨉} [A, B + (\frac{1}{n})) = \underset{k \in X}{⨉} [A, B + 1)$
21	20	sseq1d	$⊢ n = 1 \to (\underset{k \in X}{⨉} [A, B + (\frac{1}{n})) \subseteq \underset{k \in X}{⨉} ℝ \leftrightarrow \underset{k \in X}{⨉} [A, B + 1) \subseteq \underset{k \in X}{⨉} ℝ)$
22	21	rspcev	$⊢ (1 \in ℕ \land \underset{k \in X}{⨉} [A, B + 1) \subseteq \underset{k \in X}{⨉} ℝ) \to \exists n \in ℕ \underset{k \in X}{⨉} [A, B + (\frac{1}{n})) \subseteq \underset{k \in X}{⨉} ℝ$
23	7 13 22	syl2anc	$⊢ φ \to \exists n \in ℕ \underset{k \in X}{⨉} [A, B + (\frac{1}{n})) \subseteq \underset{k \in X}{⨉} ℝ$
24		iinss	$⊢ \exists n \in ℕ \underset{k \in X}{⨉} [A, B + (\frac{1}{n})) \subseteq \underset{k \in X}{⨉} ℝ \to ⋂_{n \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{n})) \subseteq \underset{k \in X}{⨉} ℝ$
25	23 24	syl	$⊢ φ \to ⋂_{n \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{n})) \subseteq \underset{k \in X}{⨉} ℝ$
26	25 4	sseldd	$⊢ φ \to F \in \underset{k \in X}{⨉} ℝ$
27		elixpconstg	$⊢ F \in ⋂_{n \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{n})) \to (F \in \underset{k \in X}{⨉} ℝ \leftrightarrow F : X ⟶ ℝ)$
28	4 27	syl	$⊢ φ \to (F \in \underset{k \in X}{⨉} ℝ \leftrightarrow F : X ⟶ ℝ)$
29	26 28	mpbid	$⊢ φ \to F : X ⟶ ℝ$
30	29	ffnd	$⊢ φ \to F Fn X$
31	29	ffvelrnda	$⊢ (φ \land k \in X) \to F (k) \in ℝ$
32	2	rexrd	$⊢ (φ \land k \in X) \to A \in ℝ^{*}$
33		ssid	$⊢ \underset{k \in X}{⨉} [A, B + 1) \subseteq \underset{k \in X}{⨉} [A, B + 1)$
34	33	a1i	$⊢ φ \to \underset{k \in X}{⨉} [A, B + 1) \subseteq \underset{k \in X}{⨉} [A, B + 1)$
35	20	sseq1d	$⊢ n = 1 \to (\underset{k \in X}{⨉} [A, B + (\frac{1}{n})) \subseteq \underset{k \in X}{⨉} [A, B + 1) \leftrightarrow \underset{k \in X}{⨉} [A, B + 1) \subseteq \underset{k \in X}{⨉} [A, B + 1))$
36	35	rspcev	$⊢ (1 \in ℕ \land \underset{k \in X}{⨉} [A, B + 1) \subseteq \underset{k \in X}{⨉} [A, B + 1)) \to \exists n \in ℕ \underset{k \in X}{⨉} [A, B + (\frac{1}{n})) \subseteq \underset{k \in X}{⨉} [A, B + 1)$
37	7 34 36	syl2anc	$⊢ φ \to \exists n \in ℕ \underset{k \in X}{⨉} [A, B + (\frac{1}{n})) \subseteq \underset{k \in X}{⨉} [A, B + 1)$
38		iinss	$⊢ \exists n \in ℕ \underset{k \in X}{⨉} [A, B + (\frac{1}{n})) \subseteq \underset{k \in X}{⨉} [A, B + 1) \to ⋂_{n \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{n})) \subseteq \underset{k \in X}{⨉} [A, B + 1)$
39	37 38	syl	$⊢ φ \to ⋂_{n \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{n})) \subseteq \underset{k \in X}{⨉} [A, B + 1)$
40	39 4	sseldd	$⊢ φ \to F \in \underset{k \in X}{⨉} [A, B + 1)$
41	40	adantr	$⊢ (φ \land k \in X) \to F \in \underset{k \in X}{⨉} [A, B + 1)$
42		simpr	$⊢ (φ \land k \in X) \to k \in X$
43		fvixp2	$⊢ (F \in \underset{k \in X}{⨉} [A, B + 1) \land k \in X) \to F (k) \in [A, B + 1)$
44	41 42 43	syl2anc	$⊢ (φ \land k \in X) \to F (k) \in [A, B + 1)$
45		icogelb	$⊢ (A \in ℝ^{} \land B + 1 \in ℝ^{} \land F (k) \in [A, B + 1)) \to A \leq F (k)$
46	32 10 44 45	syl3anc	$⊢ (φ \land k \in X) \to A \leq F (k)$
47	31	adantr	$⊢ ((φ \land k \in X) \land n \in ℕ) \to F (k) \in ℝ$
48	3	adantr	$⊢ ((φ \land k \in X) \land n \in ℕ) \to B \in ℝ$
49		nnrecre	$⊢ n \in ℕ \to \frac{1}{n} \in ℝ$
50	49	adantl	$⊢ ((φ \land k \in X) \land n \in ℕ) \to \frac{1}{n} \in ℝ$
51	48 50	readdcld	$⊢ ((φ \land k \in X) \land n \in ℕ) \to B + (\frac{1}{n}) \in ℝ$
52	32	adantr	$⊢ ((φ \land k \in X) \land n \in ℕ) \to A \in ℝ^{*}$
53		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
54	53 51	sseldi	$⊢ ((φ \land k \in X) \land n \in ℕ) \to B + (\frac{1}{n}) \in ℝ^{*}$
55		eliin	$⊢ F \in V \to (F \in ⋂_{n \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{n})) \leftrightarrow \forall n \in ℕ F \in \underset{k \in X}{⨉} [A, B + (\frac{1}{n})))$
56	5 55	syl	$⊢ φ \to (F \in ⋂_{n \in ℕ} \underset{k \in X}{⨉} [A, B + (\frac{1}{n})) \leftrightarrow \forall n \in ℕ F \in \underset{k \in X}{⨉} [A, B + (\frac{1}{n})))$
57	4 56	mpbid	$⊢ φ \to \forall n \in ℕ F \in \underset{k \in X}{⨉} [A, B + (\frac{1}{n}))$
58	57	r19.21bi	$⊢ (φ \land n \in ℕ) \to F \in \underset{k \in X}{⨉} [A, B + (\frac{1}{n}))$
59		elixp2	$⊢ F \in \underset{k \in X}{⨉} [A, B + (\frac{1}{n})) \leftrightarrow (F \in V \land F Fn X \land \forall k \in X F (k) \in [A, B + (\frac{1}{n})))$
60	58 59	sylib	$⊢ (φ \land n \in ℕ) \to (F \in V \land F Fn X \land \forall k \in X F (k) \in [A, B + (\frac{1}{n})))$
61	60	simp3d	$⊢ (φ \land n \in ℕ) \to \forall k \in X F (k) \in [A, B + (\frac{1}{n}))$
62	61	r19.21bi	$⊢ ((φ \land n \in ℕ) \land k \in X) \to F (k) \in [A, B + (\frac{1}{n}))$
63	62	an32s	$⊢ ((φ \land k \in X) \land n \in ℕ) \to F (k) \in [A, B + (\frac{1}{n}))$
64		icoltub	$⊢ (A \in ℝ^{} \land B + (\frac{1}{n}) \in ℝ^{} \land F (k) \in [A, B + (\frac{1}{n}))) \to F (k) < B + (\frac{1}{n})$
65	52 54 63 64	syl3anc	$⊢ ((φ \land k \in X) \land n \in ℕ) \to F (k) < B + (\frac{1}{n})$
66	47 51 65	ltled	$⊢ ((φ \land k \in X) \land n \in ℕ) \to F (k) \leq B + (\frac{1}{n})$
67	66	ralrimiva	$⊢ (φ \land k \in X) \to \forall n \in ℕ F (k) \leq B + (\frac{1}{n})$
68		nfv	$⊢ Ⅎ n (φ \land k \in X)$
69	53 31	sseldi	$⊢ (φ \land k \in X) \to F (k) \in ℝ^{*}$
70	68 69 3	xrralrecnnle	$⊢ (φ \land k \in X) \to (F (k) \leq B \leftrightarrow \forall n \in ℕ F (k) \leq B + (\frac{1}{n}))$
71	67 70	mpbird	$⊢ (φ \land k \in X) \to F (k) \leq B$
72	2 3 31 46 71	eliccd	$⊢ (φ \land k \in X) \to F (k) \in [A, B]$
73	72	ex	$⊢ φ \to (k \in X \to F (k) \in [A, B])$
74	1 73	ralrimi	$⊢ φ \to \forall k \in X F (k) \in [A, B]$
75	5 30 74	3jca	$⊢ φ \to (F \in V \land F Fn X \land \forall k \in X F (k) \in [A, B])$
76		elixp2	$⊢ F \in \underset{k \in X}{⨉} [A, B] \leftrightarrow (F \in V \land F Fn X \land \forall k \in X F (k) \in [A, B])$
77	75 76	sylibr	$⊢ φ \to F \in \underset{k \in X}{⨉} [A, B]$

Metamath Proof Explorer

Theorem iinhoiicclem

Proof