Theorem ovnovollem3

Description: The 1-dimensional Lebesgue outer measure agrees with the Lebesgue outer measure on subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	ovnovollem3.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	ovnovollem3.b	⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
	ovnovollem3.m	⊢ 𝑀 = { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) }
	ovnovollem3.n	⊢ 𝑁 = { 𝑧 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) }
Assertion	ovnovollem3	⊢ ( 𝜑 → ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝐵 ↑m { 𝐴 } ) ) = ( vol* ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ovnovollem3.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		ovnovollem3.b	⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
3		ovnovollem3.m	⊢ 𝑀 = { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) }
4		ovnovollem3.n	⊢ 𝑁 = { 𝑧 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) }
5		snnzg	⊢ ( 𝐴 ∈ 𝑉 → { 𝐴 } ≠ ∅ )
6	1 5	syl	⊢ ( 𝜑 → { 𝐴 } ≠ ∅ )
7	6	neneqd	⊢ ( 𝜑 → ¬ { 𝐴 } = ∅ )
8	7	iffalsed	⊢ ( 𝜑 → if ( { 𝐴 } = ∅ , 0 , inf ( 𝑀 , ℝ* , < ) ) = inf ( 𝑀 , ℝ* , < ) )
9		snfi	⊢ { 𝐴 } ∈ Fin
10	9	a1i	⊢ ( 𝜑 → { 𝐴 } ∈ Fin )
11		reex	⊢ ℝ ∈ V
12	11	a1i	⊢ ( 𝜑 → ℝ ∈ V )
13		mapss	⊢ ( ( ℝ ∈ V ∧ 𝐵 ⊆ ℝ ) → ( 𝐵 ↑m { 𝐴 } ) ⊆ ( ℝ ↑m { 𝐴 } ) )
14	12 2 13	syl2anc	⊢ ( 𝜑 → ( 𝐵 ↑m { 𝐴 } ) ⊆ ( ℝ ↑m { 𝐴 } ) )
15	10 14 3	ovnval2	⊢ ( 𝜑 → ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝐵 ↑m { 𝐴 } ) ) = if ( { 𝐴 } = ∅ , 0 , inf ( 𝑀 , ℝ* , < ) ) )
16	2 4	ovolval5	⊢ ( 𝜑 → ( vol* ‘ 𝐵 ) = inf ( 𝑁 , ℝ* , < ) )
17	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ) ∧ ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) → 𝐴 ∈ 𝑉 )
18		simplr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ) ∧ ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) → 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) )
19		fveq2	⊢ ( 𝑛 = 𝑗 → ( 𝑓 ‘ 𝑛 ) = ( 𝑓 ‘ 𝑗 ) )
20	19	opeq2d	⊢ ( 𝑛 = 𝑗 → ⟨ 𝐴 , ( 𝑓 ‘ 𝑛 ) ⟩ = ⟨ 𝐴 , ( 𝑓 ‘ 𝑗 ) ⟩ )
21	20	sneqd	⊢ ( 𝑛 = 𝑗 → { ⟨ 𝐴 , ( 𝑓 ‘ 𝑛 ) ⟩ } = { ⟨ 𝐴 , ( 𝑓 ‘ 𝑗 ) ⟩ } )
22	21	cbvmptv	⊢ ( 𝑛 ∈ ℕ ↦ { ⟨ 𝐴 , ( 𝑓 ‘ 𝑛 ) ⟩ } ) = ( 𝑗 ∈ ℕ ↦ { ⟨ 𝐴 , ( 𝑓 ‘ 𝑗 ) ⟩ } )
23		simprl	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ) ∧ ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) → 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) )
24	12 2	ssexd	⊢ ( 𝜑 → 𝐵 ∈ V )
25	24	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ) → 𝐵 ∈ V )
26	25	adantr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ) ∧ ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) → 𝐵 ∈ V )
27		simprr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ) ∧ ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) → 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) )
28	17 18 22 23 26 27	ovnovollem1	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ) ∧ ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) → ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
29	28	rexlimdva2	⊢ ( 𝜑 → ( ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) → ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
30	1	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ∧ ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → 𝐴 ∈ 𝑉 )
31	24	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ∧ ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → 𝐵 ∈ V )
32		simp2	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ∧ ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) )
33		simp3l	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ∧ ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) )
34		fveq2	⊢ ( 𝑗 = 𝑛 → ( 𝑖 ‘ 𝑗 ) = ( 𝑖 ‘ 𝑛 ) )
35	34	coeq2d	⊢ ( 𝑗 = 𝑛 → ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) = ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) )
36	35	fveq1d	⊢ ( 𝑗 = 𝑛 → ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑘 ) )
37	36	ixpeq2dv	⊢ ( 𝑗 = 𝑛 → X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑘 ) )
38		fveq2	⊢ ( 𝑘 = 𝑙 → ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑘 ) = ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 ) )
39	38	cbvixpv	⊢ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑘 ) = X 𝑙 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 )
40	39	a1i	⊢ ( 𝑗 = 𝑛 → X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑘 ) = X 𝑙 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 ) )
41	37 40	eqtrd	⊢ ( 𝑗 = 𝑛 → X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = X 𝑙 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 ) )
42	41	cbviunv	⊢ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = ∪ 𝑛 ∈ ℕ X 𝑙 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 )
43	42	sseq2i	⊢ ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ↔ ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑛 ∈ ℕ X 𝑙 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 ) )
44	43	biimpi	⊢ ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) → ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑛 ∈ ℕ X 𝑙 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 ) )
45	33 44	syl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ∧ ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑛 ∈ ℕ X 𝑙 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 ) )
46		simp3r	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ∧ ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) )
47	36	fveq2d	⊢ ( 𝑗 = 𝑛 → ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑘 ) ) )
48	47	prodeq2ad	⊢ ( 𝑗 = 𝑛 → ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑘 ) ) )
49	38	fveq2d	⊢ ( 𝑘 = 𝑙 → ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 ) ) )
50	49	cbvprodv	⊢ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑘 ) ) = ∏ 𝑙 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 ) )
51	50	a1i	⊢ ( 𝑗 = 𝑛 → ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑘 ) ) = ∏ 𝑙 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 ) ) )
52	48 51	eqtrd	⊢ ( 𝑗 = 𝑛 → ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ∏ 𝑙 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 ) ) )
53	52	cbvmptv	⊢ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) = ( 𝑛 ∈ ℕ ↦ ∏ 𝑙 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 ) ) )
54	53	fveq2i	⊢ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ∏ 𝑙 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 ) ) ) )
55	54	eqeq2i	⊢ ( 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ↔ 𝑧 = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ∏ 𝑙 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 ) ) ) ) )
56	55	biimpi	⊢ ( 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) → 𝑧 = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ∏ 𝑙 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 ) ) ) ) )
57	46 56	syl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ∧ ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → 𝑧 = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ∏ 𝑙 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑛 ) ) ‘ 𝑙 ) ) ) ) )
58		fveq2	⊢ ( 𝑚 = 𝑛 → ( 𝑖 ‘ 𝑚 ) = ( 𝑖 ‘ 𝑛 ) )
59	58	fveq1d	⊢ ( 𝑚 = 𝑛 → ( ( 𝑖 ‘ 𝑚 ) ‘ 𝐴 ) = ( ( 𝑖 ‘ 𝑛 ) ‘ 𝐴 ) )
60	59	cbvmptv	⊢ ( 𝑚 ∈ ℕ ↦ ( ( 𝑖 ‘ 𝑚 ) ‘ 𝐴 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝐴 ) )
61	30 31 32 45 57 60	ovnovollem2	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ∧ ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) )
62	61	3exp	⊢ ( 𝜑 → ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) → ( ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) ) )
63	62	rexlimdv	⊢ ( 𝜑 → ( ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) )
64	29 63	impbid	⊢ ( 𝜑 → ( ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ↔ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
65	64	rabbidv	⊢ ( 𝜑 → { 𝑧 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) } = { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } )
66	4	a1i	⊢ ( 𝜑 → 𝑁 = { 𝑧 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) } )
67	3	a1i	⊢ ( 𝜑 → 𝑀 = { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } )
68	65 66 67	3eqtr4d	⊢ ( 𝜑 → 𝑁 = 𝑀 )
69	68	infeq1d	⊢ ( 𝜑 → inf ( 𝑁 , ℝ* , < ) = inf ( 𝑀 , ℝ* , < ) )
70	16 69	eqtrd	⊢ ( 𝜑 → ( vol* ‘ 𝐵 ) = inf ( 𝑀 , ℝ* , < ) )
71	8 15 70	3eqtr4d	⊢ ( 𝜑 → ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝐵 ↑m { 𝐴 } ) ) = ( vol* ‘ 𝐵 ) )