ovolval4lem2

Description: The value of the Lebesgue outer measure for subsets of the reals. Similar to ovolval3 , but here f is may represent unordered interval bounds. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	ovolval4lem2.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	ovolval4lem2.m	⊢ 𝑀 = { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) }
	ovolval4lem2.g	⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ⟩ )
Assertion	ovolval4lem2	⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = inf ( 𝑀 , ℝ^* , < ) )

Proof

Step	Hyp	Ref	Expression
1		ovolval4lem2.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2		ovolval4lem2.m	⊢ 𝑀 = { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) }
3		ovolval4lem2.g	⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ⟩ )
4		iftrue	⊢ ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) → if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) = ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) )
5	4	opeq2d	⊢ ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) → ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ⟩ = ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ )
6	5	adantl	⊢ ( ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) → ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ⟩ = ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ )
7		df-br	⊢ ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ↔ ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ ∈ ≤ )
8	7	bilani	⊢ ( ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) → ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ ∈ ≤ )
9	6 8	eqeltrd	⊢ ( ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) → ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ⟩ ∈ ≤ )
10		iffalse	⊢ ( ¬ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) → if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) = ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) )
11	10	opeq2d	⊢ ( ¬ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) → ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ⟩ = ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ )
12	11	adantl	⊢ ( ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ ¬ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) → ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ⟩ = ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ )
13		elmapi	⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → 𝑓 : ℕ ⟶ ( ℝ × ℝ ) )
14	13	ffvelcdmda	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑓 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) )
15		xp1st	⊢ ( ( 𝑓 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) → ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ )
16	14 15	syl	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ )
17	16	leidd	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) )
18		df-br	⊢ ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ↔ ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ ∈ ≤ )
19	17 18	sylib	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ ∈ ≤ )
20	19	adantr	⊢ ( ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ ¬ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) → ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ ∈ ≤ )
21	12 20	eqeltrd	⊢ ( ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ ¬ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) → ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ⟩ ∈ ≤ )
22	9 21	pm2.61dan	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ⟩ ∈ ≤ )
23		xp2nd	⊢ ( ( 𝑓 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) → ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ )
24	14 23	syl	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ )
25	24 16	ifcld	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ∈ ℝ )
26		opelxpi	⊢ ( ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ ∧ if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ∈ ℝ ) → ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ⟩ ∈ ( ℝ × ℝ ) )
27	16 25 26	syl2anc	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ⟩ ∈ ( ℝ × ℝ ) )
28	22 27	elind	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑛 ∈ ℕ ) → ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ⟩ ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
29	28 3	fmptd	⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
30		reex	⊢ ℝ ∈ V
31	30 30	xpex	⊢ ( ℝ × ℝ ) ∈ V
32	31	inex2	⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ∈ V
33	32	a1i	⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → ( ≤ ∩ ( ℝ × ℝ ) ) ∈ V )
34		nnex	⊢ ℕ ∈ V
35	34	a1i	⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → ℕ ∈ V )
36	33 35	elmapd	⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → ( 𝐺 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ↔ 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) )
37	29 36	mpbird	⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → 𝐺 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) )
38	37	adantr	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ) → 𝐺 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) )
39		simpr	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) → 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) )
40		rexpssxrxp	⊢ ( ℝ × ℝ ) ⊆ ( ℝ^* × ℝ^* )
41	40	a1i	⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → ( ℝ × ℝ ) ⊆ ( ℝ^* × ℝ^* ) )
42	13 41	fssd	⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → 𝑓 : ℕ ⟶ ( ℝ^* × ℝ^* ) )
43		2fveq3	⊢ ( 𝑘 = 𝑛 → ( 1^st ‘ ( 𝑓 ‘ 𝑘 ) ) = ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) )
44		2fveq3	⊢ ( 𝑘 = 𝑛 → ( 2^nd ‘ ( 𝑓 ‘ 𝑘 ) ) = ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) )
45	43 44	breq12d	⊢ ( 𝑘 = 𝑛 → ( ( 1^st ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑘 ) ) ↔ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
46	45	cbvrabv	⊢ { 𝑘 ∈ ℕ ∣ ( 1^st ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑘 ) ) } = { 𝑛 ∈ ℕ ∣ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) }
47	42 3 46	ovolval4lem1	⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → ( ∪ ran ( (,) ∘ 𝑓 ) = ∪ ran ( (,) ∘ 𝐺 ) ∧ ( vol ∘ ( (,) ∘ 𝑓 ) ) = ( vol ∘ ( (,) ∘ 𝐺 ) ) ) )
48	47	simpld	⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → ∪ ran ( (,) ∘ 𝑓 ) = ∪ ran ( (,) ∘ 𝐺 ) )
49	48	adantr	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) → ∪ ran ( (,) ∘ 𝑓 ) = ∪ ran ( (,) ∘ 𝐺 ) )
50	39 49	sseqtrd	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) → 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐺 ) )
51	50	adantrr	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ) → 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐺 ) )
52		simpr	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) → 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) )
53	47	simprd	⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → ( vol ∘ ( (,) ∘ 𝑓 ) ) = ( vol ∘ ( (,) ∘ 𝐺 ) ) )
54		coass	⊢ ( ( vol ∘ (,) ) ∘ 𝑓 ) = ( vol ∘ ( (,) ∘ 𝑓 ) )
55	54	a1i	⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → ( ( vol ∘ (,) ) ∘ 𝑓 ) = ( vol ∘ ( (,) ∘ 𝑓 ) ) )
56		coass	⊢ ( ( vol ∘ (,) ) ∘ 𝐺 ) = ( vol ∘ ( (,) ∘ 𝐺 ) )
57	56	a1i	⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → ( ( vol ∘ (,) ) ∘ 𝐺 ) = ( vol ∘ ( (,) ∘ 𝐺 ) ) )
58	53 55 57	3eqtr4d	⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → ( ( vol ∘ (,) ) ∘ 𝑓 ) = ( ( vol ∘ (,) ) ∘ 𝐺 ) )
59	58	fveq2d	⊢ ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) → ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝐺 ) ) )
60	59	adantr	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) → ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝐺 ) ) )
61	52 60	eqtrd	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) → 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝐺 ) ) )
62	61	adantrl	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ) → 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝐺 ) ) )
63	51 62	jca	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ) → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐺 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝐺 ) ) ) )
64		coeq2	⊢ ( 𝑔 = 𝐺 → ( (,) ∘ 𝑔 ) = ( (,) ∘ 𝐺 ) )
65	64	rneqd	⊢ ( 𝑔 = 𝐺 → ran ( (,) ∘ 𝑔 ) = ran ( (,) ∘ 𝐺 ) )
66	65	unieqd	⊢ ( 𝑔 = 𝐺 → ∪ ran ( (,) ∘ 𝑔 ) = ∪ ran ( (,) ∘ 𝐺 ) )
67	66	sseq2d	⊢ ( 𝑔 = 𝐺 → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ↔ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐺 ) ) )
68		coeq2	⊢ ( 𝑔 = 𝐺 → ( ( vol ∘ (,) ) ∘ 𝑔 ) = ( ( vol ∘ (,) ) ∘ 𝐺 ) )
69	68	fveq2d	⊢ ( 𝑔 = 𝐺 → ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝐺 ) ) )
70	69	eqeq2d	⊢ ( 𝑔 = 𝐺 → ( 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ↔ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝐺 ) ) ) )
71	67 70	anbi12d	⊢ ( 𝑔 = 𝐺 → ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) ↔ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐺 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝐺 ) ) ) ) )
72	71	rspcev	⊢ ( ( 𝐺 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐺 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝐺 ) ) ) ) → ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) )
73	38 63 72	syl2anc	⊢ ( ( 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ) → ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) )
74	73	rexlimiva	⊢ ( ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) → ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) )
75		inss2	⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
76		mapss	⊢ ( ( ( ℝ × ℝ ) ∈ V ∧ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ ) ) → ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ⊆ ( ( ℝ × ℝ ) ↑_m ℕ ) )
77	31 75 76	mp2an	⊢ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ⊆ ( ( ℝ × ℝ ) ↑_m ℕ )
78	77	sseli	⊢ ( 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) → 𝑔 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) )
79	78	adantr	⊢ ( ( 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) ) → 𝑔 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) )
80		simpr	⊢ ( ( 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) ) → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) )
81		coeq2	⊢ ( 𝑓 = 𝑔 → ( (,) ∘ 𝑓 ) = ( (,) ∘ 𝑔 ) )
82	81	rneqd	⊢ ( 𝑓 = 𝑔 → ran ( (,) ∘ 𝑓 ) = ran ( (,) ∘ 𝑔 ) )
83	82	unieqd	⊢ ( 𝑓 = 𝑔 → ∪ ran ( (,) ∘ 𝑓 ) = ∪ ran ( (,) ∘ 𝑔 ) )
84	83	sseq2d	⊢ ( 𝑓 = 𝑔 → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ↔ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ) )
85		coeq2	⊢ ( 𝑓 = 𝑔 → ( ( vol ∘ (,) ) ∘ 𝑓 ) = ( ( vol ∘ (,) ) ∘ 𝑔 ) )
86	85	fveq2d	⊢ ( 𝑓 = 𝑔 → ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) )
87	86	eqeq2d	⊢ ( 𝑓 = 𝑔 → ( 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ↔ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) )
88	84 87	anbi12d	⊢ ( 𝑓 = 𝑔 → ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ↔ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) ) )
89	88	rspcev	⊢ ( ( 𝑔 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) ) → ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) )
90	79 80 89	syl2anc	⊢ ( ( 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) ) → ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) )
91	90	rexlimiva	⊢ ( ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) → ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) )
92	74 91	impbii	⊢ ( ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ↔ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) )
93	92	rabbii	⊢ { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) } = { 𝑦 ∈ ℝ^* ∣ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) }
94	2 93	eqtri	⊢ 𝑀 = { 𝑦 ∈ ℝ^* ∣ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) }
95	1 94	ovolval3	⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = inf ( 𝑀 , ℝ^* , < ) )

Metamath Proof Explorer

Theorem ovolval4lem2

Proof