iunhoiioo

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

	Ref	Expression
Hypotheses	iunhoiioo.k	$⊢ Ⅎ k φ$
	iunhoiioo.x	$⊢ φ \to X \in Fin$
	iunhoiioo.a	$⊢ (φ \land k \in X) \to A \in ℝ$
	iunhoiioo.b	$⊢ (φ \land k \in X) \to B \in ℝ^{*}$
Assertion	iunhoiioo	$⊢ φ \to ⋃_{n \in ℕ} \underset{k \in X}{⨉} [A + (\frac{1}{n}), B) = \underset{k \in X}{⨉} (A, B)$

Proof

Step	Hyp	Ref	Expression
1		iunhoiioo.k	$⊢ Ⅎ k φ$
2		iunhoiioo.x	$⊢ φ \to X \in Fin$
3		iunhoiioo.a	$⊢ (φ \land k \in X) \to A \in ℝ$
4		iunhoiioo.b	$⊢ (φ \land k \in X) \to B \in ℝ^{*}$
5		nnn0	$⊢ ℕ \neq \emptyset$
6		iunconst	$⊢ ℕ \neq \emptyset \to ⋃_{n \in ℕ} \{\emptyset\} = \{\emptyset\}$
7	5 6	ax-mp	$⊢ ⋃_{n \in ℕ} \{\emptyset\} = \{\emptyset\}$
8	7	a1i	$⊢ X = \emptyset \to ⋃_{n \in ℕ} \{\emptyset\} = \{\emptyset\}$
9		ixpeq1	$⊢ X = \emptyset \to \underset{k \in X}{⨉} [A + (\frac{1}{n}), B) = \underset{k \in \emptyset}{⨉} [A + (\frac{1}{n}), B)$
10		ixp0x	$⊢ \underset{k \in \emptyset}{⨉} [A + (\frac{1}{n}), B) = \{\emptyset\}$
11	10	a1i	$⊢ X = \emptyset \to \underset{k \in \emptyset}{⨉} [A + (\frac{1}{n}), B) = \{\emptyset\}$
12	9 11	eqtrd	$⊢ X = \emptyset \to \underset{k \in X}{⨉} [A + (\frac{1}{n}), B) = \{\emptyset\}$
13	12	adantr	$⊢ (X = \emptyset \land n \in ℕ) \to \underset{k \in X}{⨉} [A + (\frac{1}{n}), B) = \{\emptyset\}$
14	13	iuneq2dv	$⊢ X = \emptyset \to ⋃_{n \in ℕ} \underset{k \in X}{⨉} [A + (\frac{1}{n}), B) = ⋃_{n \in ℕ} \{\emptyset\}$
15		ixpeq1	$⊢ X = \emptyset \to \underset{k \in X}{⨉} (A, B) = \underset{k \in \emptyset}{⨉} (A, B)$
16		ixp0x	$⊢ \underset{k \in \emptyset}{⨉} (A, B) = \{\emptyset\}$
17	16	a1i	$⊢ X = \emptyset \to \underset{k \in \emptyset}{⨉} (A, B) = \{\emptyset\}$
18	15 17	eqtrd	$⊢ X = \emptyset \to \underset{k \in X}{⨉} (A, B) = \{\emptyset\}$
19	8 14 18	3eqtr4d	$⊢ X = \emptyset \to ⋃_{n \in ℕ} \underset{k \in X}{⨉} [A + (\frac{1}{n}), B) = \underset{k \in X}{⨉} (A, B)$
20	19	adantl	$⊢ (φ \land X = \emptyset) \to ⋃_{n \in ℕ} \underset{k \in X}{⨉} [A + (\frac{1}{n}), B) = \underset{k \in X}{⨉} (A, B)$
21		nfv	$⊢ Ⅎ k n \in ℕ$
22	1 21	nfan	$⊢ Ⅎ k (φ \land n \in ℕ)$
23	3	rexrd	$⊢ (φ \land k \in X) \to A \in ℝ^{*}$
24	23	adantlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to A \in ℝ^{*}$
25	4	adantlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to B \in ℝ^{*}$
26	3	adantlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to A \in ℝ$
27		nnrp	$⊢ n \in ℕ \to n \in ℝ^{+}$
28	27	ad2antlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to n \in ℝ^{+}$
29	28	rpreccld	$⊢ ((φ \land n \in ℕ) \land k \in X) \to \frac{1}{n} \in ℝ^{+}$
30	26 29	ltaddrpd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to A < A + (\frac{1}{n})$
31	4	xrleidd	$⊢ (φ \land k \in X) \to B \leq B$
32	31	adantlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to B \leq B$
33		icossioo	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A < A + (\frac{1}{n}) \land B \leq B)) \to [A + (\frac{1}{n}), B) \subseteq (A, B)$
34	24 25 30 32 33	syl22anc	$⊢ ((φ \land n \in ℕ) \land k \in X) \to [A + (\frac{1}{n}), B) \subseteq (A, B)$
35	22 34	ixpssixp	$⊢ (φ \land n \in ℕ) \to \underset{k \in X}{⨉} [A + (\frac{1}{n}), B) \subseteq \underset{k \in X}{⨉} (A, B)$
36	35	ralrimiva	$⊢ φ \to \forall n \in ℕ \underset{k \in X}{⨉} [A + (\frac{1}{n}), B) \subseteq \underset{k \in X}{⨉} (A, B)$
37		iunss	$⊢ ⋃_{n \in ℕ} \underset{k \in X}{⨉} [A + (\frac{1}{n}), B) \subseteq \underset{k \in X}{⨉} (A, B) \leftrightarrow \forall n \in ℕ \underset{k \in X}{⨉} [A + (\frac{1}{n}), B) \subseteq \underset{k \in X}{⨉} (A, B)$
38	36 37	sylibr	$⊢ φ \to ⋃_{n \in ℕ} \underset{k \in X}{⨉} [A + (\frac{1}{n}), B) \subseteq \underset{k \in X}{⨉} (A, B)$
39	38	adantr	$⊢ (φ \land \neg X = \emptyset) \to ⋃_{n \in ℕ} \underset{k \in X}{⨉} [A + (\frac{1}{n}), B) \subseteq \underset{k \in X}{⨉} (A, B)$
40		nfv	$⊢ Ⅎ k \neg X = \emptyset$
41	1 40	nfan	$⊢ Ⅎ k (φ \land \neg X = \emptyset)$
42		nfcv	$⊢ \underline{Ⅎ} k f$
43		nfixp1	$⊢ \underline{Ⅎ} k \underset{k \in X}{⨉} (A, B)$
44	42 43	nfel	$⊢ Ⅎ k f \in \underset{k \in X}{⨉} (A, B)$
45	41 44	nfan	$⊢ Ⅎ k ((φ \land \neg X = \emptyset) \land f \in \underset{k \in X}{⨉} (A, B))$
46	2	ad2antrr	$⊢ ((φ \land \neg X = \emptyset) \land f \in \underset{k \in X}{⨉} (A, B)) \to X \in Fin$
47		neqne	$⊢ \neg X = \emptyset \to X \neq \emptyset$
48	47	ad2antlr	$⊢ ((φ \land \neg X = \emptyset) \land f \in \underset{k \in X}{⨉} (A, B)) \to X \neq \emptyset$
49	3	ad4ant14	$⊢ (((φ \land \neg X = \emptyset) \land f \in \underset{k \in X}{⨉} (A, B)) \land k \in X) \to A \in ℝ$
50	4	ad4ant14	$⊢ (((φ \land \neg X = \emptyset) \land f \in \underset{k \in X}{⨉} (A, B)) \land k \in X) \to B \in ℝ^{*}$
51		simpr	$⊢ ((φ \land \neg X = \emptyset) \land f \in \underset{k \in X}{⨉} (A, B)) \to f \in \underset{k \in X}{⨉} (A, B)$
52		eqid	$⊢ sup (ran (k \in X ⟼ f (k) - A) ℝ <) = sup (ran (k \in X ⟼ f (k) - A) ℝ <)$
53	45 46 48 49 50 51 52	iunhoiioolem	$⊢ ((φ \land \neg X = \emptyset) \land f \in \underset{k \in X}{⨉} (A, B)) \to f \in ⋃_{n \in ℕ} \underset{k \in X}{⨉} [A + (\frac{1}{n}), B)$
54	39 53	eqelssd	$⊢ (φ \land \neg X = \emptyset) \to ⋃_{n \in ℕ} \underset{k \in X}{⨉} [A + (\frac{1}{n}), B) = \underset{k \in X}{⨉} (A, B)$
55	20 54	pm2.61dan	$⊢ φ \to ⋃_{n \in ℕ} \underset{k \in X}{⨉} [A + (\frac{1}{n}), B) = \underset{k \in X}{⨉} (A, B)$

Metamath Proof Explorer

Theorem iunhoiioo

Proof