Theorem issmfdf

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	issmfdf.x	⊢ Ⅎ 𝑥 𝐹
	issmfdf.a	⊢ Ⅎ 𝑎 𝜑
	issmfdf.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	issmfdf.d	⊢ ( 𝜑 → 𝐷 ⊆ ∪ 𝑆 )
	issmfdf.f	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℝ )
	issmfdf.p	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) )
Assertion	issmfdf	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )

Proof

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