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 47178

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 45455	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
5	4	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
6		rabidim1 3423	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
7		eliun 4952	. . . . . . . . . . 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 5199	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑚(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))
14	12, 13	nffv 6852	. . . . . . . . . . . . . . . . . . . 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 4986	. . . . . . . . . . . . . . . . . . 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 12782	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑘 ∈ 𝑍)
36	35	3ad2antl2 1188	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑘 ∈ 𝑍)
37		simpl1r 1227	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
38		uzss 12786	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (ℤ_≥‘𝑛) → (ℤ_≥‘𝑘) ⊆ (ℤ_≥‘𝑛))
39		iinss1 4964	. . . . . . . . . . . . . . . . . . . 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 3936	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚))
44	43	3ad2antl3 1189	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚))
45	24, 27, 28, 30, 32, 33, 34, 36, 37, 44	smflimsuplem2 47173	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑥 ∈ dom (𝐻‘𝑘))
46	45	ralrimiva 3130	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → ∀𝑘 ∈ (ℤ_≥‘𝑛)𝑥 ∈ dom (𝐻‘𝑘))
47		vex 3446	. . . . . . . . . . . . . . 15 ⊢ 𝑥 ∈ V
48		eliin 4953	. . . . . . . . . . . . . . 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 4952	. . . . . . . . . 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 4984	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)
64	62, 63	nfrabw 3438	. . . . . . . . . . . 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 47177	. . . . . . . . . . . 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 3422	. . . . . . 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 4034	. . . . . . . . . 10 ⊢ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)
86	85	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
87	28	eluzelz2 45755	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ)
88	87	uzidd 12779	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (ℤ_≥‘𝑛))
89	88	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ (ℤ_≥‘𝑛))
90		nfv 1916	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑛 ∈ 𝑍)
91		xrltso 13067	. . . . . . . . . . . . . . . . . . 19 ⊢ < Or ℝ^*
92	91	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ (𝐸‘𝑛)) → < Or ℝ^*)
93	92	supexd 9368	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ (𝐸‘𝑛)) → sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < ) ∈ V)
94		eqid 2737	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < )) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ))
95	90, 93, 94	fnmptd 6641	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < )) Fn (𝐸‘𝑛))
96		fveq2 6842	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑛 → (𝐸‘𝑘) = (𝐸‘𝑛))
97		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑛 → (ℤ_≥‘𝑘) = (ℤ_≥‘𝑛))
98	97	mpteq1d 5190	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 𝑛 → (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)))
99	98	rneqd 5895	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑛 → ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)) = ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)))
100	99	supeq1d 9361	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑛 → sup(ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) = sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ))
101	96, 100	mpteq12dv 5187	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑛 → (𝑥 ∈ (𝐸‘𝑘) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < )) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < )))
102		fvex 6855	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐸‘𝑛) ∈ V
103	102	mptex 7179	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < )) ∈ V
104	101, 34, 103	fvmpt 6949	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ 𝑍 → (𝐻‘𝑛) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < )))
105	104	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐻‘𝑛) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < )))
106	105	fneq1d 6593	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐻‘𝑛) Fn (𝐸‘𝑛) ↔ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < )) Fn (𝐸‘𝑛)))
107	95, 106	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐻‘𝑛) Fn (𝐸‘𝑛))
108	107	fndmd 6605	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom (𝐻‘𝑛) = (𝐸‘𝑛))
109	97	iineq1d 45443	. . . . . . . . . . . . . . . . . . . 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 3403	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑛 → {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ} = {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ})
114		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ 𝑍)
115		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑚)‘𝑥) = ((𝐹‘𝑚)‘𝑦))
116	115	mpteq2dv 5194	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑦 → (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)))
117	116	rneqd 5895	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) = ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)))
118	117	supeq1d 9361	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) = sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)), ℝ^, < ))
119	118	eleq1d 2822	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → (sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ ↔ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)), ℝ^, < ) ∈ ℝ))
120	119	cbvrabv 3411	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ} = {𝑦 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)), ℝ^, < ) ∈ ℝ}
121	88	ne0d 4296	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ 𝑍 → (ℤ_≥‘𝑛) ≠ ∅)
122		fvex 6855	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹‘𝑚) ∈ V
123	122	dmex 7861	. . . . . . . . . . . . . . . . . . . . 21 ⊢ dom (𝐹‘𝑚) ∈ V
124	123	rgenw 3056	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∀𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∈ V
125	124	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ 𝑍 → ∀𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∈ V)
126	121, 125	iinexd 45486	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ 𝑍 → ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∈ V)
127	120, 126	rabexd 5287	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ 𝑍 → {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < ) ∈ ℝ} ∈ V)
128	33, 113, 114, 127	fvmptd3 6973	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ 𝑍 → (𝐸‘𝑛) = {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < ) ∈ ℝ})
129	128	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) = {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < ) ∈ ℝ})
130		ssrab2 4034	. . . . . . . . . . . . . . . 16 ⊢ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < ) ∈ ℝ} ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)
131	130	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < ) ∈ ℝ} ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
132	129, 131	eqsstrd 3970	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
133	108, 132	eqsstrd 3970	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom (𝐻‘𝑛) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
134		fveq2 6842	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑛 → (𝐻‘𝑘) = (𝐻‘𝑛))
135	134	dmeqd 5862	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑛 → dom (𝐻‘𝑘) = dom (𝐻‘𝑛))
136	135	sseq1d 3967	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → (dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ↔ dom (𝐻‘𝑛) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)))
137	136	rspcev 3578	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ (ℤ_≥‘𝑛) ∧ dom (𝐻‘𝑛) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → ∃𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
138	89, 133, 137	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∃𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
139		iinss 5014	. . . . . . . . . . . 12 ⊢ (∃𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) → ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
140	138, 139	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
141	140	ralrimiva 3130	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
142		ss2iun 4967	. . . . . . . . . 10 ⊢ (∀𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) → ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
143	141, 142	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
144	86, 143	sstrd 3946	. . . . . . . 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 4984	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)
150	67, 149	nfrabw 3438	. . . . . . . . . . . . 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 5199	. . . . . . . . . . . . . . . . 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 4986	. . . . . . . . . . . . . . . 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 47175	. . . . . . . . . . . . 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 3421	. . . . . . . 8 ⊢ Ⅎ𝑥{𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }
184		nfcv 2899	. . . . . . . 8 ⊢ Ⅎ𝑥∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)
185	183, 184	ssrabf 45467	. . . . . . 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 3934	. . . . 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 3421	. . . 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 3401 Vcvv 3442 ⊆ wss 3903 ∪ ciun 4948 ∩ ciin 4949 ↦ cmpt 5181 Or wor 5539 dom cdm 5632 ran crn 5633 Fn wfn 6495 ⟶wf 6496 ‘cfv 6500 supcsup 9355 ℝcr 11037 ℝ^*cxr 11177 < clt 11178 ℤcz 12500 ℤ_≥cuz 12763 lim supclsp 15405 ⇝ cli 15419 SAlgcsalg 46660 SMblFncsmblfn 47047

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 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116

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 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-tp 4587 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-iin 4951 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-riota 7325 df-ov 7371 df-oprab 7372 df-mpo 7373 df-om 7819 df-1st 7943 df-2nd 7944 df-frecs 8233 df-wrecs 8264 df-recs 8313 df-rdg 8351 df-1o 8407 df-2o 8408 df-er 8645 df-pm 8778 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-sup 9357 df-inf 9358 df-pnf 11180 df-mnf 11181 df-xr 11182 df-ltxr 11183 df-le 11184 df-sub 11378 df-neg 11379 df-div 11807 df-nn 12158 df-2 12220 df-3 12221 df-n0 12414 df-z 12501 df-uz 12764 df-q 12874 df-rp 12918 df-ioo 13277 df-ico 13279 df-fz 13436 df-fl 13724 df-ceil 13725 df-seq 13937 df-exp 13997 df-cj 15034 df-re 15035 df-im 15036 df-sqrt 15170 df-abs 15171 df-limsup 15406 df-clim 15423 df-rlim 15424 df-smblfn 47048

This theorem is referenced by: smflimsuplem8 47179

W3C validator