iunhoiioolem

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

	Ref	Expression
Hypotheses	iunhoiioolem.K	$⊢ Ⅎ k φ$
	iunhoiioolem.x	$⊢ φ \to X \in Fin$
	iunhoiioolem.n	$⊢ φ \to X \neq \emptyset$
	iunhoiioolem.a	$⊢ (φ \land k \in X) \to A \in ℝ$
	iunhoiioolem.b	$⊢ (φ \land k \in X) \to B \in ℝ^{*}$
	iunhoiioolem.f	$⊢ φ \to F \in \underset{k \in X}{⨉} (A, B)$
	iunhoiioolem.c	$⊢ C = sup (ran (k \in X ⟼ F (k) - A) ℝ <)$
Assertion	iunhoiioolem	$⊢ φ \to F \in ⋃_{n \in ℕ} \underset{k \in X}{⨉} [A + (\frac{1}{n}), B)$

Proof

Step	Hyp	Ref	Expression
1		iunhoiioolem.K	$⊢ Ⅎ k φ$
2		iunhoiioolem.x	$⊢ φ \to X \in Fin$
3		iunhoiioolem.n	$⊢ φ \to X \neq \emptyset$
4		iunhoiioolem.a	$⊢ (φ \land k \in X) \to A \in ℝ$
5		iunhoiioolem.b	$⊢ (φ \land k \in X) \to B \in ℝ^{*}$
6		iunhoiioolem.f	$⊢ φ \to F \in \underset{k \in X}{⨉} (A, B)$
7		iunhoiioolem.c	$⊢ C = sup (ran (k \in X ⟼ F (k) - A) ℝ <)$
8		eqid	$⊢ (k \in X ⟼ F (k) - A) = (k \in X ⟼ F (k) - A)$
9		ixpf	$⊢ F \in \underset{k \in X}{⨉} (A, B) \to F : X ⟶ ⋃_{k \in X} (A, B)$
10	6 9	syl	$⊢ φ \to F : X ⟶ ⋃_{k \in X} (A, B)$
11		ioossre	$⊢ (A, B) \subseteq ℝ$
12	11	rgenw	$⊢ \forall k \in X (A, B) \subseteq ℝ$
13	12	a1i	$⊢ φ \to \forall k \in X (A, B) \subseteq ℝ$
14		iunss	$⊢ ⋃_{k \in X} (A, B) \subseteq ℝ \leftrightarrow \forall k \in X (A, B) \subseteq ℝ$
15	13 14	sylibr	$⊢ φ \to ⋃_{k \in X} (A, B) \subseteq ℝ$
16	10 15	fssd	$⊢ φ \to F : X ⟶ ℝ$
17	16	ffvelrnda	$⊢ (φ \land k \in X) \to F (k) \in ℝ$
18	17 4	resubcld	$⊢ (φ \land k \in X) \to F (k) - A \in ℝ$
19	4	rexrd	$⊢ (φ \land k \in X) \to A \in ℝ^{*}$
20	6	adantr	$⊢ (φ \land k \in X) \to F \in \underset{k \in X}{⨉} (A, B)$
21		simpr	$⊢ (φ \land k \in X) \to k \in X$
22		fvixp2	$⊢ (F \in \underset{k \in X}{⨉} (A, B) \land k \in X) \to F (k) \in (A, B)$
23	20 21 22	syl2anc	$⊢ (φ \land k \in X) \to F (k) \in (A, B)$
24		ioogtlb	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land F (k) \in (A, B)) \to A < F (k)$
25	19 5 23 24	syl3anc	$⊢ (φ \land k \in X) \to A < F (k)$
26	4 17	posdifd	$⊢ (φ \land k \in X) \to (A < F (k) \leftrightarrow 0 < F (k) - A)$
27	25 26	mpbid	$⊢ (φ \land k \in X) \to 0 < F (k) - A$
28	18 27	elrpd	$⊢ (φ \land k \in X) \to F (k) - A \in ℝ^{+}$
29	1 8 28	rnmptssd	$⊢ φ \to ran (k \in X ⟼ F (k) - A) \subseteq ℝ^{+}$
30		ltso	$⊢ < Or ℝ$
31	30	a1i	$⊢ φ \to < Or ℝ$
32	8	rnmptfi	$⊢ X \in Fin \to ran (k \in X ⟼ F (k) - A) \in Fin$
33	2 32	syl	$⊢ φ \to ran (k \in X ⟼ F (k) - A) \in Fin$
34	1 28 8 3	rnmptn0	$⊢ φ \to ran (k \in X ⟼ F (k) - A) \neq \emptyset$
35	1 8 18	rnmptssd	$⊢ φ \to ran (k \in X ⟼ F (k) - A) \subseteq ℝ$
36		fiinfcl	$⊢ (< Or ℝ \land (ran (k \in X ⟼ F (k) - A) \in Fin \land ran (k \in X ⟼ F (k) - A) \neq \emptyset \land ran (k \in X ⟼ F (k) - A) \subseteq ℝ)) \to sup (ran (k \in X ⟼ F (k) - A) ℝ <) \in ran (k \in X ⟼ F (k) - A)$
37	31 33 34 35 36	syl13anc	$⊢ φ \to sup (ran (k \in X ⟼ F (k) - A) ℝ <) \in ran (k \in X ⟼ F (k) - A)$
38	7 37	eqeltrid	$⊢ φ \to C \in ran (k \in X ⟼ F (k) - A)$
39	29 38	sseldd	$⊢ φ \to C \in ℝ^{+}$
40		rpgtrecnn	$⊢ C \in ℝ^{+} \to \exists n \in ℕ \frac{1}{n} < C$
41	39 40	syl	$⊢ φ \to \exists n \in ℕ \frac{1}{n} < C$
42	6	elexd	$⊢ φ \to F \in V$
43	42	ad2antrr	$⊢ ((φ \land n \in ℕ) \land \frac{1}{n} < C) \to F \in V$
44	10	ffnd	$⊢ φ \to F Fn X$
45	44	ad2antrr	$⊢ ((φ \land n \in ℕ) \land \frac{1}{n} < C) \to F Fn X$
46		nfv	$⊢ Ⅎ k n \in ℕ$
47	1 46	nfan	$⊢ Ⅎ k (φ \land n \in ℕ)$
48		nfcv	$⊢ \underline{Ⅎ} k (\frac{1}{n})$
49		nfcv	$⊢ \underline{Ⅎ} k <$
50		nfmpt1	$⊢ \underline{Ⅎ} k (k \in X ⟼ F (k) - A)$
51	50	nfrn	$⊢ \underline{Ⅎ} k ran (k \in X ⟼ F (k) - A)$
52		nfcv	$⊢ \underline{Ⅎ} k ℝ$
53	51 52 49	nfinf	$⊢ \underline{Ⅎ} k sup (ran (k \in X ⟼ F (k) - A) ℝ <)$
54	7 53	nfcxfr	$⊢ \underline{Ⅎ} k C$
55	48 49 54	nfbr	$⊢ Ⅎ k \frac{1}{n} < C$
56	47 55	nfan	$⊢ Ⅎ k ((φ \land n \in ℕ) \land \frac{1}{n} < C)$
57	4	adantlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to A \in ℝ$
58		nnrecre	$⊢ n \in ℕ \to \frac{1}{n} \in ℝ$
59	58	ad2antlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to \frac{1}{n} \in ℝ$
60	57 59	readdcld	$⊢ ((φ \land n \in ℕ) \land k \in X) \to A + (\frac{1}{n}) \in ℝ$
61	60	rexrd	$⊢ ((φ \land n \in ℕ) \land k \in X) \to A + (\frac{1}{n}) \in ℝ^{*}$
62	61	adantlr	$⊢ (((φ \land n \in ℕ) \land \frac{1}{n} < C) \land k \in X) \to A + (\frac{1}{n}) \in ℝ^{*}$
63	5	adantlr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to B \in ℝ^{*}$
64	63	adantlr	$⊢ (((φ \land n \in ℕ) \land \frac{1}{n} < C) \land k \in X) \to B \in ℝ^{*}$
65		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
66	65	a1i	$⊢ φ \to ℝ \subseteq ℝ^{*}$
67	16 66	fssd	$⊢ φ \to F : X ⟶ ℝ^{*}$
68	67	ad2antrr	$⊢ ((φ \land n \in ℕ) \land \frac{1}{n} < C) \to F : X ⟶ ℝ^{*}$
69	68	ffvelrnda	$⊢ (((φ \land n \in ℕ) \land \frac{1}{n} < C) \land k \in X) \to F (k) \in ℝ^{*}$
70	60	adantlr	$⊢ (((φ \land n \in ℕ) \land \frac{1}{n} < C) \land k \in X) \to A + (\frac{1}{n}) \in ℝ$
71	17	ad4ant14	$⊢ (((φ \land n \in ℕ) \land \frac{1}{n} < C) \land k \in X) \to F (k) \in ℝ$
72	59	adantlr	$⊢ (((φ \land n \in ℕ) \land \frac{1}{n} < C) \land k \in X) \to \frac{1}{n} \in ℝ$
73	35 38	sseldd	$⊢ φ \to C \in ℝ$
74	73	ad3antrrr	$⊢ (((φ \land n \in ℕ) \land \frac{1}{n} < C) \land k \in X) \to C \in ℝ$
75	18	ad4ant14	$⊢ (((φ \land n \in ℕ) \land \frac{1}{n} < C) \land k \in X) \to F (k) - A \in ℝ$
76		simplr	$⊢ (((φ \land n \in ℕ) \land \frac{1}{n} < C) \land k \in X) \to \frac{1}{n} < C$
77	35	ad2antrr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to ran (k \in X ⟼ F (k) - A) \subseteq ℝ$
78	33	ad2antrr	$⊢ ((φ \land n \in ℕ) \land k \in X) \to ran (k \in X ⟼ F (k) - A) \in Fin$
79		id	$⊢ k \in X \to k \in X$
80		ovexd	$⊢ k \in X \to F (k) - A \in V$
81	8	elrnmpt1	$⊢ (k \in X \land F (k) - A \in V) \to F (k) - A \in ran (k \in X ⟼ F (k) - A)$
82	79 80 81	syl2anc	$⊢ k \in X \to F (k) - A \in ran (k \in X ⟼ F (k) - A)$
83	82	adantl	$⊢ ((φ \land n \in ℕ) \land k \in X) \to F (k) - A \in ran (k \in X ⟼ F (k) - A)$
84		infrefilb	$⊢ (ran (k \in X ⟼ F (k) - A) \subseteq ℝ \land ran (k \in X ⟼ F (k) - A) \in Fin \land F (k) - A \in ran (k \in X ⟼ F (k) - A)) \to sup (ran (k \in X ⟼ F (k) - A) ℝ <) \leq F (k) - A$
85	77 78 83 84	syl3anc	$⊢ ((φ \land n \in ℕ) \land k \in X) \to sup (ran (k \in X ⟼ F (k) - A) ℝ <) \leq F (k) - A$
86	7 85	eqbrtrid	$⊢ ((φ \land n \in ℕ) \land k \in X) \to C \leq F (k) - A$
87	86	adantlr	$⊢ (((φ \land n \in ℕ) \land \frac{1}{n} < C) \land k \in X) \to C \leq F (k) - A$
88	72 74 75 76 87	ltletrd	$⊢ (((φ \land n \in ℕ) \land \frac{1}{n} < C) \land k \in X) \to \frac{1}{n} < F (k) - A$
89	57	adantlr	$⊢ (((φ \land n \in ℕ) \land \frac{1}{n} < C) \land k \in X) \to A \in ℝ$
90	89 72 71	ltaddsub2d	$⊢ (((φ \land n \in ℕ) \land \frac{1}{n} < C) \land k \in X) \to (A + (\frac{1}{n}) < F (k) \leftrightarrow \frac{1}{n} < F (k) - A)$
91	88 90	mpbird	$⊢ (((φ \land n \in ℕ) \land \frac{1}{n} < C) \land k \in X) \to A + (\frac{1}{n}) < F (k)$
92	70 71 91	ltled	$⊢ (((φ \land n \in ℕ) \land \frac{1}{n} < C) \land k \in X) \to A + (\frac{1}{n}) \leq F (k)$
93		iooltub	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land F (k) \in (A, B)) \to F (k) < B$
94	19 5 23 93	syl3anc	$⊢ (φ \land k \in X) \to F (k) < B$
95	94	ad4ant14	$⊢ (((φ \land n \in ℕ) \land \frac{1}{n} < C) \land k \in X) \to F (k) < B$
96	62 64 69 92 95	elicod	$⊢ (((φ \land n \in ℕ) \land \frac{1}{n} < C) \land k \in X) \to F (k) \in [A + (\frac{1}{n}), B)$
97	96	ex	$⊢ ((φ \land n \in ℕ) \land \frac{1}{n} < C) \to (k \in X \to F (k) \in [A + (\frac{1}{n}), B))$
98	56 97	ralrimi	$⊢ ((φ \land n \in ℕ) \land \frac{1}{n} < C) \to \forall k \in X F (k) \in [A + (\frac{1}{n}), B)$
99	43 45 98	3jca	$⊢ ((φ \land n \in ℕ) \land \frac{1}{n} < C) \to (F \in V \land F Fn X \land \forall k \in X F (k) \in [A + (\frac{1}{n}), B))$
100		elixp2	$⊢ F \in \underset{k \in X}{⨉} [A + (\frac{1}{n}), B) \leftrightarrow (F \in V \land F Fn X \land \forall k \in X F (k) \in [A + (\frac{1}{n}), B))$
101	99 100	sylibr	$⊢ ((φ \land n \in ℕ) \land \frac{1}{n} < C) \to F \in \underset{k \in X}{⨉} [A + (\frac{1}{n}), B)$
102	101	ex	$⊢ (φ \land n \in ℕ) \to (\frac{1}{n} < C \to F \in \underset{k \in X}{⨉} [A + (\frac{1}{n}), B))$
103	102	reximdva	$⊢ φ \to (\exists n \in ℕ \frac{1}{n} < C \to \exists n \in ℕ F \in \underset{k \in X}{⨉} [A + (\frac{1}{n}), B))$
104	41 103	mpd	$⊢ φ \to \exists n \in ℕ F \in \underset{k \in X}{⨉} [A + (\frac{1}{n}), B)$
105		eliun	$⊢ F \in ⋃_{n \in ℕ} \underset{k \in X}{⨉} [A + (\frac{1}{n}), B) \leftrightarrow \exists n \in ℕ F \in \underset{k \in X}{⨉} [A + (\frac{1}{n}), B)$
106	104 105	sylibr	$⊢ φ \to F \in ⋃_{n \in ℕ} \underset{k \in X}{⨉} [A + (\frac{1}{n}), B)$

Metamath Proof Explorer

Theorem iunhoiioolem

Proof