Theorem issmfd

Description: A sufficient condition for " F being a real-valued measurable function w.r.t. to the sigma-algebra S ". (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	issmfd.a	⊢ Ⅎ 𝑎 𝜑
	issmfd.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	issmfd.d	⊢ ( 𝜑 → 𝐷 ⊆ ∪ 𝑆 )
	issmfd.f	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℝ )
	issmfd.p	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) )
Assertion	issmfd	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		issmfd.a	⊢ Ⅎ 𝑎 𝜑
2		issmfd.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
3		issmfd.d	⊢ ( 𝜑 → 𝐷 ⊆ ∪ 𝑆 )
4		issmfd.f	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℝ )
5		issmfd.p	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) )
6	4	fdmd	⊢ ( 𝜑 → dom 𝐹 = 𝐷 )
7	6 3	eqsstrd	⊢ ( 𝜑 → dom 𝐹 ⊆ ∪ 𝑆 )
8	4	ffdmd	⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ℝ )
9	6	rabeqdv	⊢ ( 𝜑 → { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } )
10	6	oveq2d	⊢ ( 𝜑 → ( 𝑆 ↾t dom 𝐹 ) = ( 𝑆 ↾t 𝐷 ) )
11	9 10	eleq12d	⊢ ( 𝜑 → ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t dom 𝐹 ) ↔ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) )
12	11	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t dom 𝐹 ) ↔ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) )
13	5 12	mpbird	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t dom 𝐹 ) )
14	13	ex	⊢ ( 𝜑 → ( 𝑎 ∈ ℝ → { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t dom 𝐹 ) ) )
15	1 14	ralrimi	⊢ ( 𝜑 → ∀ 𝑎 ∈ ℝ { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t dom 𝐹 ) )
16	7 8 15	3jca	⊢ ( 𝜑 → ( dom 𝐹 ⊆ ∪ 𝑆 ∧ 𝐹 : dom 𝐹 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t dom 𝐹 ) ) )
17		eqid	⊢ dom 𝐹 = dom 𝐹
18	2 17	issmf	⊢ ( 𝜑 → ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ↔ ( dom 𝐹 ⊆ ∪ 𝑆 ∧ 𝐹 : dom 𝐹 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t dom 𝐹 ) ) ) )
19	16 18	mpbird	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )