Metamath Proof Explorer


Theorem smfpimltmpt

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

Ref Expression
Hypotheses smfpimltmpt.x 𝑥 𝜑
smfpimltmpt.s ( 𝜑𝑆 ∈ SAlg )
smfpimltmpt.b ( ( 𝜑𝑥𝐴 ) → 𝐵𝑉 )
smfpimltmpt.f ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
smfpimltmpt.r ( 𝜑𝑅 ∈ ℝ )
Assertion smfpimltmpt ( 𝜑 → { 𝑥𝐴𝐵 < 𝑅 } ∈ ( 𝑆t 𝐴 ) )

Proof

Step Hyp Ref Expression
1 smfpimltmpt.x 𝑥 𝜑
2 smfpimltmpt.s ( 𝜑𝑆 ∈ SAlg )
3 smfpimltmpt.b ( ( 𝜑𝑥𝐴 ) → 𝐵𝑉 )
4 smfpimltmpt.f ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
5 smfpimltmpt.r ( 𝜑𝑅 ∈ ℝ )
6 nfmpt1 𝑥 ( 𝑥𝐴𝐵 )
7 eqid dom ( 𝑥𝐴𝐵 ) = dom ( 𝑥𝐴𝐵 )
8 6 2 4 7 5 smfpreimaltf ( 𝜑 → { 𝑥 ∈ dom ( 𝑥𝐴𝐵 ) ∣ ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) < 𝑅 } ∈ ( 𝑆t dom ( 𝑥𝐴𝐵 ) ) )
9 eqid ( 𝑥𝐴𝐵 ) = ( 𝑥𝐴𝐵 )
10 1 9 3 dmmptdf ( 𝜑 → dom ( 𝑥𝐴𝐵 ) = 𝐴 )
11 6 nfdm 𝑥 dom ( 𝑥𝐴𝐵 )
12 nfcv 𝑥 𝐴
13 11 12 rabeqf ( dom ( 𝑥𝐴𝐵 ) = 𝐴 → { 𝑥 ∈ dom ( 𝑥𝐴𝐵 ) ∣ ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) < 𝑅 } = { 𝑥𝐴 ∣ ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) < 𝑅 } )
14 10 13 syl ( 𝜑 → { 𝑥 ∈ dom ( 𝑥𝐴𝐵 ) ∣ ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) < 𝑅 } = { 𝑥𝐴 ∣ ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) < 𝑅 } )
15 9 a1i ( 𝜑 → ( 𝑥𝐴𝐵 ) = ( 𝑥𝐴𝐵 ) )
16 15 3 fvmpt2d ( ( 𝜑𝑥𝐴 ) → ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) = 𝐵 )
17 16 breq1d ( ( 𝜑𝑥𝐴 ) → ( ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) < 𝑅𝐵 < 𝑅 ) )
18 1 17 rabbida ( 𝜑 → { 𝑥𝐴 ∣ ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) < 𝑅 } = { 𝑥𝐴𝐵 < 𝑅 } )
19 eqidd ( 𝜑 → { 𝑥𝐴𝐵 < 𝑅 } = { 𝑥𝐴𝐵 < 𝑅 } )
20 14 18 19 3eqtrrd ( 𝜑 → { 𝑥𝐴𝐵 < 𝑅 } = { 𝑥 ∈ dom ( 𝑥𝐴𝐵 ) ∣ ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) < 𝑅 } )
21 10 eqcomd ( 𝜑𝐴 = dom ( 𝑥𝐴𝐵 ) )
22 21 oveq2d ( 𝜑 → ( 𝑆t 𝐴 ) = ( 𝑆t dom ( 𝑥𝐴𝐵 ) ) )
23 20 22 eleq12d ( 𝜑 → ( { 𝑥𝐴𝐵 < 𝑅 } ∈ ( 𝑆t 𝐴 ) ↔ { 𝑥 ∈ dom ( 𝑥𝐴𝐵 ) ∣ ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) < 𝑅 } ∈ ( 𝑆t dom ( 𝑥𝐴𝐵 ) ) ) )
24 8 23 mpbird ( 𝜑 → { 𝑥𝐴𝐵 < 𝑅 } ∈ ( 𝑆t 𝐴 ) )