Theorem vonvol2

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

	Ref	Expression
Hypotheses	vonvol2.f	⊢ Ⅎ 𝑓 𝑌
	vonvol2.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	vonvol2.x	⊢ ( 𝜑 → 𝑋 ∈ dom ( voln ‘ { 𝐴 } ) )
	vonvol2.y	⊢ 𝑌 = ∪ 𝑓 ∈ 𝑋 ran 𝑓
Assertion	vonvol2	⊢ ( 𝜑 → ( ( voln ‘ { 𝐴 } ) ‘ 𝑋 ) = ( vol ‘ 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		vonvol2.f	⊢ Ⅎ 𝑓 𝑌
2		vonvol2.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		vonvol2.x	⊢ ( 𝜑 → 𝑋 ∈ dom ( voln ‘ { 𝐴 } ) )
4		vonvol2.y	⊢ 𝑌 = ∪ 𝑓 ∈ 𝑋 ran 𝑓
5		snfi	⊢ { 𝐴 } ∈ Fin
6	5	a1i	⊢ ( 𝜑 → { 𝐴 } ∈ Fin )
7	6 3	vonmblss2	⊢ ( 𝜑 → 𝑋 ⊆ ( ℝ ↑m { 𝐴 } ) )
8	1 2 7 4	ssmapsn	⊢ ( 𝜑 → 𝑋 = ( 𝑌 ↑m { 𝐴 } ) )
9	8	eqcomd	⊢ ( 𝜑 → ( 𝑌 ↑m { 𝐴 } ) = 𝑋 )
10	9 3	eqeltrd	⊢ ( 𝜑 → ( 𝑌 ↑m { 𝐴 } ) ∈ dom ( voln ‘ { 𝐴 } ) )
11	7	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → 𝑋 ⊆ ( ℝ ↑m { 𝐴 } ) )
12		simpr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → 𝑓 ∈ 𝑋 )
13	11 12	sseldd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → 𝑓 ∈ ( ℝ ↑m { 𝐴 } ) )
14		elmapi	⊢ ( 𝑓 ∈ ( ℝ ↑m { 𝐴 } ) → 𝑓 : { 𝐴 } ⟶ ℝ )
15		frn	⊢ ( 𝑓 : { 𝐴 } ⟶ ℝ → ran 𝑓 ⊆ ℝ )
16	13 14 15	3syl	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ran 𝑓 ⊆ ℝ )
17	16	ralrimiva	⊢ ( 𝜑 → ∀ 𝑓 ∈ 𝑋 ran 𝑓 ⊆ ℝ )
18		iunss	⊢ ( ∪ 𝑓 ∈ 𝑋 ran 𝑓 ⊆ ℝ ↔ ∀ 𝑓 ∈ 𝑋 ran 𝑓 ⊆ ℝ )
19	17 18	sylibr	⊢ ( 𝜑 → ∪ 𝑓 ∈ 𝑋 ran 𝑓 ⊆ ℝ )
20	4 19	eqsstrid	⊢ ( 𝜑 → 𝑌 ⊆ ℝ )
21	2 20	vonvolmbl	⊢ ( 𝜑 → ( ( 𝑌 ↑m { 𝐴 } ) ∈ dom ( voln ‘ { 𝐴 } ) ↔ 𝑌 ∈ dom vol ) )
22	10 21	mpbid	⊢ ( 𝜑 → 𝑌 ∈ dom vol )
23	2 22	vonvol	⊢ ( 𝜑 → ( ( voln ‘ { 𝐴 } ) ‘ ( 𝑌 ↑m { 𝐴 } ) ) = ( vol ‘ 𝑌 ) )
24	9	eqcomd	⊢ ( 𝜑 → 𝑋 = ( 𝑌 ↑m { 𝐴 } ) )
25	24	fveq2d	⊢ ( 𝜑 → ( ( voln ‘ { 𝐴 } ) ‘ 𝑋 ) = ( ( voln ‘ { 𝐴 } ) ‘ ( 𝑌 ↑m { 𝐴 } ) ) )
26		eqidd	⊢ ( 𝜑 → ( vol ‘ 𝑌 ) = ( vol ‘ 𝑌 ) )
27	23 25 26	3eqtr4d	⊢ ( 𝜑 → ( ( voln ‘ { 𝐴 } ) ‘ 𝑋 ) = ( vol ‘ 𝑌 ) )