Theorem smfliminflem 46859

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.)

Hypotheses

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

Assertion

Ref	Expression
smfliminflem	⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆))

Distinct variable groups:   𝑥,𝐷   𝑛,𝐹,𝑥   𝑚,𝑀   𝑆,𝑚   𝑚,𝑍,𝑛,𝑥   𝜑,𝑚,𝑛,𝑥

Allowed substitution hints:   𝐷(𝑚,𝑛)   𝑆(𝑥,𝑛)   𝐹(𝑚)   𝐺(𝑥,𝑚,𝑛)   𝑀(𝑥,𝑛)

Proof of Theorem smfliminflem

Step	Hyp	Ref	Expression
1		smfliminflem.g	. . . 4 ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))))
2	1	a1i 11	. . 3 ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐷 ↦ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))))
3		smfliminflem.d	. . . . . . . . . 10 ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}
4		ssrab2 4055	. . . . . . . . . 10 ⊢ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚)
5	3, 4	eqsstri 4005	. . . . . . . . 9 ⊢ 𝐷 ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚)
6		id 22	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ 𝐷)
7	5, 6	sselid 3956	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚))
8		smfliminflem.z	. . . . . . . . 9 ⊢ 𝑍 = (ℤ≥‘𝑀)
9		eqid 2735	. . . . . . . . 9 ⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚)
10	8, 9	allbutfi 45420	. . . . . . . 8 ⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ↔ ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ dom (𝐹‘𝑚))
11	7, 10	sylib 218	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 → ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ dom (𝐹‘𝑚))
12	11	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ dom (𝐹‘𝑚))
13		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑚(𝜑 ∧ 𝑛 ∈ 𝑍)
14		nfra1 3266	. . . . . . . . . 10 ⊢ Ⅎ𝑚∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ dom (𝐹‘𝑚)
15	13, 14	nfan 1899	. . . . . . . . 9 ⊢ Ⅎ𝑚((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ dom (𝐹‘𝑚))
16	8	fvexi 6890	. . . . . . . . . 10 ⊢ 𝑍 ∈ V
17	16	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ dom (𝐹‘𝑚)) → 𝑍 ∈ V)
18	8	eluzelz2 45430	. . . . . . . . . . 11 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ)
19	18	zred 12697	. . . . . . . . . 10 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ ℝ)
20	19	ad2antlr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ dom (𝐹‘𝑚)) → 𝑛 ∈ ℝ)
21		simpll 766	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ dom (𝐹‘𝑚)) → 𝜑)
22		elinel1 4176	. . . . . . . . . . 11 ⊢ (𝑚 ∈ (𝑍 ∩ (𝑛[,)+∞)) → 𝑚 ∈ 𝑍)
23		smfliminflem.s	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ∈ SAlg)
24	23	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝑆 ∈ SAlg)
25		smfliminflem.f	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))
26	25	ffvelcdmda 7074	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚) ∈ (SMblFn‘𝑆))
27		eqid 2735	. . . . . . . . . . . 12 ⊢ dom (𝐹‘𝑚) = dom (𝐹‘𝑚)
28	24, 26, 27	smff 46761	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ)
29	21, 22, 28	syl2an 596	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (𝑍 ∩ (𝑛[,)+∞))) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ)
30		simplr 768	. . . . . . . . . . . 12 ⊢ (((𝑛 ∈ 𝑍 ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (𝑍 ∩ (𝑛[,)+∞))) → ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ dom (𝐹‘𝑚))
31		eqid 2735	. . . . . . . . . . . . . 14 ⊢ (ℤ≥‘𝑛) = (ℤ≥‘𝑛)
32	18	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ 𝑍 ∧ 𝑚 ∈ (𝑍 ∩ (𝑛[,)+∞))) → 𝑛 ∈ ℤ)
33	8, 22	eluzelz2d 45440	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ (𝑍 ∩ (𝑛[,)+∞)) → 𝑚 ∈ ℤ)
34	33	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ 𝑍 ∧ 𝑚 ∈ (𝑍 ∩ (𝑛[,)+∞))) → 𝑚 ∈ ℤ)
35	19	rexrd 11285	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ ℝ*)
36	35	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ 𝑍 ∧ 𝑚 ∈ (𝑍 ∩ (𝑛[,)+∞))) → 𝑛 ∈ ℝ*)
37		pnfxr 11289	. . . . . . . . . . . . . . . 16 ⊢ +∞ ∈ ℝ*
38	37	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ 𝑍 ∧ 𝑚 ∈ (𝑍 ∩ (𝑛[,)+∞))) → +∞ ∈ ℝ*)
39		elinel2 4177	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ (𝑍 ∩ (𝑛[,)+∞)) → 𝑚 ∈ (𝑛[,)+∞))
40	39	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ 𝑍 ∧ 𝑚 ∈ (𝑍 ∩ (𝑛[,)+∞))) → 𝑚 ∈ (𝑛[,)+∞))
41	36, 38, 40	icogelbd 13414	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ 𝑍 ∧ 𝑚 ∈ (𝑍 ∩ (𝑛[,)+∞))) → 𝑛 ≤ 𝑚)
42	31, 32, 34, 41	eluzd 45436	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ 𝑍 ∧ 𝑚 ∈ (𝑍 ∩ (𝑛[,)+∞))) → 𝑚 ∈ (ℤ≥‘𝑛))
43	42	adantlr 715	. . . . . . . . . . . 12 ⊢ (((𝑛 ∈ 𝑍 ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (𝑍 ∩ (𝑛[,)+∞))) → 𝑚 ∈ (ℤ≥‘𝑛))
44		rspa 3231	. . . . . . . . . . . 12 ⊢ ((∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ dom (𝐹‘𝑚) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑥 ∈ dom (𝐹‘𝑚))
45	30, 43, 44	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝑛 ∈ 𝑍 ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (𝑍 ∩ (𝑛[,)+∞))) → 𝑥 ∈ dom (𝐹‘𝑚))
46	45	adantlll 718	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (𝑍 ∩ (𝑛[,)+∞))) → 𝑥 ∈ dom (𝐹‘𝑚))
47	29, 46	ffvelcdmd 7075	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ dom (𝐹‘𝑚)) ∧ 𝑚 ∈ (𝑍 ∩ (𝑛[,)+∞))) → ((𝐹‘𝑚)‘𝑥) ∈ ℝ)
48	15, 17, 20, 47	liminfval4 45818	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ dom (𝐹‘𝑚)) → (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = -𝑒(lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))))
49	48	rexlimdva2 3143	. . . . . . 7 ⊢ (𝜑 → (∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ dom (𝐹‘𝑚) → (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = -𝑒(lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥)))))
50	49	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ dom (𝐹‘𝑚) → (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = -𝑒(lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥)))))
51	12, 50	mpd 15	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = -𝑒(lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))))
52	51	xnegeqd 45464	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → -𝑒(lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = -𝑒-𝑒(lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))))
53	16	mptex 7215	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥)) ∈ V
54	53	limsupcli 45786	. . . . . . . . . . 11 ⊢ (lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) ∈ ℝ*
55	54	xnegnegi 45466	. . . . . . . . . 10 ⊢ -𝑒-𝑒(lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) = (lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥)))
56	55	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → -𝑒-𝑒(lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) = (lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))))
57	52, 56	eqtr2d 2771	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) = -𝑒(lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))))
58	3	reqabi 3439	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∧ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ))
59	58	simprbi 496	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
60	59	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
61	60	rexnegd 45167	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → -𝑒(lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = -(lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))))
62	57, 61	eqtr2d 2771	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → -(lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = (lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))))
63	60	renegcld 11664	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → -(lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
64	62, 63	eqeltrrd 2835	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
65	64	rexnegd 45167	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → -𝑒(lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) = -(lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))))
66	51, 65	eqtrd 2770	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = -(lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))))
67	66	mpteq2dva 5214	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) = (𝑥 ∈ 𝐷 ↦ -(lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥)))))
68	2, 67	eqtrd 2770	. 2 ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐷 ↦ -(lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥)))))
69		nfv 1914	. . 3 ⊢ Ⅎ𝑥𝜑
70	18, 31	uzn0d 45452	. . . . . . . 8 ⊢ (𝑛 ∈ 𝑍 → (ℤ≥‘𝑛) ≠ ∅)
71		fvex 6889	. . . . . . . . . . 11 ⊢ (𝐹‘𝑚) ∈ V
72	71	dmex 7905	. . . . . . . . . 10 ⊢ dom (𝐹‘𝑚) ∈ V
73	72	rgenw 3055	. . . . . . . . 9 ⊢ ∀𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V
74	73	a1i 11	. . . . . . . 8 ⊢ (𝑛 ∈ 𝑍 → ∀𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V)
75		iinexg 5318	. . . . . . . 8 ⊢ (((ℤ≥‘𝑛) ≠ ∅ ∧ ∀𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V) → ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V)
76	70, 74, 75	syl2anc 584	. . . . . . 7 ⊢ (𝑛 ∈ 𝑍 → ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V)
77	76	rgen 3053	. . . . . 6 ⊢ ∀𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V
78		iunexg 7962	. . . . . 6 ⊢ ((𝑍 ∈ V ∧ ∀𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V) → ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V)
79	16, 77, 78	mp2an 692	. . . . 5 ⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∈ V
80	79, 5	ssexi 5292	. . . 4 ⊢ 𝐷 ∈ V
81	80	a1i 11	. . 3 ⊢ (𝜑 → 𝐷 ∈ V)
82	3	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ})
83	10	biimpi 216	. . . . . . . . 9 ⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) → ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ dom (𝐹‘𝑚))
84	49	imp 406	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑥 ∈ dom (𝐹‘𝑚)) → (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = -𝑒(lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))))
85	83, 84	sylan2 593	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚)) → (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = -𝑒(lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))))
86	54	a1i 11	. . . . . . . . . 10 ⊢ (((lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = -𝑒(lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) ∧ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) → (lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) ∈ ℝ*)
87		simpl 482	. . . . . . . . . . 11 ⊢ (((lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = -𝑒(lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) ∧ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) → (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = -𝑒(lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))))
88		simpr 484	. . . . . . . . . . 11 ⊢ (((lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = -𝑒(lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) ∧ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) → (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
89	87, 88	eqeltrrd 2835	. . . . . . . . . 10 ⊢ (((lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = -𝑒(lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) ∧ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) → -𝑒(lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
90		xnegrecl2 45487	. . . . . . . . . 10 ⊢ (((lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) ∈ ℝ* ∧ -𝑒(lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) ∈ ℝ) → (lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
91	86, 89, 90	syl2anc 584	. . . . . . . . 9 ⊢ (((lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = -𝑒(lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) ∧ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) → (lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
92		simpl 482	. . . . . . . . . 10 ⊢ (((lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = -𝑒(lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) ∈ ℝ) → (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = -𝑒(lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))))
93		xnegrecl 45465	. . . . . . . . . . 11 ⊢ ((lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) ∈ ℝ → -𝑒(lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
94	93	adantl 481	. . . . . . . . . 10 ⊢ (((lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = -𝑒(lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) ∈ ℝ) → -𝑒(lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
95	92, 94	eqeltrd 2834	. . . . . . . . 9 ⊢ (((lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = -𝑒(lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) ∈ ℝ) → (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
96	91, 95	impbida 800	. . . . . . . 8 ⊢ ((lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) = -𝑒(lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) → ((lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ ↔ (lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) ∈ ℝ))
97	85, 96	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚)) → ((lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ ↔ (lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) ∈ ℝ))
98	97	rabbidva 3422	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) ∈ ℝ})
99	82, 98	eqtrd 2770	. . . . 5 ⊢ (𝜑 → 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) ∈ ℝ})
100	69, 99	mpteq1df 45260	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ (lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥)))) = (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) ∈ ℝ} ↦ (lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥)))))
101		nfv 1914	. . . . 5 ⊢ Ⅎ𝑚𝜑
102		nfv 1914	. . . . 5 ⊢ Ⅎ𝑛𝜑
103		smfliminflem.m	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ ℤ)
104		negex 11480	. . . . . 6 ⊢ -((𝐹‘𝑚)‘𝑥) ∈ V
105	104	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ dom (𝐹‘𝑚)) → -((𝐹‘𝑚)‘𝑥) ∈ V)
106		nfv 1914	. . . . . 6 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑚 ∈ 𝑍)
107	72	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → dom (𝐹‘𝑚) ∈ V)
108	28	ffvelcdmda 7074	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ 𝑍) ∧ 𝑥 ∈ dom (𝐹‘𝑚)) → ((𝐹‘𝑚)‘𝑥) ∈ ℝ)
109	28	feqmptd 6947	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚) = (𝑥 ∈ dom (𝐹‘𝑚) ↦ ((𝐹‘𝑚)‘𝑥)))
110	109, 26	eqeltrrd 2835	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝑥 ∈ dom (𝐹‘𝑚) ↦ ((𝐹‘𝑚)‘𝑥)) ∈ (SMblFn‘𝑆))
111	106, 24, 107, 108, 110	smfneg 46832	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝑥 ∈ dom (𝐹‘𝑚) ↦ -((𝐹‘𝑚)‘𝑥)) ∈ (SMblFn‘𝑆))
112		eqid 2735	. . . . 5 ⊢ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) ∈ ℝ} = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) ∈ ℝ}
113		eqid 2735	. . . . 5 ⊢ (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) ∈ ℝ} ↦ (lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥)))) = (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) ∈ ℝ} ↦ (lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))))
114	101, 69, 102, 103, 8, 23, 105, 111, 112, 113	smflimsupmpt 46858	. . . 4 ⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥))) ∈ ℝ} ↦ (lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥)))) ∈ (SMblFn‘𝑆))
115	100, 114	eqeltrd 2834	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ (lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥)))) ∈ (SMblFn‘𝑆))
116	69, 23, 81, 64, 115	smfneg 46832	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ -(lim sup‘(𝑚 ∈ 𝑍 ↦ -((𝐹‘𝑚)‘𝑥)))) ∈ (SMblFn‘𝑆))
117	68, 116	eqeltrd 2834	1 ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2108   ≠ wne 2932  ∀wral 3051  ∃wrex 3060  {crab 3415  Vcvv 3459   ∩ cin 3925  ∅c0 4308  ∪ ciun 4967  ∩ ciin 4968   ↦ cmpt 5201  dom cdm 5654  ⟶wf 6527  ‘cfv 6531  (class class class)co 7405  ℝcr 11128  +∞cpnf 11266  ℝ^*cxr 11268  -cneg 11467  ℤcz 12588  ℤ_≥cuz 12852  -_𝑒cxne 13125  [,)cico 13364  lim supclsp 15486  lim infclsi 45780  SAlgcsalg 46337  SMblFncsmblfn 46724

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5249  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729  ax-inf2 9655  ax-cc 10449  ax-ac2 10477  ax-cnex 11185  ax-resscn 11186  ax-1cn 11187  ax-icn 11188  ax-addcl 11189  ax-addrcl 11190  ax-mulcl 11191  ax-mulrcl 11192  ax-mulcom 11193  ax-addass 11194  ax-mulass 11195  ax-distr 11196  ax-i2m1 11197  ax-1ne0 11198  ax-1rid 11199  ax-rnegex 11200  ax-rrecex 11201  ax-cnre 11202  ax-pre-lttri 11203  ax-pre-lttrn 11204  ax-pre-ltadd 11205  ax-pre-mulgt0 11206  ax-pre-sup 11207

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3359  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-tp 4606  df-op 4608  df-uni 4884  df-int 4923  df-iun 4969  df-iin 4970  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-se 5607  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-isom 6540  df-riota 7362  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7862  df-1st 7988  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-2o 8481  df-oadd 8484  df-omul 8485  df-er 8719  df-map 8842  df-pm 8843  df-en 8960  df-dom 8961  df-sdom 8962  df-fin 8963  df-sup 9454  df-inf 9455  df-oi 9524  df-card 9953  df-acn 9956  df-ac 10130  df-pnf 11271  df-mnf 11272  df-xr 11273  df-ltxr 11274  df-le 11275  df-sub 11468  df-neg 11469  df-div 11895  df-nn 12241  df-2 12303  df-3 12304  df-4 12305  df-n0 12502  df-z 12589  df-uz 12853  df-q 12965  df-rp 13009  df-xneg 13128  df-ioo 13366  df-ioc 13367  df-ico 13368  df-icc 13369  df-fz 13525  df-fzo 13672  df-fl 13809  df-ceil 13810  df-seq 14020  df-exp 14080  df-hash 14349  df-word 14532  df-concat 14589  df-s1 14614  df-s2 14867  df-s3 14868  df-s4 14869  df-cj 15118  df-re 15119  df-im 15120  df-sqrt 15254  df-abs 15255  df-limsup 15487  df-clim 15504  df-rlim 15505  df-rest 17436  df-topgen 17457  df-top 22832  df-bases 22884  df-liminf 45781  df-salg 46338  df-salgen 46342  df-smblfn 46725

This theorem is referenced by:  smfliminf  46860