Metamath Proof Explorer

Theorem issmfdf

Description: A sufficient condition for " F being a measurable function w.r.t. to the sigma-algebra S ". (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses issmfdf.x ⊢ Ⅎ _ x F
issmfdf.a ⊢ Ⅎ a φ
issmfdf.s ⊢ φ → S ∈ SAlg
issmfdf.d ⊢ φ → D ⊆ ⋃ S
issmfdf.f ⊢ φ → F : D ⟶ ℝ
issmfdf.p ⊢ φ ∧ a ∈ ℝ → x ∈ D | F ⁡ x < a ∈ S ↾ 𝑡 D
Assertion issmfdf ⊢ φ → F ∈ SMblFn ⁡ S

Proof

Step Hyp Ref Expression
1 issmfdf.x ⊢ Ⅎ _ x F
2 issmfdf.a ⊢ Ⅎ a φ
3 issmfdf.s ⊢ φ → S ∈ SAlg
4 issmfdf.d ⊢ φ → D ⊆ ⋃ S
5 issmfdf.f ⊢ φ → F : D ⟶ ℝ
6 issmfdf.p ⊢ φ ∧ a ∈ ℝ → x ∈ D | F ⁡ x < a ∈ S ↾ 𝑡 D
7 5 fdmd ⊢ φ → dom ⁡ F = D
8 7 4 eqsstrd ⊢ φ → dom ⁡ F ⊆ ⋃ S
9 5 ffdmd ⊢ φ → F : dom ⁡ F ⟶ ℝ
10 1 nfdm ⊢ Ⅎ _ x dom ⁡ F
11 nfcv ⊢ Ⅎ _ x D
12 10 11 rabeqf ⊢ dom ⁡ F = D → x ∈ dom ⁡ F | F ⁡ x < a = x ∈ D | F ⁡ x < a
13 7 12 syl ⊢ φ → x ∈ dom ⁡ F | F ⁡ x < a = x ∈ D | F ⁡ x < a
14 7 oveq2d ⊢ φ → S ↾ 𝑡 dom ⁡ F = S ↾ 𝑡 D
15 13 14 eleq12d ⊢ φ → x ∈ dom ⁡ F | F ⁡ x < a ∈ S ↾ 𝑡 dom ⁡ F ↔ x ∈ D | F ⁡ x < a ∈ S ↾ 𝑡 D
16 15 adantr ⊢ φ ∧ a ∈ ℝ → x ∈ dom ⁡ F | F ⁡ x < a ∈ S ↾ 𝑡 dom ⁡ F ↔ x ∈ D | F ⁡ x < a ∈ S ↾ 𝑡 D
17 6 16 mpbird ⊢ φ ∧ a ∈ ℝ → x ∈ dom ⁡ F | F ⁡ x < a ∈ S ↾ 𝑡 dom ⁡ F
18 17 ex ⊢ φ → a ∈ ℝ → x ∈ dom ⁡ F | F ⁡ x < a ∈ S ↾ 𝑡 dom ⁡ F
19 2 18 ralrimi ⊢ φ → ∀ a ∈ ℝ x ∈ dom ⁡ F | F ⁡ x < a ∈ S ↾ 𝑡 dom ⁡ F
20 8 9 19 3jca ⊢ φ → dom ⁡ F ⊆ ⋃ S ∧ F : dom ⁡ F ⟶ ℝ ∧ ∀ a ∈ ℝ x ∈ dom ⁡ F | F ⁡ x < a ∈ S ↾ 𝑡 dom ⁡ F
21 eqid ⊢ dom ⁡ F = dom ⁡ F
22 1 3 21 issmff ⊢ φ → F ∈ SMblFn ⁡ S ↔ dom ⁡ F ⊆ ⋃ S ∧ F : dom ⁡ F ⟶ ℝ ∧ ∀ a ∈ ℝ x ∈ dom ⁡ F | F ⁡ x < a ∈ S ↾ 𝑡 dom ⁡ F
23 20 22 mpbird ⊢ φ → F ∈ SMblFn ⁡ S