smfliminflem

Description: The inferior limit of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (e) of Fremlin1 p. 39 . (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	smfliminflem.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	smfliminflem.z	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
	smfliminflem.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	smfliminflem.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
	smfliminflem.d	⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ }
	smfliminflem.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
Assertion	smfliminflem	⊢ ( 𝜑 → 𝐺 ∈ ( SMblFn ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		smfliminflem.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2		smfliminflem.z	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
3		smfliminflem.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
4		smfliminflem.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
5		smfliminflem.d	⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ }
6		smfliminflem.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
7	6	a1i	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) )
8		ssrab2	⊢ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
9	5 8	eqsstri	⊢ 𝐷 ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
10		id	⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ 𝐷 )
11	9 10	sselid	⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
12		eqid	⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
13	2 12	allbutfi	⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ↔ ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) )
14	11 13	sylib	⊢ ( 𝑥 ∈ 𝐷 → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) )
15	14	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) )
16		nfv	⊢ Ⅎ 𝑚 ( 𝜑 ∧ 𝑛 ∈ 𝑍 )
17		nfra1	⊢ Ⅎ 𝑚 ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 )
18	16 17	nfan	⊢ Ⅎ 𝑚 ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) )
19	2	fvexi	⊢ 𝑍 ∈ V
20	19	a1i	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) → 𝑍 ∈ V )
21	2	eluzelz2	⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ )
22	21	zred	⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ℝ )
23	22	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) → 𝑛 ∈ ℝ )
24		simpll	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) → 𝜑 )
25		elinel1	⊢ ( 𝑚 ∈ ( 𝑍 ∩ ( 𝑛 [,) +∞ ) ) → 𝑚 ∈ 𝑍 )
26	3	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → 𝑆 ∈ SAlg )
27	4	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) ∈ ( SMblFn ‘ 𝑆 ) )
28		eqid	⊢ dom ( 𝐹 ‘ 𝑚 ) = dom ( 𝐹 ‘ 𝑚 )
29	26 27 28	smff	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) : dom ( 𝐹 ‘ 𝑚 ) ⟶ ℝ )
30	24 25 29	syl2an	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( 𝑍 ∩ ( 𝑛 [,) +∞ ) ) ) → ( 𝐹 ‘ 𝑚 ) : dom ( 𝐹 ‘ 𝑚 ) ⟶ ℝ )
31		simplr	⊢ ( ( ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( 𝑍 ∩ ( 𝑛 [,) +∞ ) ) ) → ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) )
32		eqid	⊢ ( ℤ_≥ ‘ 𝑛 ) = ( ℤ_≥ ‘ 𝑛 )
33	21	adantr	⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝑚 ∈ ( 𝑍 ∩ ( 𝑛 [,) +∞ ) ) ) → 𝑛 ∈ ℤ )
34	2 25	eluzelz2d	⊢ ( 𝑚 ∈ ( 𝑍 ∩ ( 𝑛 [,) +∞ ) ) → 𝑚 ∈ ℤ )
35	34	adantl	⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝑚 ∈ ( 𝑍 ∩ ( 𝑛 [,) +∞ ) ) ) → 𝑚 ∈ ℤ )
36	22	rexrd	⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ℝ^* )
37	36	adantr	⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝑚 ∈ ( 𝑍 ∩ ( 𝑛 [,) +∞ ) ) ) → 𝑛 ∈ ℝ^* )
38		pnfxr	⊢ +∞ ∈ ℝ^*
39	38	a1i	⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝑚 ∈ ( 𝑍 ∩ ( 𝑛 [,) +∞ ) ) ) → +∞ ∈ ℝ^* )
40		elinel2	⊢ ( 𝑚 ∈ ( 𝑍 ∩ ( 𝑛 [,) +∞ ) ) → 𝑚 ∈ ( 𝑛 [,) +∞ ) )
41	40	adantl	⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝑚 ∈ ( 𝑍 ∩ ( 𝑛 [,) +∞ ) ) ) → 𝑚 ∈ ( 𝑛 [,) +∞ ) )
42	37 39 41	icogelbd	⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝑚 ∈ ( 𝑍 ∩ ( 𝑛 [,) +∞ ) ) ) → 𝑛 ≤ 𝑚 )
43	32 33 35 42	eluzd	⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝑚 ∈ ( 𝑍 ∩ ( 𝑛 [,) +∞ ) ) ) → 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) )
44	43	adantlr	⊢ ( ( ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( 𝑍 ∩ ( 𝑛 [,) +∞ ) ) ) → 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) )
45		rspa	⊢ ( ( ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∧ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) )
46	31 44 45	syl2anc	⊢ ( ( ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( 𝑍 ∩ ( 𝑛 [,) +∞ ) ) ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) )
47	46	adantlll	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( 𝑍 ∩ ( 𝑛 [,) +∞ ) ) ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) )
48	30 47	ffvelrnd	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑚 ∈ ( 𝑍 ∩ ( 𝑛 [,) +∞ ) ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ∈ ℝ )
49	18 20 23 48	liminfval4	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) → ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = -_𝑒 ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
50	49	rexlimdva2	⊢ ( 𝜑 → ( ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) → ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = -_𝑒 ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) )
51	50	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) → ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = -_𝑒 ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) )
52	15 51	mpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = -_𝑒 ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
53	52	xnegeqd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → -_𝑒 ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = -_𝑒 -_𝑒 ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
54	19	mptex	⊢ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ V
55	54	limsupcli	⊢ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ^*
56	55	xnegnegi	⊢ -_𝑒 -_𝑒 ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) )
57	56	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → -_𝑒 -_𝑒 ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
58	53 57	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = -_𝑒 ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
59	5	rabeq2i	⊢ ( 𝑥 ∈ 𝐷 ↔ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∧ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) )
60	59	simprbi	⊢ ( 𝑥 ∈ 𝐷 → ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
61	60	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
62	61	rexnegd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → -_𝑒 ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = - ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
63	58 62	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → - ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
64	61	renegcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → - ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
65	63 64	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
66	65	rexnegd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → -_𝑒 ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = - ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
67	52 66	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = - ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
68	67	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ - ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) )
69	7 68	eqtrd	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐷 ↦ - ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) )
70		nfv	⊢ Ⅎ 𝑥 𝜑
71	21 32	uzn0d	⊢ ( 𝑛 ∈ 𝑍 → ( ℤ_≥ ‘ 𝑛 ) ≠ ∅ )
72		fvex	⊢ ( 𝐹 ‘ 𝑚 ) ∈ V
73	72	dmex	⊢ dom ( 𝐹 ‘ 𝑚 ) ∈ V
74	73	rgenw	⊢ ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V
75	74	a1i	⊢ ( 𝑛 ∈ 𝑍 → ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V )
76		iinexg	⊢ ( ( ( ℤ_≥ ‘ 𝑛 ) ≠ ∅ ∧ ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V ) → ∩ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V )
77	71 75 76	syl2anc	⊢ ( 𝑛 ∈ 𝑍 → ∩ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V )
78	77	rgen	⊢ ∀ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V
79		iunexg	⊢ ( ( 𝑍 ∈ V ∧ ∀ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V ) → ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V )
80	19 78 79	mp2an	⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V
81	80 9	ssexi	⊢ 𝐷 ∈ V
82	81	a1i	⊢ ( 𝜑 → 𝐷 ∈ V )
83	5	a1i	⊢ ( 𝜑 → 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } )
84	13	biimpi	⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) )
85	50	imp	⊢ ( ( 𝜑 ∧ ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) → ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = -_𝑒 ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
86	84 85	sylan2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = -_𝑒 ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
87	55	a1i	⊢ ( ( ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = -_𝑒 ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∧ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ^* )
88		simpl	⊢ ( ( ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = -_𝑒 ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∧ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) → ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = -_𝑒 ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
89		simpr	⊢ ( ( ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = -_𝑒 ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∧ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) → ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
90	88 89	eqeltrrd	⊢ ( ( ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = -_𝑒 ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∧ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) → -_𝑒 ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
91		xnegrecl2	⊢ ( ( ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ^* ∧ -_𝑒 ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
92	87 90 91	syl2anc	⊢ ( ( ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = -_𝑒 ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∧ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
93		simpl	⊢ ( ( ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = -_𝑒 ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) → ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = -_𝑒 ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
94		xnegrecl	⊢ ( ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ → -_𝑒 ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
95	94	adantl	⊢ ( ( ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = -_𝑒 ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) → -_𝑒 ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
96	93 95	eqeltrd	⊢ ( ( ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = -_𝑒 ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) → ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
97	92 96	impbida	⊢ ( ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = -_𝑒 ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) → ( ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ↔ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) )
98	86 97	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → ( ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ↔ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) )
99	98	rabbidva	⊢ ( 𝜑 → { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } )
100	83 99	eqtrd	⊢ ( 𝜑 → 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } )
101	70 100	mpteq1df	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ↦ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) )
102		nfv	⊢ Ⅎ 𝑚 𝜑
103		nfv	⊢ Ⅎ 𝑛 𝜑
104		negex	⊢ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ∈ V
105	104	a1i	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) → - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ∈ V )
106		nfv	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑚 ∈ 𝑍 )
107	73	a1i	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → dom ( 𝐹 ‘ 𝑚 ) ∈ V )
108	29	ffvelrnda	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ∈ ℝ )
109	29	feqmptd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) = ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) )
110	109 27	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ ( SMblFn ‘ 𝑆 ) )
111	106 26 107 108 110	smfneg	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ ( SMblFn ‘ 𝑆 ) )
112		eqid	⊢ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ }
113		eqid	⊢ ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ↦ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ↦ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
114	102 70 103 1 2 3 105 111 112 113	smflimsupmpt	⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ_≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ↦ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) ∈ ( SMblFn ‘ 𝑆 ) )
115	101 114	eqeltrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) ∈ ( SMblFn ‘ 𝑆 ) )
116	70 3 82 65 115	smfneg	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ - ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) ∈ ( SMblFn ‘ 𝑆 ) )
117	69 116	eqeltrd	⊢ ( 𝜑 → 𝐺 ∈ ( SMblFn ‘ 𝑆 ) )

Metamath Proof Explorer

Theorem smfliminflem

Proof