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 ⊢ Ⅎ 𝑥 𝜑
smfpimgtmpt.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
smfpimgtmpt.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
smfpimgtmpt.f ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
smfpimgtmpt.l ⊢ ( 𝜑 → 𝐿 ∈ ℝ )
Assertion smfpimgtmpt ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵 } ∈ ( 𝑆 ↾t 𝐴 ) )

Proof

Step Hyp Ref Expression
1 smfpimgtmpt.x ⊢ Ⅎ 𝑥 𝜑
2 smfpimgtmpt.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
3 smfpimgtmpt.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
4 smfpimgtmpt.f ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
5 smfpimgtmpt.l ⊢ ( 𝜑 → 𝐿 ∈ ℝ )
6 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
7 eqid ⊢ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
8 6 2 4 7 5 smfpreimagtf ⊢ ( 𝜑 → { 𝑥 ∈ 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 breq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐿 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ↔ 𝐿 < 𝐵 ) )
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 𝐴 ) )