Theorem vonvolmbl2

Description: A subset X of the space of 1-dimensional Real numbers is Lebesgue measurable if and only if its projection Y on the Real numbers is Lebesgue measure. (Contributed by Glauco Siliprandi, 3-Mar-2021)

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

Proof

Step	Hyp	Ref	Expression
1		vonvolmbl2.f	⊢ Ⅎ 𝑓 𝑌
2		vonvolmbl2.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		vonvolmbl2.x	⊢ ( 𝜑 → 𝑋 ⊆ ( ℝ ↑m { 𝐴 } ) )
4		vonvolmbl2.y	⊢ 𝑌 = ∪ 𝑓 ∈ 𝑋 ran 𝑓
5	1 2 3 4	ssmapsn	⊢ ( 𝜑 → 𝑋 = ( 𝑌 ↑m { 𝐴 } ) )
6	5	eleq1d	⊢ ( 𝜑 → ( 𝑋 ∈ dom ( voln ‘ { 𝐴 } ) ↔ ( 𝑌 ↑m { 𝐴 } ) ∈ dom ( voln ‘ { 𝐴 } ) ) )
7	3	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → 𝑋 ⊆ ( ℝ ↑m { 𝐴 } ) )
8		simpr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → 𝑓 ∈ 𝑋 )
9	7 8	sseldd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → 𝑓 ∈ ( ℝ ↑m { 𝐴 } ) )
10		elmapi	⊢ ( 𝑓 ∈ ( ℝ ↑m { 𝐴 } ) → 𝑓 : { 𝐴 } ⟶ ℝ )
11		frn	⊢ ( 𝑓 : { 𝐴 } ⟶ ℝ → ran 𝑓 ⊆ ℝ )
12	9 10 11	3syl	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ran 𝑓 ⊆ ℝ )
13	12	ralrimiva	⊢ ( 𝜑 → ∀ 𝑓 ∈ 𝑋 ran 𝑓 ⊆ ℝ )
14		iunss	⊢ ( ∪ 𝑓 ∈ 𝑋 ran 𝑓 ⊆ ℝ ↔ ∀ 𝑓 ∈ 𝑋 ran 𝑓 ⊆ ℝ )
15	13 14	sylibr	⊢ ( 𝜑 → ∪ 𝑓 ∈ 𝑋 ran 𝑓 ⊆ ℝ )
16	4 15	eqsstrid	⊢ ( 𝜑 → 𝑌 ⊆ ℝ )
17	2 16	vonvolmbl	⊢ ( 𝜑 → ( ( 𝑌 ↑m { 𝐴 } ) ∈ dom ( voln ‘ { 𝐴 } ) ↔ 𝑌 ∈ dom vol ) )
18	6 17	bitrd	⊢ ( 𝜑 → ( 𝑋 ∈ dom ( voln ‘ { 𝐴 } ) ↔ 𝑌 ∈ dom vol ) )