Metamath Proof Explorer

Theorem smfinfdmmbl

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

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

Proof

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