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 ⊢ Ⅎ _ x x ∈ 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 ⊢ Ⅎ _ x dom ⁡ x ∈ A ⟼ B
12 nfcv ⊢ Ⅎ _ x A
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