# Metamath Proof Explorer

## 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 fvmptelrn ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℝ )
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 𝐴 ) )