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 𝐴 ) )