hoicvr

Description: I is a countable set of half-open intervals that covers the whole multidimensional reals. See Definition 1135 (b) of Fremlin1 p. 29. (Contributed by Glauco Siliprandi, 11-Oct-2020) Avoid ax-rep and shorten proof. (Revised by GG, 2-Apr-2026)

	Ref	Expression
Hypotheses	hoicvr.2	$⊢ I = (j \in ℕ ⟼ (x \in X ⟼ ⟨- j, j⟩))$
	hoicvr.3	$⊢ φ \to X \in Fin$
Assertion	hoicvr	$⊢ φ \to ℝ^{X} \subseteq ⋃_{j \in ℕ} \underset{i \in X}{⨉} ([.) \circ I (j)) (i)$

Proof

Step	Hyp	Ref	Expression
1		hoicvr.2	$⊢ I = (j \in ℕ ⟼ (x \in X ⟼ ⟨- j, j⟩))$
2		hoicvr.3	$⊢ φ \to X \in Fin$
3		reex	$⊢ ℝ \in V$
4		mapdm0	$⊢ ℝ \in V \to ℝ^{\emptyset} = \{\emptyset\}$
5	3 4	ax-mp	$⊢ ℝ^{\emptyset} = \{\emptyset\}$
6		oveq2	$⊢ X = \emptyset \to ℝ^{X} = ℝ^{\emptyset}$
7		ixpeq1	$⊢ X = \emptyset \to \underset{i \in X}{⨉} ([.) \circ I (j)) (i) = \underset{i \in \emptyset}{⨉} ([.) \circ I (j)) (i)$
8	7	iuneq2d	$⊢ X = \emptyset \to ⋃_{j \in ℕ} \underset{i \in X}{⨉} ([.) \circ I (j)) (i) = ⋃_{j \in ℕ} \underset{i \in \emptyset}{⨉} ([.) \circ I (j)) (i)$
9		ixp0x	$⊢ \underset{i \in \emptyset}{⨉} ([.) \circ I (j)) (i) = \{\emptyset\}$
10	9	a1i	$⊢ j \in ℕ \to \underset{i \in \emptyset}{⨉} ([.) \circ I (j)) (i) = \{\emptyset\}$
11	10	iuneq2i	$⊢ ⋃_{j \in ℕ} \underset{i \in \emptyset}{⨉} ([.) \circ I (j)) (i) = ⋃_{j \in ℕ} \{\emptyset\}$
12		nnn0	$⊢ ℕ \neq \emptyset$
13		iunconst	$⊢ ℕ \neq \emptyset \to ⋃_{j \in ℕ} \{\emptyset\} = \{\emptyset\}$
14	12 13	ax-mp	$⊢ ⋃_{j \in ℕ} \{\emptyset\} = \{\emptyset\}$
15	11 14	eqtri	$⊢ ⋃_{j \in ℕ} \underset{i \in \emptyset}{⨉} ([.) \circ I (j)) (i) = \{\emptyset\}$
16	8 15	eqtrdi	$⊢ X = \emptyset \to ⋃_{j \in ℕ} \underset{i \in X}{⨉} ([.) \circ I (j)) (i) = \{\emptyset\}$
17	5 6 16	3eqtr4a	$⊢ X = \emptyset \to ℝ^{X} = ⋃_{j \in ℕ} \underset{i \in X}{⨉} ([.) \circ I (j)) (i)$
18	17	eqimssd	$⊢ X = \emptyset \to ℝ^{X} \subseteq ⋃_{j \in ℕ} \underset{i \in X}{⨉} ([.) \circ I (j)) (i)$
19	18	adantl	$⊢ (φ \land X = \emptyset) \to ℝ^{X} \subseteq ⋃_{j \in ℕ} \underset{i \in X}{⨉} ([.) \circ I (j)) (i)$
20		elmapi	$⊢ f \in (ℝ^{X}) \to f : X ⟶ ℝ$
21	20	adantl	$⊢ (φ \land f \in (ℝ^{X})) \to f : X ⟶ ℝ$
22	21	ffnd	$⊢ (φ \land f \in (ℝ^{X})) \to f Fn X$
23	22	ad3antrrr	$⊢ ((((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \land j \in ℕ) \land sup (ran (abs \circ f) ℝ <) < j) \to f Fn X$
24		simplll	$⊢ ((((φ \land f \in (ℝ^{X})) \land j \in ℕ) \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to (φ \land f \in (ℝ^{X}))$
25		simpllr	$⊢ ((((φ \land f \in (ℝ^{X})) \land j \in ℕ) \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to j \in ℕ$
26		simplr	$⊢ ((((φ \land f \in (ℝ^{X})) \land j \in ℕ) \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to sup (ran (abs \circ f) ℝ <) < j$
27		simpr	$⊢ ((((φ \land f \in (ℝ^{X})) \land j \in ℕ) \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to i \in X$
28		nnnegz	$⊢ j \in ℕ \to - j \in ℤ$
29	28	zxrd	$⊢ j \in ℕ \to - j \in ℝ^{*}$
30	29	adantr	$⊢ (j \in ℕ \land i \in X) \to - j \in ℝ^{*}$
31	30	3ad2antl2	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to - j \in ℝ^{*}$
32		nnxr	$⊢ j \in ℕ \to j \in ℝ^{*}$
33	32	adantr	$⊢ (j \in ℕ \land i \in X) \to j \in ℝ^{*}$
34	33	3ad2antl2	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to j \in ℝ^{*}$
35	20	3ad2ant1	$⊢ (f \in (ℝ^{X}) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \to f : X ⟶ ℝ$
36	35	frexr	$⊢ (f \in (ℝ^{X}) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \to f : X ⟶ ℝ^{*}$
37	36	3adant1l	$⊢ ((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \to f : X ⟶ ℝ^{*}$
38	37	ffvelcdmda	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to f (i) \in ℝ^{*}$
39		nnre	$⊢ j \in ℕ \to j \in ℝ$
40	39	adantr	$⊢ (j \in ℕ \land i \in X) \to j \in ℝ$
41	40	3ad2antl2	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to j \in ℝ$
42	41	renegcld	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to - j \in ℝ$
43	21	ffvelcdmda	$⊢ ((φ \land f \in (ℝ^{X})) \land i \in X) \to f (i) \in ℝ$
44	43	3ad2antl1	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to f (i) \in ℝ$
45	44	renegcld	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to - f (i) \in ℝ$
46		n0i	$⊢ i \in X \to \neg X = \emptyset$
47		rncoss	$⊢ ran (abs \circ f) \subseteq ran abs$
48		absf	$⊢ abs : ℂ ⟶ ℝ$
49		frn	$⊢ abs : ℂ ⟶ ℝ \to ran abs \subseteq ℝ$
50	48 49	ax-mp	$⊢ ran abs \subseteq ℝ$
51	47 50	sstri	$⊢ ran (abs \circ f) \subseteq ℝ$
52		ltso	$⊢ < Or ℝ$
53	52	a1i	$⊢ ((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \to < Or ℝ$
54	48	a1i	$⊢ (φ \land f \in (ℝ^{X})) \to abs : ℂ ⟶ ℝ$
55		ax-resscn	$⊢ ℝ \subseteq ℂ$
56	55	a1i	$⊢ (φ \land f \in (ℝ^{X})) \to ℝ \subseteq ℂ$
57	54 56 21	fcoss	$⊢ (φ \land f \in (ℝ^{X})) \to (abs \circ f) : X ⟶ ℝ$
58	2	adantr	$⊢ (φ \land f \in (ℝ^{X})) \to X \in Fin$
59		rnffi	$⊢ ((abs \circ f) : X ⟶ ℝ \land X \in Fin) \to ran (abs \circ f) \in Fin$
60	57 58 59	syl2anc	$⊢ (φ \land f \in (ℝ^{X})) \to ran (abs \circ f) \in Fin$
61	60	adantr	$⊢ ((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \to ran (abs \circ f) \in Fin$
62	20	frnd	$⊢ f \in (ℝ^{X}) \to ran f \subseteq ℝ$
63	48	fdmi	$⊢ dom abs = ℂ$
64	63	eqcomi	$⊢ ℂ = dom abs$
65	55 64	sseqtri	$⊢ ℝ \subseteq dom abs$
66	62 65	sstrdi	$⊢ f \in (ℝ^{X}) \to ran f \subseteq dom abs$
67		dmcosseq	$⊢ ran f \subseteq dom abs \to dom (abs \circ f) = dom f$
68	66 67	syl	$⊢ f \in (ℝ^{X}) \to dom (abs \circ f) = dom f$
69	20	fdmd	$⊢ f \in (ℝ^{X}) \to dom f = X$
70	68 69	eqtrd	$⊢ f \in (ℝ^{X}) \to dom (abs \circ f) = X$
71	70	adantr	$⊢ (f \in (ℝ^{X}) \land \neg X = \emptyset) \to dom (abs \circ f) = X$
72		neqne	$⊢ \neg X = \emptyset \to X \neq \emptyset$
73	72	adantl	$⊢ (f \in (ℝ^{X}) \land \neg X = \emptyset) \to X \neq \emptyset$
74	71 73	eqnetrd	$⊢ (f \in (ℝ^{X}) \land \neg X = \emptyset) \to dom (abs \circ f) \neq \emptyset$
75	74	neneqd	$⊢ (f \in (ℝ^{X}) \land \neg X = \emptyset) \to \neg dom (abs \circ f) = \emptyset$
76		dm0rn0	$⊢ dom (abs \circ f) = \emptyset \leftrightarrow ran (abs \circ f) = \emptyset$
77	75 76	sylnib	$⊢ (f \in (ℝ^{X}) \land \neg X = \emptyset) \to \neg ran (abs \circ f) = \emptyset$
78	77	neqned	$⊢ (f \in (ℝ^{X}) \land \neg X = \emptyset) \to ran (abs \circ f) \neq \emptyset$
79	78	adantll	$⊢ ((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \to ran (abs \circ f) \neq \emptyset$
80	51	a1i	$⊢ ((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \to ran (abs \circ f) \subseteq ℝ$
81		fisupcl	$⊢ (< Or ℝ \land (ran (abs \circ f) \in Fin \land ran (abs \circ f) \neq \emptyset \land ran (abs \circ f) \subseteq ℝ)) \to sup (ran (abs \circ f) ℝ <) \in ran (abs \circ f)$
82	53 61 79 80 81	syl13anc	$⊢ ((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \to sup (ran (abs \circ f) ℝ <) \in ran (abs \circ f)$
83	51 82	sselid	$⊢ ((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \to sup (ran (abs \circ f) ℝ <) \in ℝ$
84	46 83	sylan2	$⊢ ((φ \land f \in (ℝ^{X})) \land i \in X) \to sup (ran (abs \circ f) ℝ <) \in ℝ$
85	84	3ad2antl1	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to sup (ran (abs \circ f) ℝ <) \in ℝ$
86	20	ffvelcdmda	$⊢ (f \in (ℝ^{X}) \land i \in X) \to f (i) \in ℝ$
87	86	recnd	$⊢ (f \in (ℝ^{X}) \land i \in X) \to f (i) \in ℂ$
88	87	abscld	$⊢ (f \in (ℝ^{X}) \land i \in X) \to \|f (i)\| \in ℝ$
89	88	adantll	$⊢ ((φ \land f \in (ℝ^{X})) \land i \in X) \to \|f (i)\| \in ℝ$
90	89	3ad2antl1	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to \|f (i)\| \in ℝ$
91	86	renegcld	$⊢ (f \in (ℝ^{X}) \land i \in X) \to - f (i) \in ℝ$
92	91	leabsd	$⊢ (f \in (ℝ^{X}) \land i \in X) \to - f (i) \leq \|- f (i)\|$
93	87	absnegd	$⊢ (f \in (ℝ^{X}) \land i \in X) \to \|- f (i)\| = \|f (i)\|$
94	92 93	breqtrd	$⊢ (f \in (ℝ^{X}) \land i \in X) \to - f (i) \leq \|f (i)\|$
95	94	adantll	$⊢ ((φ \land f \in (ℝ^{X})) \land i \in X) \to - f (i) \leq \|f (i)\|$
96	95	3ad2antl1	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to - f (i) \leq \|f (i)\|$
97	51	a1i	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to ran (abs \circ f) \subseteq ℝ$
98	46 79	sylan2	$⊢ ((φ \land f \in (ℝ^{X})) \land i \in X) \to ran (abs \circ f) \neq \emptyset$
99	98	3ad2antl1	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to ran (abs \circ f) \neq \emptyset$
100		fimaxre2	$⊢ (ran (abs \circ f) \subseteq ℝ \land ran (abs \circ f) \in Fin) \to \exists y \in ℝ \forall z \in ran (abs \circ f) z \leq y$
101	51 60 100	sylancr	$⊢ (φ \land f \in (ℝ^{X})) \to \exists y \in ℝ \forall z \in ran (abs \circ f) z \leq y$
102	101	adantr	$⊢ ((φ \land f \in (ℝ^{X})) \land i \in X) \to \exists y \in ℝ \forall z \in ran (abs \circ f) z \leq y$
103	102	3ad2antl1	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to \exists y \in ℝ \forall z \in ran (abs \circ f) z \leq y$
104		elmapfun	$⊢ f \in (ℝ^{X}) \to Fun f$
105		simpr	$⊢ (f \in (ℝ^{X}) \land i \in X) \to i \in X$
106	69	eqcomd	$⊢ f \in (ℝ^{X}) \to X = dom f$
107	106	adantr	$⊢ (f \in (ℝ^{X}) \land i \in X) \to X = dom f$
108	105 107	eleqtrd	$⊢ (f \in (ℝ^{X}) \land i \in X) \to i \in dom f$
109		fvco	$⊢ (Fun f \land i \in dom f) \to (abs \circ f) (i) = \|f (i)\|$
110	104 108 109	syl2an2r	$⊢ (f \in (ℝ^{X}) \land i \in X) \to (abs \circ f) (i) = \|f (i)\|$
111		absfun	$⊢ Fun abs$
112		funco	$⊢ (Fun abs \land Fun f) \to Fun (abs \circ f)$
113	111 104 112	sylancr	$⊢ f \in (ℝ^{X}) \to Fun (abs \circ f)$
114	87 64	eleqtrdi	$⊢ (f \in (ℝ^{X}) \land i \in X) \to f (i) \in dom abs$
115		dmfco	$⊢ (Fun f \land i \in dom f) \to (i \in dom (abs \circ f) \leftrightarrow f (i) \in dom abs)$
116	104 108 115	syl2an2r	$⊢ (f \in (ℝ^{X}) \land i \in X) \to (i \in dom (abs \circ f) \leftrightarrow f (i) \in dom abs)$
117	114 116	mpbird	$⊢ (f \in (ℝ^{X}) \land i \in X) \to i \in dom (abs \circ f)$
118		fvelrn	$⊢ (Fun (abs \circ f) \land i \in dom (abs \circ f)) \to (abs \circ f) (i) \in ran (abs \circ f)$
119	113 117 118	syl2an2r	$⊢ (f \in (ℝ^{X}) \land i \in X) \to (abs \circ f) (i) \in ran (abs \circ f)$
120	110 119	eqeltrrd	$⊢ (f \in (ℝ^{X}) \land i \in X) \to \|f (i)\| \in ran (abs \circ f)$
121	120	adantll	$⊢ ((φ \land f \in (ℝ^{X})) \land i \in X) \to \|f (i)\| \in ran (abs \circ f)$
122	121	3ad2antl1	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to \|f (i)\| \in ran (abs \circ f)$
123	97 99 103 122	suprubd	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to \|f (i)\| \leq sup (ran (abs \circ f) ℝ <)$
124	45 90 85 96 123	letrd	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to - f (i) \leq sup (ran (abs \circ f) ℝ <)$
125		simpl3	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to sup (ran (abs \circ f) ℝ <) < j$
126	45 85 41 124 125	lelttrd	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to - f (i) < j$
127	44 41 126	ltnegcon1d	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to - j < f (i)$
128	42 44 127	ltled	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to - j \leq f (i)$
129	44	leabsd	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to f (i) \leq \|f (i)\|$
130	44 90 85 129 123	letrd	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to f (i) \leq sup (ran (abs \circ f) ℝ <)$
131	44 85 41 130 125	lelttrd	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to f (i) < j$
132	31 34 38 128 131	elicod	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to f (i) \in [- j, j)$
133	24 25 26 27 132	syl31anc	$⊢ ((((φ \land f \in (ℝ^{X})) \land j \in ℕ) \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to f (i) \in [- j, j)$
134	133	adantl3r	$⊢ (((((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \land j \in ℕ) \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to f (i) \in [- j, j)$
135		simpr	$⊢ (φ \land j \in ℕ) \to j \in ℕ$
136		fconstmpt	$⊢ X \times \{⟨- j, j⟩\} = (x \in X ⟼ ⟨- j, j⟩)$
137		snex	$⊢ \{⟨- j, j⟩\} \in V$
138	137	a1i	$⊢ φ \to \{⟨- j, j⟩\} \in V$
139	2 138	xpexd	$⊢ φ \to X \times \{⟨- j, j⟩\} \in V$
140	136 139	eqeltrrid	$⊢ φ \to (x \in X ⟼ ⟨- j, j⟩) \in V$
141	140	adantr	$⊢ (φ \land j \in ℕ) \to (x \in X ⟼ ⟨- j, j⟩) \in V$
142	1	fvmpt2	$⊢ (j \in ℕ \land (x \in X ⟼ ⟨- j, j⟩) \in V) \to I (j) = (x \in X ⟼ ⟨- j, j⟩)$
143	135 141 142	syl2anc	$⊢ (φ \land j \in ℕ) \to I (j) = (x \in X ⟼ ⟨- j, j⟩)$
144	143	fveq1d	$⊢ (φ \land j \in ℕ) \to I (j) (i) = (x \in X ⟼ ⟨- j, j⟩) (i)$
145	144	3adant3	$⊢ (φ \land j \in ℕ \land i \in X) \to I (j) (i) = (x \in X ⟼ ⟨- j, j⟩) (i)$
146		eqidd	$⊢ i \in X \to (x \in X ⟼ ⟨- j, j⟩) = (x \in X ⟼ ⟨- j, j⟩)$
147		eqidd	$⊢ (i \in X \land x = i) \to ⟨- j, j⟩ = ⟨- j, j⟩$
148		id	$⊢ i \in X \to i \in X$
149		opex	$⊢ ⟨- j, j⟩ \in V$
150	149	a1i	$⊢ i \in X \to ⟨- j, j⟩ \in V$
151	146 147 148 150	fvmptd	$⊢ i \in X \to (x \in X ⟼ ⟨- j, j⟩) (i) = ⟨- j, j⟩$
152	151	3ad2ant3	$⊢ (φ \land j \in ℕ \land i \in X) \to (x \in X ⟼ ⟨- j, j⟩) (i) = ⟨- j, j⟩$
153	145 152	eqtrd	$⊢ (φ \land j \in ℕ \land i \in X) \to I (j) (i) = ⟨- j, j⟩$
154	153	fveq2d	$⊢ (φ \land j \in ℕ \land i \in X) \to 1^{st} (I (j) (i)) = 1^{st} (⟨- j, j⟩)$
155		negex	$⊢ - j \in V$
156		vex	$⊢ j \in V$
157	155 156	op1st	$⊢ 1^{st} (⟨- j, j⟩) = - j$
158	154 157	eqtrdi	$⊢ (φ \land j \in ℕ \land i \in X) \to 1^{st} (I (j) (i)) = - j$
159	153	fveq2d	$⊢ (φ \land j \in ℕ \land i \in X) \to 2^{nd} (I (j) (i)) = 2^{nd} (⟨- j, j⟩)$
160	155 156	op2nd	$⊢ 2^{nd} (⟨- j, j⟩) = j$
161	159 160	eqtrdi	$⊢ (φ \land j \in ℕ \land i \in X) \to 2^{nd} (I (j) (i)) = j$
162	158 161	oveq12d	$⊢ (φ \land j \in ℕ \land i \in X) \to [1^{st} (I (j) (i)), 2^{nd} (I (j) (i))) = [- j, j)$
163	162	eqcomd	$⊢ (φ \land j \in ℕ \land i \in X) \to [- j, j) = [1^{st} (I (j) (i)), 2^{nd} (I (j) (i)))$
164	163	3adant1r	$⊢ ((φ \land f \in (ℝ^{X})) \land j \in ℕ \land i \in X) \to [- j, j) = [1^{st} (I (j) (i)), 2^{nd} (I (j) (i)))$
165	164	ad5ant135	$⊢ (((((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \land j \in ℕ) \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to [- j, j) = [1^{st} (I (j) (i)), 2^{nd} (I (j) (i)))$
166	134 165	eleqtrd	$⊢ (((((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \land j \in ℕ) \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to f (i) \in [1^{st} (I (j) (i)), 2^{nd} (I (j) (i)))$
167	28	zred	$⊢ j \in ℕ \to - j \in ℝ$
168	167 39	opelxpd	$⊢ j \in ℕ \to ⟨- j, j⟩ \in ℝ^{2}$
169	168	ad2antlr	$⊢ ((φ \land j \in ℕ) \land x \in X) \to ⟨- j, j⟩ \in ℝ^{2}$
170	143 169	fmpt3d	$⊢ (φ \land j \in ℕ) \to I (j) : X ⟶ ℝ^{2}$
171	170	ad4ant14	$⊢ (((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \land j \in ℕ) \to I (j) : X ⟶ ℝ^{2}$
172	171	ad2antrr	$⊢ (((((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \land j \in ℕ) \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to I (j) : X ⟶ ℝ^{2}$
173		simpr	$⊢ (((((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \land j \in ℕ) \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to i \in X$
174	172 173	fvovco	$⊢ (((((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \land j \in ℕ) \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to ([.) \circ I (j)) (i) = [1^{st} (I (j) (i)), 2^{nd} (I (j) (i)))$
175	166 174	eleqtrrd	$⊢ (((((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \land j \in ℕ) \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to f (i) \in ([.) \circ I (j)) (i)$
176	175	ralrimiva	$⊢ ((((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \land j \in ℕ) \land sup (ran (abs \circ f) ℝ <) < j) \to \forall i \in X f (i) \in ([.) \circ I (j)) (i)$
177		vex	$⊢ f \in V$
178	177	elixp	$⊢ f \in \underset{i \in X}{⨉} ([.) \circ I (j)) (i) \leftrightarrow (f Fn X \land \forall i \in X f (i) \in ([.) \circ I (j)) (i))$
179	23 176 178	sylanbrc	$⊢ ((((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \land j \in ℕ) \land sup (ran (abs \circ f) ℝ <) < j) \to f \in \underset{i \in X}{⨉} ([.) \circ I (j)) (i)$
180	83	archd	$⊢ ((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \to \exists j \in ℕ sup (ran (abs \circ f) ℝ <) < j$
181	179 180	reximddv3	$⊢ ((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \to \exists j \in ℕ f \in \underset{i \in X}{⨉} ([.) \circ I (j)) (i)$
182	181	an32s	$⊢ ((φ \land \neg X = \emptyset) \land f \in (ℝ^{X})) \to \exists j \in ℕ f \in \underset{i \in X}{⨉} ([.) \circ I (j)) (i)$
183	182	eliund	$⊢ ((φ \land \neg X = \emptyset) \land f \in (ℝ^{X})) \to f \in ⋃_{j \in ℕ} \underset{i \in X}{⨉} ([.) \circ I (j)) (i)$
184	183	ssd	$⊢ (φ \land \neg X = \emptyset) \to ℝ^{X} \subseteq ⋃_{j \in ℕ} \underset{i \in X}{⨉} ([.) \circ I (j)) (i)$
185	19 184	pm2.61dan	$⊢ φ \to ℝ^{X} \subseteq ⋃_{j \in ℕ} \underset{i \in X}{⨉} ([.) \circ I (j)) (i)$

Metamath Proof Explorer

Theorem hoicvr

Proof