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

Proof

Step Hyp Ref Expression
1 smfpimltmpt.x ⊢ Ⅎ x φ
2 smfpimltmpt.s ⊢ φ → S ∈ SAlg
3 smfpimltmpt.b ⊢ φ ∧ x ∈ A → B ∈ V
4 smfpimltmpt.f ⊢ φ → x ∈ A ⟼ B ∈ SMblFn ⁡ S
5 smfpimltmpt.r ⊢ φ → R ∈ ℝ
6 nfmpt1 ⊢ Ⅎ _ x x ∈ A ⟼ B
7 eqid ⊢ dom ⁡ x ∈ A ⟼ B = dom ⁡ x ∈ A ⟼ B
8 6 2 4 7 5 smfpreimaltf ⊢ φ → x ∈ dom ⁡ x ∈ A ⟼ B | x ∈ A ⟼ B ⁡ x < R ∈ 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 ⊢ Ⅎ _ x dom ⁡ x ∈ A ⟼ B
12 nfcv ⊢ Ⅎ _ x A
13 11 12 rabeqf ⊢ dom ⁡ x ∈ A ⟼ B = A → x ∈ dom ⁡ x ∈ A ⟼ B | x ∈ A ⟼ B ⁡ x < R = x ∈ A | x ∈ A ⟼ B ⁡ x < R
14 10 13 syl ⊢ φ → x ∈ dom ⁡ x ∈ A ⟼ B | x ∈ A ⟼ B ⁡ x < R = x ∈ A | x ∈ A ⟼ B ⁡ x < R
15 9 a1i ⊢ φ → x ∈ A ⟼ B = x ∈ A ⟼ B
16 15 3 fvmpt2d ⊢ φ ∧ x ∈ A → x ∈ A ⟼ B ⁡ x = B
17 16 breq1d ⊢ φ ∧ x ∈ A → x ∈ A ⟼ B ⁡ x < R ↔ B < R
18 1 17 rabbida ⊢ φ → x ∈ A | x ∈ A ⟼ B ⁡ x < R = x ∈ A | B < R
19 eqidd ⊢ φ → x ∈ A | B < R = x ∈ A | B < R
20 14 18 19 3eqtrrd ⊢ φ → x ∈ A | B < R = x ∈ dom ⁡ x ∈ A ⟼ B | x ∈ A ⟼ B ⁡ x < R
21 10 eqcomd ⊢ φ → A = dom ⁡ x ∈ A ⟼ B
22 21 oveq2d ⊢ φ → S ↾ 𝑡 A = S ↾ 𝑡 dom ⁡ x ∈ A ⟼ B
23 20 22 eleq12d ⊢ φ → x ∈ A | B < R ∈ S ↾ 𝑡 A ↔ x ∈ dom ⁡ x ∈ A ⟼ B | x ∈ A ⟼ B ⁡ x < R ∈ S ↾ 𝑡 dom ⁡ x ∈ A ⟼ B
24 8 23 mpbird ⊢ φ → x ∈ A | B < R ∈ S ↾ 𝑡 A