Theorem smfinfdmmbllem

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

Proof

Step	Hyp	Ref	Expression
1		smfinfdmmbllem.1	⊢ Ⅎ 𝑛 𝜑
2		smfinfdmmbllem.2	⊢ Ⅎ 𝑥 𝜑
3		smfinfdmmbllem.3	⊢ Ⅎ 𝑚 𝜑
4		smfinfdmmbllem.4	⊢ Ⅎ 𝑥 𝐹
5		smfinfdmmbllem.5	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
6		smfinfdmmbllem.6	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
7		smfinfdmmbllem.7	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
8		smfinfdmmbllem.8	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
9		smfinfdmmbllem.9	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → dom ( 𝐹 ‘ 𝑛 ) ∈ 𝑆 )
10		smfinfdmmbllem.10	⊢ 𝐷 = { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) }
11		smfinfdmmbllem.11	⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ inf ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
12		smfinfdmmbllem.12	⊢ 𝐻 = ( 𝑛 ∈ 𝑍 ↦ ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ - 𝑚 < ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } ) )
13	7	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑆 ∈ SAlg )
14	8	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ∈ ( SMblFn ‘ 𝑆 ) )
15		eqid	⊢ dom ( 𝐹 ‘ 𝑛 ) = dom ( 𝐹 ‘ 𝑛 )
16	13 14 15	smff	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) : dom ( 𝐹 ‘ 𝑛 ) ⟶ ℝ )
17	16	frexr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) : dom ( 𝐹 ‘ 𝑛 ) ⟶ ℝ* )
18	1 2 3 4 17 10 11 12	finfdm2	⊢ ( 𝜑 → dom 𝐺 = ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) )
19		nfcv	⊢ Ⅎ 𝑚 𝑆
20		nfcv	⊢ Ⅎ 𝑚 ℕ
21		nnct	⊢ ℕ ≼ ω
22	21	a1i	⊢ ( 𝜑 → ℕ ≼ ω )
23		nfv	⊢ Ⅎ 𝑛 𝑚 ∈ ℕ
24	1 23	nfan	⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑚 ∈ ℕ )
25		nfcv	⊢ Ⅎ 𝑛 𝑆
26		nfcv	⊢ Ⅎ 𝑛 𝑍
27	7	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑆 ∈ SAlg )
28	6	uzct	⊢ 𝑍 ≼ ω
29	28	a1i	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑍 ≼ ω )
30	5 6	uzn0d	⊢ ( 𝜑 → 𝑍 ≠ ∅ )
31	30	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑍 ≠ ∅ )
32	27	adantr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑛 ∈ 𝑍 ) → 𝑆 ∈ SAlg )
33	9	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑛 ∈ 𝑍 ) → dom ( 𝐹 ‘ 𝑛 ) ∈ 𝑆 )
34	32 33	salrestss	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝑆 ↾t dom ( 𝐹 ‘ 𝑛 ) ) ⊆ 𝑆 )
35		nfv	⊢ Ⅎ 𝑚 𝑛 ∈ 𝑍
36	3 35	nfan	⊢ Ⅎ 𝑚 ( 𝜑 ∧ 𝑛 ∈ 𝑍 )
37		nfcv	⊢ Ⅎ 𝑥 𝑛
38	4 37	nffv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑛 )
39	14	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ∈ ( SMblFn ‘ 𝑆 ) )
40		nnre	⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℝ )
41	40	renegcld	⊢ ( 𝑚 ∈ ℕ → - 𝑚 ∈ ℝ )
42	41	rexrd	⊢ ( 𝑚 ∈ ℕ → - 𝑚 ∈ ℝ* )
43	42	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑛 ∈ 𝑍 ) → - 𝑚 ∈ ℝ* )
44	38 32 39 15 43	smfpimgtxr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑛 ∈ 𝑍 ) → { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ - 𝑚 < ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } ∈ ( 𝑆 ↾t dom ( 𝐹 ‘ 𝑛 ) ) )
45	44	an32s	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ℕ ) → { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ - 𝑚 < ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } ∈ ( 𝑆 ↾t dom ( 𝐹 ‘ 𝑛 ) ) )
46	36 45	fmptd2f	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ - 𝑚 < ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } ) : ℕ ⟶ ( 𝑆 ↾t dom ( 𝐹 ‘ 𝑛 ) ) )
47		simpr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑛 ∈ 𝑍 )
48		nnex	⊢ ℕ ∈ V
49	48	mptex	⊢ ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ - 𝑚 < ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } ) ∈ V
50	12	fvmpt2	⊢ ( ( 𝑛 ∈ 𝑍 ∧ ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ - 𝑚 < ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } ) ∈ V ) → ( 𝐻 ‘ 𝑛 ) = ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ - 𝑚 < ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } ) )
51	47 49 50	sylancl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑛 ) = ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ - 𝑚 < ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } ) )
52	51	feq1d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐻 ‘ 𝑛 ) : ℕ ⟶ ( 𝑆 ↾t dom ( 𝐹 ‘ 𝑛 ) ) ↔ ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ - 𝑚 < ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } ) : ℕ ⟶ ( 𝑆 ↾t dom ( 𝐹 ‘ 𝑛 ) ) ) )
53	46 52	mpbird	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑛 ) : ℕ ⟶ ( 𝑆 ↾t dom ( 𝐹 ‘ 𝑛 ) ) )
54	53	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑛 ) : ℕ ⟶ ( 𝑆 ↾t dom ( 𝐹 ‘ 𝑛 ) ) )
55		simplr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑛 ∈ 𝑍 ) → 𝑚 ∈ ℕ )
56	54 55	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ∈ ( 𝑆 ↾t dom ( 𝐹 ‘ 𝑛 ) ) )
57	34 56	sseldd	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ∈ 𝑆 )
58	24 25 26 27 29 31 57	saliinclf	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ∈ 𝑆 )
59	3 19 20 7 22 58	saliunclf	⊢ ( 𝜑 → ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ∈ 𝑆 )
60	18 59	eqeltrd	⊢ ( 𝜑 → dom 𝐺 ∈ 𝑆 )