Theorem smfsupdmmbllem

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

Proof

Step	Hyp	Ref	Expression
1		smfsupdmmbllem.1	⊢ Ⅎ 𝑛 𝜑
2		smfsupdmmbllem.2	⊢ Ⅎ 𝑥 𝜑
3		smfsupdmmbllem.3	⊢ Ⅎ 𝑚 𝜑
4		smfsupdmmbllem.4	⊢ Ⅎ 𝑥 𝐹
5		smfsupdmmbllem.5	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
6		smfsupdmmbllem.6	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
7		smfsupdmmbllem.7	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
8		smfsupdmmbllem.8	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
9		smfsupdmmbllem.9	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → dom ( 𝐹 ‘ 𝑛 ) ∈ 𝑆 )
10		smfsupdmmbllem.10	⊢ 𝐷 = { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 }
11		smfsupdmmbllem.11	⊢ 𝐻 = ( 𝑛 ∈ 𝑍 ↦ ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < 𝑚 } ) )
12		smfsupdmmbllem.12	⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
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 12 11	fsupdm2	⊢ ( 𝜑 → 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		nnxr	⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℝ* )
41	40	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑛 ∈ 𝑍 ) → 𝑚 ∈ ℝ* )
42	38 32 39 15 41	smfpimltxr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑛 ∈ 𝑍 ) → { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < 𝑚 } ∈ ( 𝑆 ↾t dom ( 𝐹 ‘ 𝑛 ) ) )
43	42	an32s	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ℕ ) → { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < 𝑚 } ∈ ( 𝑆 ↾t dom ( 𝐹 ‘ 𝑛 ) ) )
44	36 43	fmptd2f	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < 𝑚 } ) : ℕ ⟶ ( 𝑆 ↾t dom ( 𝐹 ‘ 𝑛 ) ) )
45		simpr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑛 ∈ 𝑍 )
46		nnex	⊢ ℕ ∈ V
47	46	mptex	⊢ ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < 𝑚 } ) ∈ V
48	11	fvmpt2	⊢ ( ( 𝑛 ∈ 𝑍 ∧ ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < 𝑚 } ) ∈ V ) → ( 𝐻 ‘ 𝑛 ) = ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < 𝑚 } ) )
49	45 47 48	sylancl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑛 ) = ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < 𝑚 } ) )
50	49	feq1d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐻 ‘ 𝑛 ) : ℕ ⟶ ( 𝑆 ↾t dom ( 𝐹 ‘ 𝑛 ) ) ↔ ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < 𝑚 } ) : ℕ ⟶ ( 𝑆 ↾t dom ( 𝐹 ‘ 𝑛 ) ) ) )
51	44 50	mpbird	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑛 ) : ℕ ⟶ ( 𝑆 ↾t dom ( 𝐹 ‘ 𝑛 ) ) )
52	51	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑛 ) : ℕ ⟶ ( 𝑆 ↾t dom ( 𝐹 ‘ 𝑛 ) ) )
53		simplr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑛 ∈ 𝑍 ) → 𝑚 ∈ ℕ )
54	52 53	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ∈ ( 𝑆 ↾t dom ( 𝐹 ‘ 𝑛 ) ) )
55	34 54	sseldd	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ∈ 𝑆 )
56	24 25 26 27 29 31 55	saliinclf	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ∈ 𝑆 )
57	3 19 20 7 22 56	saliunclf	⊢ ( 𝜑 → ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ∈ 𝑆 )
58	18 57	eqeltrd	⊢ ( 𝜑 → dom 𝐺 ∈ 𝑆 )