Theorem smflimsuplem6

Description: The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of Fremlin1 p. 39 . (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	smflimsuplem6.a	⊢ Ⅎ 𝑛 𝜑
	smflimsuplem6.b	⊢ Ⅎ 𝑚 𝜑
	smflimsuplem6.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	smflimsuplem6.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	smflimsuplem6.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	smflimsuplem6.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
	smflimsuplem6.e	⊢ 𝐸 = ( 𝑛 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
	smflimsuplem6.h	⊢ 𝐻 = ( 𝑛 ∈ 𝑍 ↦ ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) )
	smflimsuplem6.r	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) ∈ ℝ )
	smflimsuplem6.n	⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
	smflimsuplem6.x	⊢ ( 𝜑 → 𝑋 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) dom ( 𝐹 ‘ 𝑚 ) )
Assertion	smflimsuplem6	⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑋 ) ) ∈ dom ⇝ )

Proof

Step	Hyp	Ref	Expression
1		smflimsuplem6.a	⊢ Ⅎ 𝑛 𝜑
2		smflimsuplem6.b	⊢ Ⅎ 𝑚 𝜑
3		smflimsuplem6.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4		smflimsuplem6.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
5		smflimsuplem6.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
6		smflimsuplem6.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
7		smflimsuplem6.e	⊢ 𝐸 = ( 𝑛 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
8		smflimsuplem6.h	⊢ 𝐻 = ( 𝑛 ∈ 𝑍 ↦ ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) )
9		smflimsuplem6.r	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) ∈ ℝ )
10		smflimsuplem6.n	⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
11		smflimsuplem6.x	⊢ ( 𝜑 → 𝑋 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) dom ( 𝐹 ‘ 𝑚 ) )
12	4	fvexi	⊢ 𝑍 ∈ V
13	12	a1i	⊢ ( 𝜑 → 𝑍 ∈ V )
14	13	mptexd	⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑋 ) ) ∈ V )
15		fvexd	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) ∈ V )
16	1 2 3 4 5 6 7 8 9 10 11	smflimsuplem5	⊢ ( 𝜑 → ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑋 ) ) ⇝ ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) )
17		fvexd	⊢ ( 𝜑 → ( ℤ≥ ‘ 𝑁 ) ∈ V )
18	4	eluzelz2	⊢ ( 𝑁 ∈ 𝑍 → 𝑁 ∈ ℤ )
19	10 18	syl	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
20		eqid	⊢ ( ℤ≥ ‘ 𝑁 ) = ( ℤ≥ ‘ 𝑁 )
21	4	eleq2i	⊢ ( 𝑁 ∈ 𝑍 ↔ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
22	21	biimpi	⊢ ( 𝑁 ∈ 𝑍 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
23		uzss	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ 𝑁 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
24	22 23	syl	⊢ ( 𝑁 ∈ 𝑍 → ( ℤ≥ ‘ 𝑁 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
25	24 4	sseqtrrdi	⊢ ( 𝑁 ∈ 𝑍 → ( ℤ≥ ‘ 𝑁 ) ⊆ 𝑍 )
26	10 25	syl	⊢ ( 𝜑 → ( ℤ≥ ‘ 𝑁 ) ⊆ 𝑍 )
27		ssid	⊢ ( ℤ≥ ‘ 𝑁 ) ⊆ ( ℤ≥ ‘ 𝑁 )
28	27	a1i	⊢ ( 𝜑 → ( ℤ≥ ‘ 𝑁 ) ⊆ ( ℤ≥ ‘ 𝑁 ) )
29		fvexd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑋 ) ∈ V )
30	1 13 17 19 20 26 28 29	climeqmpt	⊢ ( 𝜑 → ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑋 ) ) ⇝ ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) ↔ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑋 ) ) ⇝ ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) ) )
31	16 30	mpbird	⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑋 ) ) ⇝ ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) )
32		breldmg	⊢ ( ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑋 ) ) ∈ V ∧ ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) ∈ V ∧ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑋 ) ) ⇝ ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) ) → ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑋 ) ) ∈ dom ⇝ )
33	14 15 31 32	syl3anc	⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑋 ) ) ∈ dom ⇝ )