Theorem smfpimioo

Description: Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	smfpimioo.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	smfpimioo.f	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
	smfpimioo.d	⊢ 𝐷 = dom 𝐹
	smfpimioo.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
	smfpimioo.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
Assertion	smfpimioo	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( 𝐴 (,) 𝐵 ) ) ∈ ( 𝑆 ↾t 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		smfpimioo.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
2		smfpimioo.f	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
3		smfpimioo.d	⊢ 𝐷 = dom 𝐹
4		smfpimioo.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
5		smfpimioo.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
6	1 2 3	smff	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℝ )
7	6	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑥 ) ) )
8	7	cnveqd	⊢ ( 𝜑 → ◡ 𝐹 = ◡ ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑥 ) ) )
9	8	imaeq1d	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( 𝐴 (,) 𝐵 ) ) = ( ◡ ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑥 ) ) “ ( 𝐴 (,) 𝐵 ) ) )
10		eqid	⊢ ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑥 ) )
11	10	mptpreima	⊢ ( ◡ ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑥 ) ) “ ( 𝐴 (,) 𝐵 ) ) = { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 (,) 𝐵 ) }
12	11	a1i	⊢ ( 𝜑 → ( ◡ ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑥 ) ) “ ( 𝐴 (,) 𝐵 ) ) = { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 (,) 𝐵 ) } )
13	9 12	eqtrd	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( 𝐴 (,) 𝐵 ) ) = { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 (,) 𝐵 ) } )
14		nfv	⊢ Ⅎ 𝑥 𝜑
15	1	uniexd	⊢ ( 𝜑 → ∪ 𝑆 ∈ V )
16	1 2 3	smfdmss	⊢ ( 𝜑 → 𝐷 ⊆ ∪ 𝑆 )
17	15 16	ssexd	⊢ ( 𝜑 → 𝐷 ∈ V )
18	6	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
19	7 2	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ ( SMblFn ‘ 𝑆 ) )
20	14 1 17 18 19 4 5	smfpimioompt	⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 (,) 𝐵 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
21	13 20	eqeltrd	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( 𝐴 (,) 𝐵 ) ) ∈ ( 𝑆 ↾t 𝐷 ) )