Theorem issmfdmpt

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	issmfdmpt.x	⊢ Ⅎ 𝑥 𝜑
	issmfdmpt.a	⊢ Ⅎ 𝑎 𝜑
	issmfdmpt.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	issmfdmpt.i	⊢ ( 𝜑 → 𝐴 ⊆ ∪ 𝑆 )
	issmfdmpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
	issmfdmpt.p	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑎 } ∈ ( 𝑆 ↾t 𝐴 ) )
Assertion	issmfdmpt	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		issmfdmpt.x	⊢ Ⅎ 𝑥 𝜑
2		issmfdmpt.a	⊢ Ⅎ 𝑎 𝜑
3		issmfdmpt.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
4		issmfdmpt.i	⊢ ( 𝜑 → 𝐴 ⊆ ∪ 𝑆 )
5		issmfdmpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
6		issmfdmpt.p	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑎 } ∈ ( 𝑆 ↾t 𝐴 ) )
7		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
8		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
9	1 5 8	fmptdf	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℝ )
10		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
11	10 5	fvmpt2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
12	11	breq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) < 𝑎 ↔ 𝐵 < 𝑎 ) )
13	12	ex	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) < 𝑎 ↔ 𝐵 < 𝑎 ) ) )
14	1 13	ralrimi	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) < 𝑎 ↔ 𝐵 < 𝑎 ) )
15		rabbi	⊢ ( ∀ 𝑥 ∈ 𝐴 ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) < 𝑎 ↔ 𝐵 < 𝑎 ) ↔ { 𝑥 ∈ 𝐴 ∣ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) < 𝑎 } = { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑎 } )
16	14 15	sylib	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) < 𝑎 } = { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑎 } )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ 𝐴 ∣ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) < 𝑎 } = { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑎 } )
18	17 6	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ 𝐴 ∣ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐴 ) )
19	7 2 3 4 9 18	issmfdf	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )