Theorem issmfgtd

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

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

Proof

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