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	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	hoicvrrex.y	⊢ ( 𝜑 → 𝑌 ⊆ ( ℝ ↑_m 𝑋 ) )
Assertion	hoicvrrex	⊢ ( 𝜑 → ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( 𝑌 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ +∞ = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )

Proof

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

Metamath Proof Explorer

Theorem hoicvrrex

Proof