smflimsuplem7 - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > smflimsuplem7		Structured version Visualization version GIF version

Theorem smflimsuplem7 47272

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

**Hypotheses**
Ref	Expression
smflimsuplem7.m	⊢ (𝜑 → 𝑀 ∈ ℤ)
smflimsuplem7.z	⊢ 𝑍 = (ℤ_≥‘𝑀)
smflimsuplem7.s	⊢ (𝜑 → 𝑆 ∈ SAlg)
smflimsuplem7.f	⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))
smflimsuplem7.d	⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}
smflimsuplem7.e	⊢ 𝐸 = (𝑘 ∈ 𝑍 ↦ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < ) ∈ ℝ})
smflimsuplem7.h	⊢ 𝐻 = (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ (𝐸‘𝑘) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < )))

**Assertion**
Ref	Expression
smflimsuplem7	⊢ (𝜑 → 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ })

Distinct variable groups: 𝑘,𝐸,𝑥 𝑘,𝐹,𝑚,𝑛,𝑥 𝑘,𝐻,𝑚,𝑛,𝑥 𝑚,𝑀 𝑘,𝑍,𝑚,𝑛,𝑥 𝜑,𝑘,𝑚,𝑛,𝑥 Allowed substitution hints: 𝐷(𝑥,𝑘,𝑚,𝑛) 𝑆(𝑥,𝑘,𝑚,𝑛) 𝐸(𝑚,𝑛) 𝑀(𝑥,𝑘,𝑛)

Proof of Theorem smflimsuplem7 Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		smflimsuplem7.d	. . 3 ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}
2	1	a1i 11	. 2 ⊢ (𝜑 → 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ})
3		simpl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → 𝜑)
4		rabidim2 45550	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
5	4	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
6		rabidim1 3412	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
7		eliun 4938	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ↔ ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
8	6, 7	sylib 218	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
9	8	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
10		nfv 1916	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛(𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
11		nfv 1916	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑚𝜑
12		nfcv 2899	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑚lim sup
13		nfmpt1 5185	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑚(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))
14	12, 13	nffv 6844	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑚(lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))
15		nfcv 2899	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑚ℝ
16	14, 15	nfel 2914	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑚(lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ
17	11, 16	nfan 1901	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑚(𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
18		nfv 1916	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑚 𝑛 ∈ 𝑍
19		nfcv 2899	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑚𝑥
20		nfii1 4972	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑚∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)
21	19, 20	nfel 2914	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑚 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)
22	17, 18, 21	nf3an 1903	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑚((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
23		nfv 1916	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑚 𝑘 ∈ (ℤ_≥‘𝑛)
24	22, 23	nfan 1901	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑚(((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘𝑛))
25		simpl1l 1226	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝜑)
26		smflimsuplem7.m	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℤ)
27	25, 26	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑀 ∈ ℤ)
28		smflimsuplem7.z	. . . . . . . . . . . . . . . 16 ⊢ 𝑍 = (ℤ_≥‘𝑀)
29		smflimsuplem7.s	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑆 ∈ SAlg)
30	25, 29	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑆 ∈ SAlg)
31		smflimsuplem7.f	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))
32	25, 31	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝐹:𝑍⟶(SMblFn‘𝑆))
33		smflimsuplem7.e	. . . . . . . . . . . . . . . 16 ⊢ 𝐸 = (𝑘 ∈ 𝑍 ↦ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < ) ∈ ℝ})
34		smflimsuplem7.h	. . . . . . . . . . . . . . . 16 ⊢ 𝐻 = (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ (𝐸‘𝑘) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < )))
35	28	uztrn2 12798	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑘 ∈ 𝑍)
36	35	3ad2antl2 1188	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑘 ∈ 𝑍)
37		simpl1r 1227	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
38		uzss 12802	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (ℤ_≥‘𝑛) → (ℤ_≥‘𝑘) ⊆ (ℤ_≥‘𝑛))
39		iinss1 4950	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℤ_≥‘𝑘) ⊆ (ℤ_≥‘𝑛) → ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚))
40	38, 39	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (ℤ_≥‘𝑛) → ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚))
41	40	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚))
42		simpl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
43	41, 42	sseldd 3923	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚))
44	43	3ad2antl3 1189	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚))
45	24, 27, 28, 30, 32, 33, 34, 36, 37, 44	smflimsuplem2 47267	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑥 ∈ dom (𝐻‘𝑘))
46	45	ralrimiva 3130	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → ∀𝑘 ∈ (ℤ_≥‘𝑛)𝑥 ∈ dom (𝐻‘𝑘))
47		vex 3434	. . . . . . . . . . . . . . 15 ⊢ 𝑥 ∈ V
48		eliin 4939	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ V → (𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ↔ ∀𝑘 ∈ (ℤ_≥‘𝑛)𝑥 ∈ dom (𝐻‘𝑘)))
49	47, 48	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ↔ ∀𝑘 ∈ (ℤ_≥‘𝑛)𝑥 ∈ dom (𝐻‘𝑘))
50	46, 49	sylibr 234	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
51	50	3exp 1120	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) → (𝑛 ∈ 𝑍 → (𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) → 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))))
52	10, 51	reximdai 3240	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) → (∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)))
53	52	imp 406	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
54		eliun 4938	. . . . . . . . . 10 ⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ↔ ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
55	53, 54	sylibr 234	. . . . . . . . 9 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
56	3, 5, 9, 55	syl21anc 838	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
57	7	biimpi 216	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
58	6, 57	syl 17	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
59	58	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
60		nfv 1916	. . . . . . . . . . 11 ⊢ Ⅎ𝑛𝜑
61		nfcv 2899	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛𝑥
62		nfv 1916	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛(lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ
63		nfiu1 4970	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)
64	62, 63	nfrabw 3427	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛{𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}
65	61, 64	nfel 2914	. . . . . . . . . . 11 ⊢ Ⅎ𝑛 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}
66	60, 65	nfan 1901	. . . . . . . . . 10 ⊢ Ⅎ𝑛(𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ})
67		nfv 1916	. . . . . . . . . 10 ⊢ Ⅎ𝑛(𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝
68		nfv 1916	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
69		simp1l 1199	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → 𝜑)
70	69, 26	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → 𝑀 ∈ ℤ)
71	69, 29	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → 𝑆 ∈ SAlg)
72	69, 31	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → 𝐹:𝑍⟶(SMblFn‘𝑆))
73		simp1r 1200	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
74		simp2 1138	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → 𝑛 ∈ 𝑍)
75		simp3 1139	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
76	68, 22, 70, 28, 71, 72, 33, 34, 73, 74, 75	smflimsuplem6 47271	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ )
77	76	3exp 1120	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) → (𝑛 ∈ 𝑍 → (𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ )))
78	5, 77	syldan 592	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → (𝑛 ∈ 𝑍 → (𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ )))
79	66, 67, 78	rexlimd 3245	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → (∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ))
80	59, 79	mpd 15	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ )
81	56, 80	jca 511	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ))
82		rabid 3411	. . . . . . 7 ⊢ (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ↔ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ))
83	81, 82	sylibr 234	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ })
84	83	ex 412	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} → 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }))
85		ssrab2 4021	. . . . . . . . . 10 ⊢ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)
86	85	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
87	28	eluzelz2 45849	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ)
88	87	uzidd 12795	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (ℤ_≥‘𝑛))
89	88	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ (ℤ_≥‘𝑛))
90		nfv 1916	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑛 ∈ 𝑍)
91		xrltso 13083	. . . . . . . . . . . . . . . . . . 19 ⊢ < Or ℝ^*
92	91	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ (𝐸‘𝑛)) → < Or ℝ^*)
93	92	supexd 9359	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ (𝐸‘𝑛)) → sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < ) ∈ V)
94		eqid 2737	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < )) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ))
95	90, 93, 94	fnmptd 6633	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < )) Fn (𝐸‘𝑛))
96		fveq2 6834	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑛 → (𝐸‘𝑘) = (𝐸‘𝑛))
97		fveq2 6834	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑛 → (ℤ_≥‘𝑘) = (ℤ_≥‘𝑛))
98	97	mpteq1d 5176	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 𝑛 → (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)))
99	98	rneqd 5887	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑛 → ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)) = ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)))
100	99	supeq1d 9352	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑛 → sup(ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) = sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ))
101	96, 100	mpteq12dv 5173	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑛 → (𝑥 ∈ (𝐸‘𝑘) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < )) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < )))
102		fvex 6847	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐸‘𝑛) ∈ V
103	102	mptex 7171	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < )) ∈ V
104	101, 34, 103	fvmpt 6941	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ 𝑍 → (𝐻‘𝑛) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < )))
105	104	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐻‘𝑛) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < )))
106	105	fneq1d 6585	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐻‘𝑛) Fn (𝐸‘𝑛) ↔ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < )) Fn (𝐸‘𝑛)))
107	95, 106	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐻‘𝑛) Fn (𝐸‘𝑛))
108	107	fndmd 6597	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom (𝐻‘𝑛) = (𝐸‘𝑛))
109	97	iineq1d 45538	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑛 → ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚) = ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
110	109	eleq2d 2823	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑛 → (𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚) ↔ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)))
111	100	eleq1d 2822	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑛 → (sup(ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ ↔ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ))
112	110, 111	anbi12d 633	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑛 → ((𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚) ∧ sup(ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ) ↔ (𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∧ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ)))
113	112	rabbidva2 3392	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑛 → {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ} = {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ})
114		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ 𝑍)
115		fveq2 6834	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑚)‘𝑥) = ((𝐹‘𝑚)‘𝑦))
116	115	mpteq2dv 5180	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑦 → (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)))
117	116	rneqd 5887	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) = ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)))
118	117	supeq1d 9352	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) = sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)), ℝ^, < ))
119	118	eleq1d 2822	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → (sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ ↔ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)), ℝ^, < ) ∈ ℝ))
120	119	cbvrabv 3400	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ} = {𝑦 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)), ℝ^, < ) ∈ ℝ}
121	88	ne0d 4283	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ 𝑍 → (ℤ_≥‘𝑛) ≠ ∅)
122		fvex 6847	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹‘𝑚) ∈ V
123	122	dmex 7853	. . . . . . . . . . . . . . . . . . . . 21 ⊢ dom (𝐹‘𝑚) ∈ V
124	123	rgenw 3056	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∀𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∈ V
125	124	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ 𝑍 → ∀𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∈ V)
126	121, 125	iinexd 45581	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ 𝑍 → ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∈ V)
127	120, 126	rabexd 5277	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ 𝑍 → {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < ) ∈ ℝ} ∈ V)
128	33, 113, 114, 127	fvmptd3 6965	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ 𝑍 → (𝐸‘𝑛) = {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < ) ∈ ℝ})
129	128	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) = {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < ) ∈ ℝ})
130		ssrab2 4021	. . . . . . . . . . . . . . . 16 ⊢ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < ) ∈ ℝ} ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)
131	130	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < ) ∈ ℝ} ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
132	129, 131	eqsstrd 3957	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
133	108, 132	eqsstrd 3957	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom (𝐻‘𝑛) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
134		fveq2 6834	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑛 → (𝐻‘𝑘) = (𝐻‘𝑛))
135	134	dmeqd 5854	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑛 → dom (𝐻‘𝑘) = dom (𝐻‘𝑛))
136	135	sseq1d 3954	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → (dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ↔ dom (𝐻‘𝑛) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)))
137	136	rspcev 3565	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ (ℤ_≥‘𝑛) ∧ dom (𝐻‘𝑛) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → ∃𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
138	89, 133, 137	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∃𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
139		iinss 5000	. . . . . . . . . . . 12 ⊢ (∃𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) → ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
140	138, 139	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
141	140	ralrimiva 3130	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
142		ss2iun 4953	. . . . . . . . . 10 ⊢ (∀𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) → ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
143	141, 142	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
144	86, 143	sstrd 3933	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
145	82	simplbi 496	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
146	54	biimpi 216	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
147	145, 146	syl 17	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
148	147	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
149		nfiu1 4970	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)
150	67, 149	nfrabw 3427	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛{𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }
151	61, 150	nfel 2914	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }
152	60, 151	nfan 1901	. . . . . . . . . . 11 ⊢ Ⅎ𝑛(𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ })
153	82	simprbi 497	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ )
154		nfv 1916	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘𝜑
155		nfmpt1 5185	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘(𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥))
156		nfcv 2899	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘dom ⇝
157	155, 156	nfel 2914	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘(𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝
158	154, 157	nfan 1901	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘(𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ )
159		nfv 1916	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘 𝑛 ∈ 𝑍
160		nfcv 2899	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘𝑥
161		nfii1 4972	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)
162	160, 161	nfel 2914	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)
163	158, 159, 162	nf3an 1903	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
164	26	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑀 ∈ ℤ)
165	164	3adant3 1133	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → 𝑀 ∈ ℤ)
166	165	3adant1r 1179	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → 𝑀 ∈ ℤ)
167	29	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑆 ∈ SAlg)
168	167	3adant3 1133	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → 𝑆 ∈ SAlg)
169	168	3adant1r 1179	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → 𝑆 ∈ SAlg)
170	31	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝐹:𝑍⟶(SMblFn‘𝑆))
171	170	3adant3 1133	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → 𝐹:𝑍⟶(SMblFn‘𝑆))
172	171	3adant1r 1179	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → 𝐹:𝑍⟶(SMblFn‘𝑆))
173		simp2 1138	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → 𝑛 ∈ 𝑍)
174		simp3 1139	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
175		simp1r 1200	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ )
176	163, 166, 28, 169, 172, 33, 34, 173, 174, 175	smflimsuplem4 47269	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
177	176	3exp 1120	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) → (𝑛 ∈ 𝑍 → (𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)))
178	153, 177	sylan2 594	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }) → (𝑛 ∈ 𝑍 → (𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)))
179	152, 62, 178	rexlimd 3245	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }) → (∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ))
180	148, 179	mpd 15	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
181	180	ralrimiva 3130	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
182	144, 181	jca 511	. . . . . . 7 ⊢ (𝜑 → ({𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∧ ∀𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ))
183		nfrab1 3410	. . . . . . . 8 ⊢ Ⅎ𝑥{𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }
184		nfcv 2899	. . . . . . . 8 ⊢ Ⅎ𝑥∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)
185	183, 184	ssrabf 45562	. . . . . . 7 ⊢ ({𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} ↔ ({𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∧ ∀𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ))
186	182, 185	sylibr 234	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ})
187	186	sseld 3921	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } → 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}))
188	84, 187	impbid 212	. . . 4 ⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} ↔ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }))
189	188	alrimiv 1929	. . 3 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} ↔ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }))
190		nfrab1 3410	. . . 4 ⊢ Ⅎ𝑥{𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}
191	190, 183	cleqf 2928	. . 3 ⊢ ({𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ↔ ∀𝑥(𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} ↔ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }))
192	189, 191	sylibr 234	. 2 ⊢ (𝜑 → {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ })
193	2, 192	eqtrd 2772	1 ⊢ (𝜑 → 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ })

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 ∀wal 1540 = wceq 1542 ∈ wcel 2114 ∀wral 3052 ∃wrex 3062 {crab 3390 Vcvv 3430 ⊆ wss 3890 ∪ ciun 4934 ∩ ciin 4935 ↦ cmpt 5167 Or wor 5531 dom cdm 5624 ran crn 5625 Fn wfn 6487 ⟶wf 6488 ‘cfv 6492 supcsup 9346 ℝcr 11028 ℝ^*cxr 11169 < clt 11170 ℤcz 12515 ℤ_≥cuz 12779 lim supclsp 15423 ⇝ cli 15437 SAlgcsalg 46754 SMblFncsmblfn 47141

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5302 ax-pr 5370 ax-un 7682 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106 ax-pre-sup 11107

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-tp 4573 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-iin 4937 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-om 7811 df-1st 7935 df-2nd 7936 df-frecs 8224 df-wrecs 8255 df-recs 8304 df-rdg 8342 df-1o 8398 df-2o 8399 df-er 8636 df-pm 8769 df-en 8887 df-dom 8888 df-sdom 8889 df-fin 8890 df-sup 9348 df-inf 9349 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-div 11799 df-nn 12166 df-2 12235 df-3 12236 df-n0 12429 df-z 12516 df-uz 12780 df-q 12890 df-rp 12934 df-ioo 13293 df-ico 13295 df-fz 13453 df-fl 13742 df-ceil 13743 df-seq 13955 df-exp 14015 df-cj 15052 df-re 15053 df-im 15054 df-sqrt 15188 df-abs 15189 df-limsup 15424 df-clim 15441 df-rlim 15442 df-smblfn 47142

This theorem is referenced by: smflimsuplem8 47273

W3C validator