Metamath Proof Explorer

Theorem smfsupdmmbl

Description: If a countable set of sigma-measurable functions have domains in the sigma-algebra, then their supremum function has the domain in the sigma-algebra. This is the fourth statement of Proposition 121H of Fremlin1 p. 39 . (Contributed by Glauco Siliprandi, 24-Jan-2025)

Ref Expression
Hypotheses smfsupdmmbl.1 ⊢ Ⅎ n φ
smfsupdmmbl.2 ⊢ Ⅎ x φ
smfsupdmmbl.3 ⊢ Ⅎ _ x F
smfsupdmmbl.4 ⊢ φ → M ∈ ℤ
smfsupdmmbl.5 ⊢ Z = ℤ ≥ M
smfsupdmmbl.6 ⊢ φ → S ∈ SAlg
smfsupdmmbl.7 ⊢ φ → F : Z ⟶ SMblFn ⁡ S
smfsupdmmbl.8 ⊢ φ ∧ n ∈ Z → dom ⁡ F ⁡ n ∈ S
smfsupdmmbl.9 ⊢ D = x ∈ ⋂ n ∈ Z dom ⁡ F ⁡ n | ∃ y ∈ ℝ ∀ n ∈ Z F ⁡ n ⁡ x ≤ y
smfsupdmmbl.10 ⊢ G = x ∈ D ⟼ sup ran ⁡ n ∈ Z ⟼ F ⁡ n ⁡ x ℝ <
Assertion smfsupdmmbl ⊢ φ → dom ⁡ G ∈ S

Proof

Step Hyp Ref Expression
1 smfsupdmmbl.1 ⊢ Ⅎ n φ
2 smfsupdmmbl.2 ⊢ Ⅎ x φ
3 smfsupdmmbl.3 ⊢ Ⅎ _ x F
4 smfsupdmmbl.4 ⊢ φ → M ∈ ℤ
5 smfsupdmmbl.5 ⊢ Z = ℤ ≥ M
6 smfsupdmmbl.6 ⊢ φ → S ∈ SAlg
7 smfsupdmmbl.7 ⊢ φ → F : Z ⟶ SMblFn ⁡ S
8 smfsupdmmbl.8 ⊢ φ ∧ n ∈ Z → dom ⁡ F ⁡ n ∈ S
9 smfsupdmmbl.9 ⊢ D = x ∈ ⋂ n ∈ Z dom ⁡ F ⁡ n | ∃ y ∈ ℝ ∀ n ∈ Z F ⁡ n ⁡ x ≤ y
10 smfsupdmmbl.10 ⊢ G = x ∈ D ⟼ sup ran ⁡ n ∈ Z ⟼ F ⁡ n ⁡ x ℝ <
11 nfv ⊢ Ⅎ m φ
12 eqid ⊢ n ∈ Z ⟼ m ∈ ℕ ⟼ x ∈ dom ⁡ F ⁡ n | F ⁡ n ⁡ x < m = n ∈ Z ⟼ m ∈ ℕ ⟼ x ∈ dom ⁡ F ⁡ n | F ⁡ n ⁡ x < m
13 1 2 11 3 4 5 6 7 8 9 12 10 smfsupdmmbllem ⊢ φ → dom ⁡ G ∈ S