hoicvrrex

Description: Any subset of the multidimensional reals can be covered by a countable set of half-open intervals, see Definition 115A (b) of Fremlin1 p. 29. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	hoicvrrex.fi	$⊢ φ \to X \in Fin$
	hoicvrrex.y	$⊢ φ \to Y \subseteq ℝ^{X}$
Assertion	hoicvrrex	$⊢ φ \to \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (Y \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land +∞ = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))$

Proof

Step	Hyp	Ref	Expression
1		hoicvrrex.fi	$⊢ φ \to X \in Fin$
2		hoicvrrex.y	$⊢ φ \to Y \subseteq ℝ^{X}$
3		nnre	$⊢ j \in ℕ \to j \in ℝ$
4	3	renegcld	$⊢ j \in ℕ \to - j \in ℝ$
5		opelxpi	$⊢ (- j \in ℝ \land j \in ℝ) \to ⟨- j, j⟩ \in ℝ^{2}$
6	4 3 5	syl2anc	$⊢ j \in ℕ \to ⟨- j, j⟩ \in ℝ^{2}$
7	6	ad2antlr	$⊢ ((φ \land j \in ℕ) \land k \in X) \to ⟨- j, j⟩ \in ℝ^{2}$
8		eqid	$⊢ (k \in X ⟼ ⟨- j, j⟩) = (k \in X ⟼ ⟨- j, j⟩)$
9	7 8	fmptd	$⊢ (φ \land j \in ℕ) \to (k \in X ⟼ ⟨- j, j⟩) : X ⟶ ℝ^{2}$
10		reex	$⊢ ℝ \in V$
11	10 10	xpex	$⊢ ℝ^{2} \in V$
12	11	a1i	$⊢ φ \to ℝ^{2} \in V$
13		elmapg	$⊢ (ℝ^{2} \in V \land X \in Fin) \to ((k \in X ⟼ ⟨- j, j⟩) \in ({ℝ^{2}}^{X}) \leftrightarrow (k \in X ⟼ ⟨- j, j⟩) : X ⟶ ℝ^{2})$
14	12 1 13	syl2anc	$⊢ φ \to ((k \in X ⟼ ⟨- j, j⟩) \in ({ℝ^{2}}^{X}) \leftrightarrow (k \in X ⟼ ⟨- j, j⟩) : X ⟶ ℝ^{2})$
15	14	adantr	$⊢ (φ \land j \in ℕ) \to ((k \in X ⟼ ⟨- j, j⟩) \in ({ℝ^{2}}^{X}) \leftrightarrow (k \in X ⟼ ⟨- j, j⟩) : X ⟶ ℝ^{2})$
16	9 15	mpbird	$⊢ (φ \land j \in ℕ) \to (k \in X ⟼ ⟨- j, j⟩) \in ({ℝ^{2}}^{X})$
17		eqid	$⊢ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) = (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩))$
18	16 17	fmptd	$⊢ φ \to (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) : ℕ ⟶ {ℝ^{2}}^{X}$
19		ovex	$⊢ {ℝ^{2}}^{X} \in V$
20		nnex	$⊢ ℕ \in V$
21	19 20	elmap	$⊢ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) \in ({({ℝ^{2}}^{X})}^{ℕ}) \leftrightarrow (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) : ℕ ⟶ {ℝ^{2}}^{X}$
22	18 21	sylibr	$⊢ φ \to (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) \in ({({ℝ^{2}}^{X})}^{ℕ})$
23		eqid	$⊢ (j \in ℕ ⟼ (l \in X ⟼ ⟨- j, j⟩)) = (j \in ℕ ⟼ (l \in X ⟼ ⟨- j, j⟩))$
24	23 1	hoicvr	$⊢ φ \to ℝ^{X} \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ (j \in ℕ ⟼ (l \in X ⟼ ⟨- j, j⟩)) (j)) (k)$
25		eqidd	$⊢ l = k \to ⟨- j, j⟩ = ⟨- j, j⟩$
26	25	cbvmptv	$⊢ (l \in X ⟼ ⟨- j, j⟩) = (k \in X ⟼ ⟨- j, j⟩)$
27	26	mpteq2i	$⊢ (j \in ℕ ⟼ (l \in X ⟼ ⟨- j, j⟩)) = (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩))$
28	27	a1i	$⊢ φ \to (j \in ℕ ⟼ (l \in X ⟼ ⟨- j, j⟩)) = (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩))$
29	28	fveq1d	$⊢ φ \to (j \in ℕ ⟼ (l \in X ⟼ ⟨- j, j⟩)) (j) = (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)$
30	29	coeq2d	$⊢ φ \to [.) \circ (j \in ℕ ⟼ (l \in X ⟼ ⟨- j, j⟩)) (j) = [.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)$
31	30	fveq1d	$⊢ φ \to ([.) \circ (j \in ℕ ⟼ (l \in X ⟼ ⟨- j, j⟩)) (j)) (k) = ([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k)$
32	31	ixpeq2dv	$⊢ φ \to \underset{k \in X}{⨉} ([.) \circ (j \in ℕ ⟼ (l \in X ⟼ ⟨- j, j⟩)) (j)) (k) = \underset{k \in X}{⨉} ([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k)$
33	32	iuneq2d	$⊢ φ \to ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ (j \in ℕ ⟼ (l \in X ⟼ ⟨- j, j⟩)) (j)) (k) = ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k)$
34	24 33	sseqtrd	$⊢ φ \to ℝ^{X} \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k)$
35	2 34	sstrd	$⊢ φ \to Y \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k)$
36		simpr	$⊢ (φ \land j \in ℕ) \to j \in ℕ$
37	16	elexd	$⊢ (φ \land j \in ℕ) \to (k \in X ⟼ ⟨- j, j⟩) \in V$
38	17	fvmpt2	$⊢ (j \in ℕ \land (k \in X ⟼ ⟨- j, j⟩) \in V) \to (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j) = (k \in X ⟼ ⟨- j, j⟩)$
39	36 37 38	syl2anc	$⊢ (φ \land j \in ℕ) \to (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j) = (k \in X ⟼ ⟨- j, j⟩)$
40	39 7	fmpt3d	$⊢ (φ \land j \in ℕ) \to (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j) : X ⟶ ℝ^{2}$
41	40	adantr	$⊢ ((φ \land j \in ℕ) \land k \in X) \to (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j) : X ⟶ ℝ^{2}$
42		simpr	$⊢ ((φ \land j \in ℕ) \land k \in X) \to k \in X$
43	41 42	fvovco	$⊢ ((φ \land j \in ℕ) \land k \in X) \to ([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k) = [1^{st} ((j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j) (k)), 2^{nd} ((j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j) (k)))$
44	39	fveq1d	$⊢ (φ \land j \in ℕ) \to (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j) (k) = (k \in X ⟼ ⟨- j, j⟩) (k)$
45	44	adantr	$⊢ ((φ \land j \in ℕ) \land k \in X) \to (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j) (k) = (k \in X ⟼ ⟨- j, j⟩) (k)$
46		simpr	$⊢ (φ \land k \in X) \to k \in X$
47		opex	$⊢ ⟨- j, j⟩ \in V$
48	47	a1i	$⊢ (φ \land k \in X) \to ⟨- j, j⟩ \in V$
49	8	fvmpt2	$⊢ (k \in X \land ⟨- j, j⟩ \in V) \to (k \in X ⟼ ⟨- j, j⟩) (k) = ⟨- j, j⟩$
50	46 48 49	syl2anc	$⊢ (φ \land k \in X) \to (k \in X ⟼ ⟨- j, j⟩) (k) = ⟨- j, j⟩$
51	50	adantlr	$⊢ ((φ \land j \in ℕ) \land k \in X) \to (k \in X ⟼ ⟨- j, j⟩) (k) = ⟨- j, j⟩$
52	45 51	eqtrd	$⊢ ((φ \land j \in ℕ) \land k \in X) \to (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j) (k) = ⟨- j, j⟩$
53	52	fveq2d	$⊢ ((φ \land j \in ℕ) \land k \in X) \to 1^{st} ((j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j) (k)) = 1^{st} (⟨- j, j⟩)$
54		negex	$⊢ - j \in V$
55		vex	$⊢ j \in V$
56	54 55	op1st	$⊢ 1^{st} (⟨- j, j⟩) = - j$
57	56	a1i	$⊢ ((φ \land j \in ℕ) \land k \in X) \to 1^{st} (⟨- j, j⟩) = - j$
58	53 57	eqtrd	$⊢ ((φ \land j \in ℕ) \land k \in X) \to 1^{st} ((j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j) (k)) = - j$
59	52	fveq2d	$⊢ ((φ \land j \in ℕ) \land k \in X) \to 2^{nd} ((j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j) (k)) = 2^{nd} (⟨- j, j⟩)$
60	54 55	op2nd	$⊢ 2^{nd} (⟨- j, j⟩) = j$
61	60	a1i	$⊢ ((φ \land j \in ℕ) \land k \in X) \to 2^{nd} (⟨- j, j⟩) = j$
62	59 61	eqtrd	$⊢ ((φ \land j \in ℕ) \land k \in X) \to 2^{nd} ((j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j) (k)) = j$
63	58 62	oveq12d	$⊢ ((φ \land j \in ℕ) \land k \in X) \to [1^{st} ((j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j) (k)), 2^{nd} ((j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j) (k))) = [- j, j)$
64	43 63	eqtrd	$⊢ ((φ \land j \in ℕ) \land k \in X) \to ([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k) = [- j, j)$
65	64	fveq2d	$⊢ ((φ \land j \in ℕ) \land k \in X) \to vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k)) = vol ([- j, j))$
66		volico	$⊢ (- j \in ℝ \land j \in ℝ) \to vol ([- j, j)) = if (- j < j, j - (- j), 0)$
67	4 3 66	syl2anc	$⊢ j \in ℕ \to vol ([- j, j)) = if (- j < j, j - (- j), 0)$
68		nnrp	$⊢ j \in ℕ \to j \in ℝ^{+}$
69		neglt	$⊢ j \in ℝ^{+} \to - j < j$
70	68 69	syl	$⊢ j \in ℕ \to - j < j$
71	70	iftrued	$⊢ j \in ℕ \to if (- j < j, j - (- j), 0) = j - (- j)$
72	3	recnd	$⊢ j \in ℕ \to j \in ℂ$
73	72 72	subnegd	$⊢ j \in ℕ \to j - (- j) = j + j$
74	72	2timesd	$⊢ j \in ℕ \to 2 j = j + j$
75	73 74	eqtr4d	$⊢ j \in ℕ \to j - (- j) = 2 j$
76	67 71 75	3eqtrd	$⊢ j \in ℕ \to vol ([- j, j)) = 2 j$
77	76	ad2antlr	$⊢ ((φ \land j \in ℕ) \land k \in X) \to vol ([- j, j)) = 2 j$
78	65 77	eqtrd	$⊢ ((φ \land j \in ℕ) \land k \in X) \to vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k)) = 2 j$
79	78	prodeq2dv	$⊢ (φ \land j \in ℕ) \to \prod_{k \in X} vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k)) = \prod_{k \in X} 2 j$
80	1	adantr	$⊢ (φ \land j \in ℕ) \to X \in Fin$
81		2cnd	$⊢ (φ \land j \in ℕ) \to 2 \in ℂ$
82	72	adantl	$⊢ (φ \land j \in ℕ) \to j \in ℂ$
83	81 82	mulcld	$⊢ (φ \land j \in ℕ) \to 2 j \in ℂ$
84		fprodconst	$⊢ (X \in Fin \land 2 j \in ℂ) \to \prod_{k \in X} 2 j = {2 j}^{\|X\|}$
85	80 83 84	syl2anc	$⊢ (φ \land j \in ℕ) \to \prod_{k \in X} 2 j = {2 j}^{\|X\|}$
86	79 85	eqtrd	$⊢ (φ \land j \in ℕ) \to \prod_{k \in X} vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k)) = {2 j}^{\|X\|}$
87	86	mpteq2dva	$⊢ φ \to (j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k))) = (j \in ℕ ⟼ {2 j}^{\|X\|})$
88	87	fveq2d	$⊢ φ \to sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k)))) = sum^((j \in ℕ ⟼ {2 j}^{\|X\|}))$
89	20	a1i	$⊢ φ \to ℕ \in V$
90	68	ssriv	$⊢ ℕ \subseteq ℝ^{+}$
91		ioorp	$⊢ (0, +∞) = ℝ^{+}$
92	91	eqcomi	$⊢ ℝ^{+} = (0, +∞)$
93	90 92	sseqtri	$⊢ ℕ \subseteq (0, +∞)$
94		ioossicc	$⊢ (0, +∞) \subseteq [0, +∞]$
95	93 94	sstri	$⊢ ℕ \subseteq [0, +∞]$
96		2nn	$⊢ 2 \in ℕ$
97	96	a1i	$⊢ (φ \land j \in ℕ) \to 2 \in ℕ$
98	97 36	nnmulcld	$⊢ (φ \land j \in ℕ) \to 2 j \in ℕ$
99		hashcl	$⊢ X \in Fin \to \|X\| \in ℕ_{0}$
100	1 99	syl	$⊢ φ \to \|X\| \in ℕ_{0}$
101	100	adantr	$⊢ (φ \land j \in ℕ) \to \|X\| \in ℕ_{0}$
102		nnexpcl	$⊢ (2 j \in ℕ \land \|X\| \in ℕ_{0}) \to {2 j}^{\|X\|} \in ℕ$
103	98 101 102	syl2anc	$⊢ (φ \land j \in ℕ) \to {2 j}^{\|X\|} \in ℕ$
104	95 103	sselid	$⊢ (φ \land j \in ℕ) \to {2 j}^{\|X\|} \in [0, +∞]$
105		eqid	$⊢ (j \in ℕ ⟼ {2 j}^{\|X\|}) = (j \in ℕ ⟼ {2 j}^{\|X\|})$
106	104 105	fmptd	$⊢ φ \to (j \in ℕ ⟼ {2 j}^{\|X\|}) : ℕ ⟶ [0, +∞]$
107	89 106	sge0xrcl	$⊢ φ \to sum^((j \in ℕ ⟼ {2 j}^{\|X\|})) \in ℝ^{*}$
108		pnfxr	$⊢ +∞ \in ℝ^{*}$
109	108	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
110		1nn	$⊢ 1 \in ℕ$
111	95 110	sselii	$⊢ 1 \in [0, +∞]$
112	111	a1i	$⊢ (φ \land j \in ℕ) \to 1 \in [0, +∞]$
113		eqid	$⊢ (j \in ℕ ⟼ 1) = (j \in ℕ ⟼ 1)$
114	112 113	fmptd	$⊢ φ \to (j \in ℕ ⟼ 1) : ℕ ⟶ [0, +∞]$
115	89 114	sge0xrcl	$⊢ φ \to sum^((j \in ℕ ⟼ 1)) \in ℝ^{*}$
116		nnnfi	$⊢ \neg ℕ \in Fin$
117	116	a1i	$⊢ φ \to \neg ℕ \in Fin$
118		1rp	$⊢ 1 \in ℝ^{+}$
119	118	a1i	$⊢ φ \to 1 \in ℝ^{+}$
120	89 117 119	sge0rpcpnf	$⊢ φ \to sum^((j \in ℕ ⟼ 1)) = +∞$
121	120	eqcomd	$⊢ φ \to +∞ = sum^((j \in ℕ ⟼ 1))$
122	109 121	xreqled	$⊢ φ \to +∞ \leq sum^((j \in ℕ ⟼ 1))$
123		nfv	$⊢ Ⅎ j φ$
124	114	fvmptelcdm	$⊢ (φ \land j \in ℕ) \to 1 \in [0, +∞]$
125	103	nnge1d	$⊢ (φ \land j \in ℕ) \to 1 \leq {2 j}^{\|X\|}$
126	123 89 124 104 125	sge0lempt	$⊢ φ \to sum^((j \in ℕ ⟼ 1)) \leq sum^((j \in ℕ ⟼ {2 j}^{\|X\|}))$
127	109 115 107 122 126	xrletrd	$⊢ φ \to +∞ \leq sum^((j \in ℕ ⟼ {2 j}^{\|X\|}))$
128	107 127	xrgepnfd	$⊢ φ \to sum^((j \in ℕ ⟼ {2 j}^{\|X\|})) = +∞$
129		eqidd	$⊢ φ \to +∞ = +∞$
130	88 128 129	3eqtrrd	$⊢ φ \to +∞ = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k))))$
131	35 130	jca	$⊢ φ \to (Y \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k) \land +∞ = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k)))))$
132		nfcv	$⊢ \underline{Ⅎ} j i$
133		nfmpt1	$⊢ \underline{Ⅎ} j (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩))$
134	132 133	nfeq	$⊢ Ⅎ j i = (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩))$
135		nfcv	$⊢ \underline{Ⅎ} k i$
136		nfcv	$⊢ \underline{Ⅎ} k ℕ$
137		nfmpt1	$⊢ \underline{Ⅎ} k (k \in X ⟼ ⟨- j, j⟩)$
138	136 137	nfmpt	$⊢ \underline{Ⅎ} k (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩))$
139	135 138	nfeq	$⊢ Ⅎ k i = (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩))$
140		fveq1	$⊢ i = (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) \to i (j) = (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)$
141	140	coeq2d	$⊢ i = (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) \to [.) \circ i (j) = [.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)$
142	141	fveq1d	$⊢ i = (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) \to ([.) \circ i (j)) (k) = ([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k)$
143	142	adantr	$⊢ (i = (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) \land k \in X) \to ([.) \circ i (j)) (k) = ([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k)$
144	139 143	ixpeq2d	$⊢ i = (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) \to \underset{k \in X}{⨉} ([.) \circ i (j)) (k) = \underset{k \in X}{⨉} ([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k)$
145	144	adantr	$⊢ (i = (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) \land j \in ℕ) \to \underset{k \in X}{⨉} ([.) \circ i (j)) (k) = \underset{k \in X}{⨉} ([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k)$
146	134 145	iuneq2df	$⊢ i = (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) \to ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) = ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k)$
147	146	sseq2d	$⊢ i = (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) \to (Y \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \leftrightarrow Y \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k))$
148	142	fveq2d	$⊢ i = (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) \to vol (([.) \circ i (j)) (k)) = vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k))$
149	148	a1d	$⊢ i = (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) \to (k \in X \to vol (([.) \circ i (j)) (k)) = vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k)))$
150	139 149	ralrimi	$⊢ i = (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) \to \forall k \in X vol (([.) \circ i (j)) (k)) = vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k))$
151	150	adantr	$⊢ (i = (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) \land j \in ℕ) \to \forall k \in X vol (([.) \circ i (j)) (k)) = vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k))$
152	151	prodeq2d	$⊢ (i = (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) \land j \in ℕ) \to \prod_{k \in X} vol (([.) \circ i (j)) (k)) = \prod_{k \in X} vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k))$
153	134 152	mpteq2da	$⊢ i = (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) \to (j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))) = (j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k)))$
154	153	fveq2d	$⊢ i = (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) \to sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k))))$
155	154	eqeq2d	$⊢ i = (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) \to (+∞ = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))) \leftrightarrow +∞ = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k)))))$
156	147 155	anbi12d	$⊢ i = (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) \to ((Y \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land +∞ = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))) \leftrightarrow (Y \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k) \land +∞ = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k))))))$
157	156	rspcev	$⊢ ((j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) \in ({({ℝ^{2}}^{X})}^{ℕ}) \land (Y \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k) \land +∞ = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ (j \in ℕ ⟼ (k \in X ⟼ ⟨- j, j⟩)) (j)) (k)))))) \to \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (Y \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land +∞ = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))$
158	22 131 157	syl2anc	$⊢ φ \to \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (Y \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land +∞ = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))$

Metamath Proof Explorer

Theorem hoicvrrex

Proof