# Metamath Proof Explorer

## Theorem smfpimgtxrmpt

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

Ref Expression
Hypotheses smfpimgtxrmpt.x 𝑥 𝜑
smfpimgtxrmpt.s ( 𝜑𝑆 ∈ SAlg )
smfpimgtxrmpt.b ( ( 𝜑𝑥𝐴 ) → 𝐵𝑉 )
smfpimgtxrmpt.f ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
smfpimgtxrmpt.l ( 𝜑𝐿 ∈ ℝ* )
Assertion smfpimgtxrmpt ( 𝜑 → { 𝑥𝐴𝐿 < 𝐵 } ∈ ( 𝑆t 𝐴 ) )

### Proof

Step Hyp Ref Expression
1 smfpimgtxrmpt.x 𝑥 𝜑
2 smfpimgtxrmpt.s ( 𝜑𝑆 ∈ SAlg )
3 smfpimgtxrmpt.b ( ( 𝜑𝑥𝐴 ) → 𝐵𝑉 )
4 smfpimgtxrmpt.f ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
5 smfpimgtxrmpt.l ( 𝜑𝐿 ∈ ℝ* )
6 nfmpt1 𝑥 ( 𝑥𝐴𝐵 )
7 6 nfdm 𝑥 dom ( 𝑥𝐴𝐵 )
8 nfcv 𝑦 dom ( 𝑥𝐴𝐵 )
9 nfv 𝑦 𝐿 < ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 )
10 nfcv 𝑥 𝐿
11 nfcv 𝑥 <
12 nfcv 𝑥 𝑦
13 6 12 nffv 𝑥 ( ( 𝑥𝐴𝐵 ) ‘ 𝑦 )
14 10 11 13 nfbr 𝑥 𝐿 < ( ( 𝑥𝐴𝐵 ) ‘ 𝑦 )
15 fveq2 ( 𝑥 = 𝑦 → ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) = ( ( 𝑥𝐴𝐵 ) ‘ 𝑦 ) )
16 15 breq2d ( 𝑥 = 𝑦 → ( 𝐿 < ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) ↔ 𝐿 < ( ( 𝑥𝐴𝐵 ) ‘ 𝑦 ) ) )
17 7 8 9 14 16 cbvrabw { 𝑥 ∈ dom ( 𝑥𝐴𝐵 ) ∣ 𝐿 < ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) } = { 𝑦 ∈ dom ( 𝑥𝐴𝐵 ) ∣ 𝐿 < ( ( 𝑥𝐴𝐵 ) ‘ 𝑦 ) }
18 17 a1i ( 𝜑 → { 𝑥 ∈ dom ( 𝑥𝐴𝐵 ) ∣ 𝐿 < ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) } = { 𝑦 ∈ dom ( 𝑥𝐴𝐵 ) ∣ 𝐿 < ( ( 𝑥𝐴𝐵 ) ‘ 𝑦 ) } )
19 nfcv 𝑦 ( 𝑥𝐴𝐵 )
20 eqid dom ( 𝑥𝐴𝐵 ) = dom ( 𝑥𝐴𝐵 )
21 19 2 4 20 5 smfpimgtxr ( 𝜑 → { 𝑦 ∈ dom ( 𝑥𝐴𝐵 ) ∣ 𝐿 < ( ( 𝑥𝐴𝐵 ) ‘ 𝑦 ) } ∈ ( 𝑆t dom ( 𝑥𝐴𝐵 ) ) )
22 18 21 eqeltrd ( 𝜑 → { 𝑥 ∈ dom ( 𝑥𝐴𝐵 ) ∣ 𝐿 < ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) } ∈ ( 𝑆t dom ( 𝑥𝐴𝐵 ) ) )
23 eqid ( 𝑥𝐴𝐵 ) = ( 𝑥𝐴𝐵 )
24 1 23 3 dmmptdf ( 𝜑 → dom ( 𝑥𝐴𝐵 ) = 𝐴 )
25 nfcv 𝑥 𝐴
26 7 25 rabeqf ( dom ( 𝑥𝐴𝐵 ) = 𝐴 → { 𝑥 ∈ dom ( 𝑥𝐴𝐵 ) ∣ 𝐿 < ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) } = { 𝑥𝐴𝐿 < ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) } )
27 24 26 syl ( 𝜑 → { 𝑥 ∈ dom ( 𝑥𝐴𝐵 ) ∣ 𝐿 < ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) } = { 𝑥𝐴𝐿 < ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) } )
28 23 a1i ( 𝜑 → ( 𝑥𝐴𝐵 ) = ( 𝑥𝐴𝐵 ) )
29 28 3 fvmpt2d ( ( 𝜑𝑥𝐴 ) → ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) = 𝐵 )
30 29 breq2d ( ( 𝜑𝑥𝐴 ) → ( 𝐿 < ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) ↔ 𝐿 < 𝐵 ) )
31 1 30 rabbida ( 𝜑 → { 𝑥𝐴𝐿 < ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) } = { 𝑥𝐴𝐿 < 𝐵 } )
32 eqidd ( 𝜑 → { 𝑥𝐴𝐿 < 𝐵 } = { 𝑥𝐴𝐿 < 𝐵 } )
33 27 31 32 3eqtrrd ( 𝜑 → { 𝑥𝐴𝐿 < 𝐵 } = { 𝑥 ∈ dom ( 𝑥𝐴𝐵 ) ∣ 𝐿 < ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) } )
34 24 eqcomd ( 𝜑𝐴 = dom ( 𝑥𝐴𝐵 ) )
35 34 oveq2d ( 𝜑 → ( 𝑆t 𝐴 ) = ( 𝑆t dom ( 𝑥𝐴𝐵 ) ) )
36 33 35 eleq12d ( 𝜑 → ( { 𝑥𝐴𝐿 < 𝐵 } ∈ ( 𝑆t 𝐴 ) ↔ { 𝑥 ∈ dom ( 𝑥𝐴𝐵 ) ∣ 𝐿 < ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) } ∈ ( 𝑆t dom ( 𝑥𝐴𝐵 ) ) ) )
37 22 36 mpbird ( 𝜑 → { 𝑥𝐴𝐿 < 𝐵 } ∈ ( 𝑆t 𝐴 ) )