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)

	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	5	a1i	$⊢ X = \emptyset \to ℝ^{\emptyset} = \{\emptyset\}$
7		oveq2	$⊢ X = \emptyset \to ℝ^{X} = ℝ^{\emptyset}$
8		ixpeq1	$⊢ X = \emptyset \to \underset{i \in X}{⨉} ([.) \circ I (j)) (i) = \underset{i \in \emptyset}{⨉} ([.) \circ I (j)) (i)$
9	8	iuneq2d	$⊢ X = \emptyset \to ⋃_{j \in ℕ} \underset{i \in X}{⨉} ([.) \circ I (j)) (i) = ⋃_{j \in ℕ} \underset{i \in \emptyset}{⨉} ([.) \circ I (j)) (i)$
10		ixp0x	$⊢ \underset{i \in \emptyset}{⨉} ([.) \circ I (j)) (i) = \{\emptyset\}$
11	10	a1i	$⊢ j \in ℕ \to \underset{i \in \emptyset}{⨉} ([.) \circ I (j)) (i) = \{\emptyset\}$
12	11	iuneq2i	$⊢ ⋃_{j \in ℕ} \underset{i \in \emptyset}{⨉} ([.) \circ I (j)) (i) = ⋃_{j \in ℕ} \{\emptyset\}$
13		1nn	$⊢ 1 \in ℕ$
14	13	ne0ii	$⊢ ℕ \neq \emptyset$
15		iunconst	$⊢ ℕ \neq \emptyset \to ⋃_{j \in ℕ} \{\emptyset\} = \{\emptyset\}$
16	14 15	ax-mp	$⊢ ⋃_{j \in ℕ} \{\emptyset\} = \{\emptyset\}$
17	12 16	eqtri	$⊢ ⋃_{j \in ℕ} \underset{i \in \emptyset}{⨉} ([.) \circ I (j)) (i) = \{\emptyset\}$
18	17	a1i	$⊢ X = \emptyset \to ⋃_{j \in ℕ} \underset{i \in \emptyset}{⨉} ([.) \circ I (j)) (i) = \{\emptyset\}$
19	9 18	eqtrd	$⊢ X = \emptyset \to ⋃_{j \in ℕ} \underset{i \in X}{⨉} ([.) \circ I (j)) (i) = \{\emptyset\}$
20	6 7 19	3eqtr4d	$⊢ X = \emptyset \to ℝ^{X} = ⋃_{j \in ℕ} \underset{i \in X}{⨉} ([.) \circ I (j)) (i)$
21		eqimss	$⊢ ℝ^{X} = ⋃_{j \in ℕ} \underset{i \in X}{⨉} ([.) \circ I (j)) (i) \to ℝ^{X} \subseteq ⋃_{j \in ℕ} \underset{i \in X}{⨉} ([.) \circ I (j)) (i)$
22	20 21	syl	$⊢ X = \emptyset \to ℝ^{X} \subseteq ⋃_{j \in ℕ} \underset{i \in X}{⨉} ([.) \circ I (j)) (i)$
23	22	adantl	$⊢ (φ \land X = \emptyset) \to ℝ^{X} \subseteq ⋃_{j \in ℕ} \underset{i \in X}{⨉} ([.) \circ I (j)) (i)$
24		simpll	$⊢ ((φ \land \neg X = \emptyset) \land f \in (ℝ^{X})) \to φ$
25		simpr	$⊢ ((φ \land \neg X = \emptyset) \land f \in (ℝ^{X})) \to f \in (ℝ^{X})$
26		simplr	$⊢ ((φ \land \neg X = \emptyset) \land f \in (ℝ^{X})) \to \neg X = \emptyset$
27		rncoss	$⊢ ran (abs \circ f) \subseteq ran abs$
28		absf	$⊢ abs : ℂ ⟶ ℝ$
29		frn	$⊢ abs : ℂ ⟶ ℝ \to ran abs \subseteq ℝ$
30	28 29	ax-mp	$⊢ ran abs \subseteq ℝ$
31	27 30	sstri	$⊢ ran (abs \circ f) \subseteq ℝ$
32	31	a1i	$⊢ ((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \to ran (abs \circ f) \subseteq ℝ$
33		ltso	$⊢ < Or ℝ$
34	33	a1i	$⊢ ((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \to < Or ℝ$
35	28	a1i	$⊢ (φ \land f \in (ℝ^{X})) \to abs : ℂ ⟶ ℝ$
36		elmapi	$⊢ f \in (ℝ^{X}) \to f : X ⟶ ℝ$
37	36	adantl	$⊢ (φ \land f \in (ℝ^{X})) \to f : X ⟶ ℝ$
38		ax-resscn	$⊢ ℝ \subseteq ℂ$
39	38	a1i	$⊢ (φ \land f \in (ℝ^{X})) \to ℝ \subseteq ℂ$
40	37 39	fssd	$⊢ (φ \land f \in (ℝ^{X})) \to f : X ⟶ ℂ$
41		fco	$⊢ (abs : ℂ ⟶ ℝ \land f : X ⟶ ℂ) \to (abs \circ f) : X ⟶ ℝ$
42	35 40 41	syl2anc	$⊢ (φ \land f \in (ℝ^{X})) \to (abs \circ f) : X ⟶ ℝ$
43	2	adantr	$⊢ (φ \land f \in (ℝ^{X})) \to X \in Fin$
44		rnffi	$⊢ ((abs \circ f) : X ⟶ ℝ \land X \in Fin) \to ran (abs \circ f) \in Fin$
45	42 43 44	syl2anc	$⊢ (φ \land f \in (ℝ^{X})) \to ran (abs \circ f) \in Fin$
46	45	adantr	$⊢ ((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \to ran (abs \circ f) \in Fin$
47	36	frnd	$⊢ f \in (ℝ^{X}) \to ran f \subseteq ℝ$
48	28	fdmi	$⊢ dom abs = ℂ$
49	48	eqcomi	$⊢ ℂ = dom abs$
50	38 49	sseqtri	$⊢ ℝ \subseteq dom abs$
51	50	a1i	$⊢ f \in (ℝ^{X}) \to ℝ \subseteq dom abs$
52	47 51	sstrd	$⊢ f \in (ℝ^{X}) \to ran f \subseteq dom abs$
53		dmcosseq	$⊢ ran f \subseteq dom abs \to dom (abs \circ f) = dom f$
54	52 53	syl	$⊢ f \in (ℝ^{X}) \to dom (abs \circ f) = dom f$
55	36	fdmd	$⊢ f \in (ℝ^{X}) \to dom f = X$
56	54 55	eqtrd	$⊢ f \in (ℝ^{X}) \to dom (abs \circ f) = X$
57	56	adantr	$⊢ (f \in (ℝ^{X}) \land \neg X = \emptyset) \to dom (abs \circ f) = X$
58		neqne	$⊢ \neg X = \emptyset \to X \neq \emptyset$
59	58	adantl	$⊢ (f \in (ℝ^{X}) \land \neg X = \emptyset) \to X \neq \emptyset$
60	57 59	eqnetrd	$⊢ (f \in (ℝ^{X}) \land \neg X = \emptyset) \to dom (abs \circ f) \neq \emptyset$
61	60	neneqd	$⊢ (f \in (ℝ^{X}) \land \neg X = \emptyset) \to \neg dom (abs \circ f) = \emptyset$
62		dm0rn0	$⊢ dom (abs \circ f) = \emptyset \leftrightarrow ran (abs \circ f) = \emptyset$
63	61 62	sylnib	$⊢ (f \in (ℝ^{X}) \land \neg X = \emptyset) \to \neg ran (abs \circ f) = \emptyset$
64	63	neqned	$⊢ (f \in (ℝ^{X}) \land \neg X = \emptyset) \to ran (abs \circ f) \neq \emptyset$
65	64	adantll	$⊢ ((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \to ran (abs \circ f) \neq \emptyset$
66		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)$
67	34 46 65 32 66	syl13anc	$⊢ ((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \to sup (ran (abs \circ f) ℝ <) \in ran (abs \circ f)$
68	32 67	sseldd	$⊢ ((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \to sup (ran (abs \circ f) ℝ <) \in ℝ$
69		arch	$⊢ sup (ran (abs \circ f) ℝ <) \in ℝ \to \exists j \in ℕ sup (ran (abs \circ f) ℝ <) < j$
70	68 69	syl	$⊢ ((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \to \exists j \in ℕ sup (ran (abs \circ f) ℝ <) < j$
71	37	ffnd	$⊢ (φ \land f \in (ℝ^{X})) \to f Fn X$
72	71	ad2antrr	$⊢ (((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \land sup (ran (abs \circ f) ℝ <) < j) \to f Fn X$
73	72	adantlr	$⊢ ((((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \land j \in ℕ) \land sup (ran (abs \circ f) ℝ <) < j) \to f Fn X$
74		simplll	$⊢ ((((φ \land f \in (ℝ^{X})) \land j \in ℕ) \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to (φ \land f \in (ℝ^{X}))$
75		id	$⊢ j \in ℕ \to j \in ℕ$
76	75	ad3antlr	$⊢ ((((φ \land f \in (ℝ^{X})) \land j \in ℕ) \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to j \in ℕ$
77		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$
78		simpr	$⊢ ((((φ \land f \in (ℝ^{X})) \land j \in ℕ) \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to i \in X$
79		simp2	$⊢ ((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \to j \in ℕ$
80		zssre	$⊢ ℤ \subseteq ℝ$
81		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
82	80 81	sstri	$⊢ ℤ \subseteq ℝ^{*}$
83		nnnegz	$⊢ j \in ℕ \to - j \in ℤ$
84	82 83	sselid	$⊢ j \in ℕ \to - j \in ℝ^{*}$
85	84	adantr	$⊢ (j \in ℕ \land i \in X) \to - j \in ℝ^{*}$
86	79 85	sylan	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to - j \in ℝ^{*}$
87	75	nnxrd	$⊢ j \in ℕ \to j \in ℝ^{*}$
88	87	adantr	$⊢ (j \in ℕ \land i \in X) \to j \in ℝ^{*}$
89	79 88	sylan	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to j \in ℝ^{*}$
90	36	3ad2ant1	$⊢ (f \in (ℝ^{X}) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \to f : X ⟶ ℝ$
91	81	a1i	$⊢ (f \in (ℝ^{X}) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \to ℝ \subseteq ℝ^{*}$
92	90 91	fssd	$⊢ (f \in (ℝ^{X}) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \to f : X ⟶ ℝ^{*}$
93	92	3adant1l	$⊢ ((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \to f : X ⟶ ℝ^{*}$
94	93	ffvelcdmda	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to f (i) \in ℝ^{*}$
95		nnre	$⊢ j \in ℕ \to j \in ℝ$
96	95	adantr	$⊢ (j \in ℕ \land i \in X) \to j \in ℝ$
97	96	3ad2antl2	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to j \in ℝ$
98	97	renegcld	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to - j \in ℝ$
99	37	ffvelcdmda	$⊢ ((φ \land f \in (ℝ^{X})) \land i \in X) \to f (i) \in ℝ$
100	99	3ad2antl1	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to f (i) \in ℝ$
101	100	renegcld	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to - f (i) \in ℝ$
102		simpll	$⊢ ((φ \land f \in (ℝ^{X})) \land i \in X) \to φ$
103		simplr	$⊢ ((φ \land f \in (ℝ^{X})) \land i \in X) \to f \in (ℝ^{X})$
104		n0i	$⊢ i \in X \to \neg X = \emptyset$
105	104	adantl	$⊢ ((φ \land f \in (ℝ^{X})) \land i \in X) \to \neg X = \emptyset$
106	102 103 105 68	syl21anc	$⊢ ((φ \land f \in (ℝ^{X})) \land i \in X) \to sup (ran (abs \circ f) ℝ <) \in ℝ$
107	106	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 ℝ$
108	36	ffvelcdmda	$⊢ (f \in (ℝ^{X}) \land i \in X) \to f (i) \in ℝ$
109	38 108	sselid	$⊢ (f \in (ℝ^{X}) \land i \in X) \to f (i) \in ℂ$
110	109	abscld	$⊢ (f \in (ℝ^{X}) \land i \in X) \to \|f (i)\| \in ℝ$
111	110	adantll	$⊢ ((φ \land f \in (ℝ^{X})) \land i \in X) \to \|f (i)\| \in ℝ$
112	111	3ad2antl1	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to \|f (i)\| \in ℝ$
113	108	renegcld	$⊢ (f \in (ℝ^{X}) \land i \in X) \to - f (i) \in ℝ$
114	113	leabsd	$⊢ (f \in (ℝ^{X}) \land i \in X) \to - f (i) \leq \|- f (i)\|$
115	109	absnegd	$⊢ (f \in (ℝ^{X}) \land i \in X) \to \|- f (i)\| = \|f (i)\|$
116	114 115	breqtrd	$⊢ (f \in (ℝ^{X}) \land i \in X) \to - f (i) \leq \|f (i)\|$
117	116	adantll	$⊢ ((φ \land f \in (ℝ^{X})) \land i \in X) \to - f (i) \leq \|f (i)\|$
118	117	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)\|$
119	31	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 ℝ$
120	105 65	syldan	$⊢ ((φ \land f \in (ℝ^{X})) \land i \in X) \to ran (abs \circ f) \neq \emptyset$
121	120	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$
122		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$
123	31 45 122	sylancr	$⊢ (φ \land f \in (ℝ^{X})) \to \exists y \in ℝ \forall z \in ran (abs \circ f) z \leq y$
124	123	adantr	$⊢ ((φ \land f \in (ℝ^{X})) \land i \in X) \to \exists y \in ℝ \forall z \in ran (abs \circ f) z \leq y$
125	124	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$
126		elmapfun	$⊢ f \in (ℝ^{X}) \to Fun f$
127	126	adantr	$⊢ (f \in (ℝ^{X}) \land i \in X) \to Fun f$
128		simpr	$⊢ (f \in (ℝ^{X}) \land i \in X) \to i \in X$
129	55	eqcomd	$⊢ f \in (ℝ^{X}) \to X = dom f$
130	129	adantr	$⊢ (f \in (ℝ^{X}) \land i \in X) \to X = dom f$
131	128 130	eleqtrd	$⊢ (f \in (ℝ^{X}) \land i \in X) \to i \in dom f$
132		fvco	$⊢ (Fun f \land i \in dom f) \to (abs \circ f) (i) = \|f (i)\|$
133	127 131 132	syl2anc	$⊢ (f \in (ℝ^{X}) \land i \in X) \to (abs \circ f) (i) = \|f (i)\|$
134	133	eqcomd	$⊢ (f \in (ℝ^{X}) \land i \in X) \to \|f (i)\| = (abs \circ f) (i)$
135		absfun	$⊢ Fun abs$
136	135	a1i	$⊢ f \in (ℝ^{X}) \to Fun abs$
137		funco	$⊢ (Fun abs \land Fun f) \to Fun (abs \circ f)$
138	136 126 137	syl2anc	$⊢ f \in (ℝ^{X}) \to Fun (abs \circ f)$
139	138	adantr	$⊢ (f \in (ℝ^{X}) \land i \in X) \to Fun (abs \circ f)$
140	109 49	eleqtrdi	$⊢ (f \in (ℝ^{X}) \land i \in X) \to f (i) \in dom abs$
141		dmfco	$⊢ (Fun f \land i \in dom f) \to (i \in dom (abs \circ f) \leftrightarrow f (i) \in dom abs)$
142	127 131 141	syl2anc	$⊢ (f \in (ℝ^{X}) \land i \in X) \to (i \in dom (abs \circ f) \leftrightarrow f (i) \in dom abs)$
143	140 142	mpbird	$⊢ (f \in (ℝ^{X}) \land i \in X) \to i \in dom (abs \circ f)$
144		fvelrn	$⊢ (Fun (abs \circ f) \land i \in dom (abs \circ f)) \to (abs \circ f) (i) \in ran (abs \circ f)$
145	139 143 144	syl2anc	$⊢ (f \in (ℝ^{X}) \land i \in X) \to (abs \circ f) (i) \in ran (abs \circ f)$
146	134 145	eqeltrd	$⊢ (f \in (ℝ^{X}) \land i \in X) \to \|f (i)\| \in ran (abs \circ f)$
147	146	adantll	$⊢ ((φ \land f \in (ℝ^{X})) \land i \in X) \to \|f (i)\| \in ran (abs \circ f)$
148	147	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)$
149		suprub	$⊢ ((ran (abs \circ f) \subseteq ℝ \land ran (abs \circ f) \neq \emptyset \land \exists y \in ℝ \forall z \in ran (abs \circ f) z \leq y) \land \|f (i)\| \in ran (abs \circ f)) \to \|f (i)\| \leq sup (ran (abs \circ f) ℝ <)$
150	119 121 125 148 149	syl31anc	$⊢ (((φ \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) ℝ <)$
151	101 112 107 118 150	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) ℝ <)$
152		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$
153	101 107 97 151 152	lelttrd	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to - f (i) < j$
154	101 97	ltnegd	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to (- f (i) < j \leftrightarrow - j < - (- f (i)))$
155	153 154	mpbid	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to - j < - (- f (i))$
156	38 100	sselid	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to f (i) \in ℂ$
157	156	negnegd	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to - (- f (i)) = f (i)$
158	155 157	breqtrd	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to - j < f (i)$
159	98 100 158	ltled	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to - j \leq f (i)$
160	100	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)\|$
161	100 112 107 160 150	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) ℝ <)$
162	100 107 97 161 152	lelttrd	$⊢ (((φ \land f \in (ℝ^{X})) \land j \in ℕ \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to f (i) < j$
163	86 89 94 159 162	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)$
164	74 76 77 78 163	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)$
165	164	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)$
166		simpr	$⊢ (φ \land j \in ℕ) \to j \in ℕ$
167		mptexg	$⊢ X \in Fin \to (x \in X ⟼ ⟨- j, j⟩) \in V$
168	2 167	syl	$⊢ φ \to (x \in X ⟼ ⟨- j, j⟩) \in V$
169	168	adantr	$⊢ (φ \land j \in ℕ) \to (x \in X ⟼ ⟨- j, j⟩) \in V$
170	1	fvmpt2	$⊢ (j \in ℕ \land (x \in X ⟼ ⟨- j, j⟩) \in V) \to I (j) = (x \in X ⟼ ⟨- j, j⟩)$
171	166 169 170	syl2anc	$⊢ (φ \land j \in ℕ) \to I (j) = (x \in X ⟼ ⟨- j, j⟩)$
172	171	fveq1d	$⊢ (φ \land j \in ℕ) \to I (j) (i) = (x \in X ⟼ ⟨- j, j⟩) (i)$
173	172	3adant3	$⊢ (φ \land j \in ℕ \land i \in X) \to I (j) (i) = (x \in X ⟼ ⟨- j, j⟩) (i)$
174		eqidd	$⊢ i \in X \to (x \in X ⟼ ⟨- j, j⟩) = (x \in X ⟼ ⟨- j, j⟩)$
175		eqid	$⊢ ⟨- j, j⟩ = ⟨- j, j⟩$
176	175	a1i	$⊢ (i \in X \land x = i) \to ⟨- j, j⟩ = ⟨- j, j⟩$
177		id	$⊢ i \in X \to i \in X$
178		opex	$⊢ ⟨- j, j⟩ \in V$
179	178	a1i	$⊢ i \in X \to ⟨- j, j⟩ \in V$
180	174 176 177 179	fvmptd	$⊢ i \in X \to (x \in X ⟼ ⟨- j, j⟩) (i) = ⟨- j, j⟩$
181	180	3ad2ant3	$⊢ (φ \land j \in ℕ \land i \in X) \to (x \in X ⟼ ⟨- j, j⟩) (i) = ⟨- j, j⟩$
182	173 181	eqtrd	$⊢ (φ \land j \in ℕ \land i \in X) \to I (j) (i) = ⟨- j, j⟩$
183	182	fveq2d	$⊢ (φ \land j \in ℕ \land i \in X) \to 1^{st} (I (j) (i)) = 1^{st} (⟨- j, j⟩)$
184		negex	$⊢ - j \in V$
185		vex	$⊢ j \in V$
186	184 185	op1st	$⊢ 1^{st} (⟨- j, j⟩) = - j$
187	186	a1i	$⊢ (φ \land j \in ℕ \land i \in X) \to 1^{st} (⟨- j, j⟩) = - j$
188	183 187	eqtrd	$⊢ (φ \land j \in ℕ \land i \in X) \to 1^{st} (I (j) (i)) = - j$
189	182	fveq2d	$⊢ (φ \land j \in ℕ \land i \in X) \to 2^{nd} (I (j) (i)) = 2^{nd} (⟨- j, j⟩)$
190	184 185	op2nd	$⊢ 2^{nd} (⟨- j, j⟩) = j$
191	190	a1i	$⊢ (φ \land j \in ℕ \land i \in X) \to 2^{nd} (⟨- j, j⟩) = j$
192	189 191	eqtrd	$⊢ (φ \land j \in ℕ \land i \in X) \to 2^{nd} (I (j) (i)) = j$
193	188 192	oveq12d	$⊢ (φ \land j \in ℕ \land i \in X) \to [1^{st} (I (j) (i)), 2^{nd} (I (j) (i))) = [- j, j)$
194	193	eqcomd	$⊢ (φ \land j \in ℕ \land i \in X) \to [- j, j) = [1^{st} (I (j) (i)), 2^{nd} (I (j) (i)))$
195	194	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)))$
196	195	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)))$
197	165 196	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)))$
198	80 83	sselid	$⊢ j \in ℕ \to - j \in ℝ$
199		opelxpi	$⊢ (- j \in ℝ \land j \in ℝ) \to ⟨- j, j⟩ \in ℝ^{2}$
200	198 95 199	syl2anc	$⊢ j \in ℕ \to ⟨- j, j⟩ \in ℝ^{2}$
201	200	ad2antlr	$⊢ ((φ \land j \in ℕ) \land x \in X) \to ⟨- j, j⟩ \in ℝ^{2}$
202		eqid	$⊢ (x \in X ⟼ ⟨- j, j⟩) = (x \in X ⟼ ⟨- j, j⟩)$
203	201 202	fmptd	$⊢ (φ \land j \in ℕ) \to (x \in X ⟼ ⟨- j, j⟩) : X ⟶ ℝ^{2}$
204	171	feq1d	$⊢ (φ \land j \in ℕ) \to (I (j) : X ⟶ ℝ^{2} \leftrightarrow (x \in X ⟼ ⟨- j, j⟩) : X ⟶ ℝ^{2})$
205	203 204	mpbird	$⊢ (φ \land j \in ℕ) \to I (j) : X ⟶ ℝ^{2}$
206	205	ad4ant14	$⊢ (((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \land j \in ℕ) \to I (j) : X ⟶ ℝ^{2}$
207	206	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}$
208		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$
209	207 208	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)))$
210	209	eqcomd	$⊢ (((((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \land j \in ℕ) \land sup (ran (abs \circ f) ℝ <) < j) \land i \in X) \to [1^{st} (I (j) (i)), 2^{nd} (I (j) (i))) = ([.) \circ I (j)) (i)$
211	197 210	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 ([.) \circ I (j)) (i)$
212	211	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)$
213	73 212	jca	$⊢ ((((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \land j \in ℕ) \land sup (ran (abs \circ f) ℝ <) < j) \to (f Fn X \land \forall i \in X f (i) \in ([.) \circ I (j)) (i))$
214		vex	$⊢ f \in V$
215	214	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))$
216	213 215	sylibr	$⊢ ((((φ \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)$
217	216	ex	$⊢ (((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \land j \in ℕ) \to (sup (ran (abs \circ f) ℝ <) < j \to f \in \underset{i \in X}{⨉} ([.) \circ I (j)) (i))$
218	217	reximdva	$⊢ ((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \to (\exists j \in ℕ sup (ran (abs \circ f) ℝ <) < j \to \exists j \in ℕ f \in \underset{i \in X}{⨉} ([.) \circ I (j)) (i))$
219	70 218	mpd	$⊢ ((φ \land f \in (ℝ^{X})) \land \neg X = \emptyset) \to \exists j \in ℕ f \in \underset{i \in X}{⨉} ([.) \circ I (j)) (i)$
220	24 25 26 219	syl21anc	$⊢ ((φ \land \neg X = \emptyset) \land f \in (ℝ^{X})) \to \exists j \in ℕ f \in \underset{i \in X}{⨉} ([.) \circ I (j)) (i)$
221		eliun	$⊢ f \in ⋃_{j \in ℕ} \underset{i \in X}{⨉} ([.) \circ I (j)) (i) \leftrightarrow \exists j \in ℕ f \in \underset{i \in X}{⨉} ([.) \circ I (j)) (i)$
222	220 221	sylibr	$⊢ ((φ \land \neg X = \emptyset) \land f \in (ℝ^{X})) \to f \in ⋃_{j \in ℕ} \underset{i \in X}{⨉} ([.) \circ I (j)) (i)$
223	222	ralrimiva	$⊢ (φ \land \neg X = \emptyset) \to \forall f \in (ℝ^{X}) f \in ⋃_{j \in ℕ} \underset{i \in X}{⨉} ([.) \circ I (j)) (i)$
224		dfss3	$⊢ ℝ^{X} \subseteq ⋃_{j \in ℕ} \underset{i \in X}{⨉} ([.) \circ I (j)) (i) \leftrightarrow \forall f \in (ℝ^{X}) f \in ⋃_{j \in ℕ} \underset{i \in X}{⨉} ([.) \circ I (j)) (i)$
225	223 224	sylibr	$⊢ (φ \land \neg X = \emptyset) \to ℝ^{X} \subseteq ⋃_{j \in ℕ} \underset{i \in X}{⨉} ([.) \circ I (j)) (i)$
226	23 225	pm2.61dan	$⊢ φ \to ℝ^{X} \subseteq ⋃_{j \in ℕ} \underset{i \in X}{⨉} ([.) \circ I (j)) (i)$

Metamath Proof Explorer

Theorem hoicvr

Proof