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	⊢ Ⅎ 𝑛 𝜑
	smfsupdmmbl.2	⊢ Ⅎ 𝑥 𝜑
	smfsupdmmbl.3	⊢ Ⅎ 𝑥 𝐹
	smfsupdmmbl.4	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	smfsupdmmbl.5	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	smfsupdmmbl.6	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	smfsupdmmbl.7	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
	smfsupdmmbl.8	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → dom ( 𝐹 ‘ 𝑛 ) ∈ 𝑆 )
	smfsupdmmbl.9	⊢ 𝐷 = { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 }
	smfsupdmmbl.10	⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
Assertion	smfsupdmmbl	⊢ ( 𝜑 → dom 𝐺 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		smfsupdmmbl.1	⊢ Ⅎ 𝑛 𝜑
2		smfsupdmmbl.2	⊢ Ⅎ 𝑥 𝜑
3		smfsupdmmbl.3	⊢ Ⅎ 𝑥 𝐹
4		smfsupdmmbl.4	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
5		smfsupdmmbl.5	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
6		smfsupdmmbl.6	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
7		smfsupdmmbl.7	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
8		smfsupdmmbl.8	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → dom ( 𝐹 ‘ 𝑛 ) ∈ 𝑆 )
9		smfsupdmmbl.9	⊢ 𝐷 = { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 }
10		smfsupdmmbl.10	⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
11		nfv	⊢ Ⅎ 𝑚 𝜑
12		eqid	⊢ ( 𝑛 ∈ 𝑍 ↦ ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < 𝑚 } ) ) = ( 𝑛 ∈ 𝑍 ↦ ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < 𝑚 } ) )
13	1 2 11 3 4 5 6 7 8 9 12 10	smfsupdmmbllem	⊢ ( 𝜑 → dom 𝐺 ∈ 𝑆 )