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

Proof

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