Metamath Proof Explorer

Theorem smfdmmblpimne

Description: If a measurable function w.r.t. to a sigma-algebra has domain in the sigma-algebra, the set of elements that are not mapped to a given real, is in the sigma-algebra. (Contributed by Glauco Siliprandi, 5-Jan-2025)

Ref Expression
Hypotheses smfdmmblpimne.1 ⊢ Ⅎ x φ
smfdmmblpimne.2 ⊢ Ⅎ _ x A
smfdmmblpimne.3 ⊢ φ → S ∈ SAlg
smfdmmblpimne.4 ⊢ φ → A ∈ S
smfdmmblpimne.5 ⊢ φ ∧ x ∈ A → B ∈ ℝ
smfdmmblpimne.6 ⊢ φ → x ∈ A ⟼ B ∈ SMblFn ⁡ S
smfdmmblpimne.7 ⊢ φ → C ∈ ℝ
smfdmmblpimne.8 ⊢ D = x ∈ A | B ≠ C
Assertion smfdmmblpimne ⊢ φ → D ∈ S

Proof

Step Hyp Ref Expression
1 smfdmmblpimne.1 ⊢ Ⅎ x φ
2 smfdmmblpimne.2 ⊢ Ⅎ _ x A
3 smfdmmblpimne.3 ⊢ φ → S ∈ SAlg
4 smfdmmblpimne.4 ⊢ φ → A ∈ S
5 smfdmmblpimne.5 ⊢ φ ∧ x ∈ A → B ∈ ℝ
6 smfdmmblpimne.6 ⊢ φ → x ∈ A ⟼ B ∈ SMblFn ⁡ S
7 smfdmmblpimne.7 ⊢ φ → C ∈ ℝ
8 smfdmmblpimne.8 ⊢ D = x ∈ A | B ≠ C
9 5 rexrd ⊢ φ ∧ x ∈ A → B ∈ ℝ *
10 7 rexrd ⊢ φ → C ∈ ℝ *
11 10 adantr ⊢ φ ∧ x ∈ A → C ∈ ℝ *
12 1 9 11 pimxrneun ⊢ φ → x ∈ A | B ≠ C = x ∈ A | B < C ∪ x ∈ A | C < B
13 8 12 eqtrid ⊢ φ → D = x ∈ A | B < C ∪ x ∈ A | C < B
14 3 4 salrestss ⊢ φ → S ↾ 𝑡 A ⊆ S
15 1 2 3 5 6 10 smfpimltxrmptf ⊢ φ → x ∈ A | B < C ∈ S ↾ 𝑡 A
16 14 15 sseldd ⊢ φ → x ∈ A | B < C ∈ S
17 1 2 3 5 6 10 smfpimgtxrmptf ⊢ φ → x ∈ A | C < B ∈ S ↾ 𝑡 A
18 14 17 sseldd ⊢ φ → x ∈ A | C < B ∈ S
19 3 16 18 saluncld ⊢ φ → x ∈ A | B < C ∪ x ∈ A | C < B ∈ S
20 13 19 eqeltrd ⊢ φ → D ∈ S