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	$⊢ \underline{Ⅎ} x F$
	smfsupdmmbl.4	$⊢ φ \to M \in ℤ$
	smfsupdmmbl.5	$⊢ Z = ℤ_{\geq M}$
	smfsupdmmbl.6	$⊢ φ \to S \in SAlg$
	smfsupdmmbl.7	$⊢ φ \to F : Z ⟶ SMblFn (S)$
	smfsupdmmbl.8	$⊢ (φ \land n \in Z) \to dom F (n) \in S$
	smfsupdmmbl.9	$⊢ D = \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z F (n) (x) \leq y\}$
	smfsupdmmbl.10	$⊢ G = (x \in D ⟼ sup (ran (n \in Z ⟼ F (n) (x)) ℝ <))$
Assertion	smfsupdmmbl	$⊢ φ \to dom G \in S$

Proof

Step	Hyp	Ref	Expression
1		smfsupdmmbl.1	$⊢ Ⅎ n φ$
2		smfsupdmmbl.2	$⊢ Ⅎ x φ$
3		smfsupdmmbl.3	$⊢ \underline{Ⅎ} x F$
4		smfsupdmmbl.4	$⊢ φ \to M \in ℤ$
5		smfsupdmmbl.5	$⊢ Z = ℤ_{\geq M}$
6		smfsupdmmbl.6	$⊢ φ \to S \in SAlg$
7		smfsupdmmbl.7	$⊢ φ \to F : Z ⟶ SMblFn (S)$
8		smfsupdmmbl.8	$⊢ (φ \land n \in Z) \to dom F (n) \in S$
9		smfsupdmmbl.9	$⊢ D = \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z F (n) (x) \leq y\}$
10		smfsupdmmbl.10	$⊢ G = (x \in D ⟼ sup (ran (n \in Z ⟼ F (n) (x)) ℝ <))$
11		nfv	$⊢ Ⅎ m φ$
12		eqid	$⊢ (n \in Z ⟼ (m \in ℕ ⟼ \{x \in dom F (n) \| F (n) (x) < m\})) = (n \in Z ⟼ (m \in ℕ ⟼ \{x \in dom F (n) \| F (n) (x) < m\}))$
13	1 2 11 3 4 5 6 7 8 9 12 10	smfsupdmmbllem	$⊢ φ \to dom G \in S$

Metamath Proof Explorer

Theorem smfsupdmmbl

Proof