Theorem smfpimioompt

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	smfpimioompt.x	⊢ Ⅎ 𝑥 𝜑
	smfpimioompt.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	smfpimioompt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	smfpimioompt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
	smfpimioompt.m	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
	smfpimioompt.l	⊢ ( 𝜑 → 𝐿 ∈ ℝ* )
	smfpimioompt.r	⊢ ( 𝜑 → 𝑅 ∈ ℝ* )
Assertion	smfpimioompt	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) } ∈ ( 𝑆 ↾t 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		smfpimioompt.x	⊢ Ⅎ 𝑥 𝜑
2		smfpimioompt.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
3		smfpimioompt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4		smfpimioompt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
5		smfpimioompt.m	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
6		smfpimioompt.l	⊢ ( 𝜑 → 𝐿 ∈ ℝ* )
7		smfpimioompt.r	⊢ ( 𝜑 → 𝑅 ∈ ℝ* )
8		eqid	⊢ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
9	2 5 8	smff	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⟶ ℝ )
10		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
11	1 10 4	dmmptdf	⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
12	11	feq2d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⟶ ℝ ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℝ ) )
13	9 12	mpbid	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℝ )
14	13	fvmptelcdm	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
15	14	rexrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
16	1 6 7 15	pimiooltgt	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) } = ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) )
17		eqid	⊢ ( 𝑆 ↾t 𝐴 ) = ( 𝑆 ↾t 𝐴 )
18	2 3 17	subsalsal	⊢ ( 𝜑 → ( 𝑆 ↾t 𝐴 ) ∈ SAlg )
19	1 2 4 5 7	smfpimltxrmpt	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∈ ( 𝑆 ↾t 𝐴 ) )
20	1 2 4 5 6	smfpimgtxrmpt	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ∈ ( 𝑆 ↾t 𝐴 ) )
21	18 19 20	salincld	⊢ ( 𝜑 → ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ) ∈ ( 𝑆 ↾t 𝐴 ) )
22	16 21	eqeltrd	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝐿 (,) 𝑅 ) } ∈ ( 𝑆 ↾t 𝐴 ) )