Metamath Proof Explorer

Theorem smfpimgtmpt

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 smfpimgtmpt.x ⊢Ⅎxφ
smfpimgtmpt.s ⊢φ→S∈SAlg
smfpimgtmpt.b ⊢φ∧x∈A→B∈V
smfpimgtmpt.f ⊢φ→x∈A⟼B∈SMblFn⁡S
smfpimgtmpt.l ⊢φ→L∈ℝ
Assertion smfpimgtmpt ⊢φ→x∈A|L<B∈S↾𝑡A

Proof

Step Hyp Ref Expression
1 smfpimgtmpt.x ⊢Ⅎxφ
2 smfpimgtmpt.s ⊢φ→S∈SAlg
3 smfpimgtmpt.b ⊢φ∧x∈A→B∈V
4 smfpimgtmpt.f ⊢φ→x∈A⟼B∈SMblFn⁡S
5 smfpimgtmpt.l ⊢φ→L∈ℝ
6 nfmpt1 ⊢Ⅎ_xx∈A⟼B
7 eqid ⊢dom⁡x∈A⟼B=dom⁡x∈A⟼B
8 6 2 4 7 5 smfpreimagtf ⊢φ→x∈dom⁡x∈A⟼B|L<x∈A⟼B⁡x∈S↾𝑡dom⁡x∈A⟼B
9 eqid ⊢x∈A⟼B=x∈A⟼B
10 1 9 3 dmmptdf ⊢φ→dom⁡x∈A⟼B=A
11 6 nfdm ⊢Ⅎ_xdom⁡x∈A⟼B
12 nfcv ⊢Ⅎ_xA
13 11 12 rabeqf ⊢dom⁡x∈A⟼B=A→x∈dom⁡x∈A⟼B|L<x∈A⟼B⁡x=x∈A|L<x∈A⟼B⁡x
14 10 13 syl ⊢φ→x∈dom⁡x∈A⟼B|L<x∈A⟼B⁡x=x∈A|L<x∈A⟼B⁡x
15 9 a1i ⊢φ→x∈A⟼B=x∈A⟼B
16 15 3 fvmpt2d ⊢φ∧x∈A→x∈A⟼B⁡x=B
17 16 breq2d ⊢φ∧x∈A→L<x∈A⟼B⁡x↔L<B
18 1 17 rabbida ⊢φ→x∈A|L<x∈A⟼B⁡x=x∈A|L<B
19 eqidd ⊢φ→x∈A|L<B=x∈A|L<B
20 14 18 19 3eqtrrd ⊢φ→x∈A|L<B=x∈dom⁡x∈A⟼B|L<x∈A⟼B⁡x
21 10 eqcomd ⊢φ→A=dom⁡x∈A⟼B
22 21 oveq2d ⊢φ→S↾𝑡A=S↾𝑡dom⁡x∈A⟼B
23 20 22 eleq12d ⊢φ→x∈A|L<B∈S↾𝑡A↔x∈dom⁡x∈A⟼B|L<x∈A⟼B⁡x∈S↾𝑡dom⁡x∈A⟼B
24 8 23 mpbird ⊢φ→x∈A|L<B∈S↾𝑡A