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 43107

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 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → 𝜑)
4		rabidim2 41374	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
5	4	adantl 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
6		rabidim1 3383	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
7		eliun 4926	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ↔ ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
8	6, 7	sylib 220	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
9	8	adantl 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
10		nfv 1914	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛(𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
11		nfv 1914	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑚𝜑
12		nfcv 2980	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑚lim sup
13		nfmpt1 5167	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑚(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))
14	12, 13	nffv 6683	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑚(lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))
15		nfcv 2980	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑚ℝ
16	14, 15	nfel 2995	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑚(lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ
17	11, 16	nfan 1899	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑚(𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
18		nfv 1914	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑚 𝑛 ∈ 𝑍
19		nfcv 2980	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑚𝑥
20		nfii1 4957	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑚∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)
21	19, 20	nfel 2995	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑚 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)
22	17, 18, 21	nf3an 1901	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑚((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
23		nfv 1914	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑚 𝑘 ∈ (ℤ_≥‘𝑛)
24	22, 23	nfan 1899	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑚(((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘𝑛))
25		simpl1l 1220	. . . . . . . . . . . . . . . . 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 12265	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑘 ∈ 𝑍)
36	35	3ad2antl2 1182	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑘 ∈ 𝑍)
37		simpl1r 1221	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
38		uzss 12268	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (ℤ_≥‘𝑛) → (ℤ_≥‘𝑘) ⊆ (ℤ_≥‘𝑛))
39		iinss1 4937	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℤ_≥‘𝑘) ⊆ (ℤ_≥‘𝑛) → ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚))
40	38, 39	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (ℤ_≥‘𝑛) → ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚))
41	40	adantl 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚))
42		simpl 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
43	41, 42	sseldd 3971	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚))
44	43	3ad2antl3 1183	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚))
45	24, 27, 28, 30, 32, 33, 34, 36, 37, 44	smflimsuplem2 43102	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑥 ∈ dom (𝐻‘𝑘))
46	45	ralrimiva 3185	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → ∀𝑘 ∈ (ℤ_≥‘𝑛)𝑥 ∈ dom (𝐻‘𝑘))
47		vex 3500	. . . . . . . . . . . . . . 15 ⊢ 𝑥 ∈ V
48		eliin 4927	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ V → (𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ↔ ∀𝑘 ∈ (ℤ_≥‘𝑛)𝑥 ∈ dom (𝐻‘𝑘)))
49	47, 48	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ↔ ∀𝑘 ∈ (ℤ_≥‘𝑛)𝑥 ∈ dom (𝐻‘𝑘))
50	46, 49	sylibr 236	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
51	50	3exp 1115	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) → (𝑛 ∈ 𝑍 → (𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) → 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))))
52	10, 51	reximdai 3314	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) → (∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)))
53	52	imp 409	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
54		eliun 4926	. . . . . . . . . 10 ⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ↔ ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
55	53, 54	sylibr 236	. . . . . . . . 9 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
56	3, 5, 9, 55	syl21anc 835	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
57	7	biimpi 218	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
58	6, 57	syl 17	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
59	58	adantl 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
60		nfv 1914	. . . . . . . . . . 11 ⊢ Ⅎ𝑛𝜑
61		nfcv 2980	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛𝑥
62		nfv 1914	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛(lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ
63		nfiu1 4956	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)
64	62, 63	nfrabw 3388	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛{𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}
65	61, 64	nfel 2995	. . . . . . . . . . 11 ⊢ Ⅎ𝑛 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}
66	60, 65	nfan 1899	. . . . . . . . . 10 ⊢ Ⅎ𝑛(𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ})
67		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑛(𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝
68		nfv 1914	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
69		simp1l 1193	. . . . . . . . . . . . . 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 1194	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
74		simp2 1133	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → 𝑛 ∈ 𝑍)
75		simp3 1134	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
76	68, 22, 70, 28, 71, 72, 33, 34, 73, 74, 75	smflimsuplem6 43106	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ )
77	76	3exp 1115	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) → (𝑛 ∈ 𝑍 → (𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ )))
78	5, 77	syldan 593	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → (𝑛 ∈ 𝑍 → (𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ )))
79	66, 67, 78	rexlimd 3320	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → (∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ))
80	59, 79	mpd 15	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ )
81	56, 80	jca 514	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ))
82		rabid 3381	. . . . . . 7 ⊢ (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ↔ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ))
83	81, 82	sylibr 236	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ })
84	83	ex 415	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} → 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }))
85		ssrab2 4059	. . . . . . . . . 10 ⊢ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)
86	85	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
87	28	eluzelz2 41682	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ)
88	87	uzidd 12262	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (ℤ_≥‘𝑛))
89	88	adantl 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ (ℤ_≥‘𝑛))
90		nfv 1914	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑛 ∈ 𝑍)
91		xrltso 12537	. . . . . . . . . . . . . . . . . . 19 ⊢ < Or ℝ^*
92	91	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ (𝐸‘𝑛)) → < Or ℝ^*)
93	92	supexd 8920	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ (𝐸‘𝑛)) → sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < ) ∈ V)
94		eqid 2824	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < )) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ))
95	90, 93, 94	fnmptd 6492	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < )) Fn (𝐸‘𝑛))
96		fveq2 6673	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑛 → (𝐸‘𝑘) = (𝐸‘𝑛))
97		fveq2 6673	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑛 → (ℤ_≥‘𝑘) = (ℤ_≥‘𝑛))
98	97	mpteq1d 5158	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 𝑛 → (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)))
99	98	rneqd 5811	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑛 → ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)) = ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)))
100	99	supeq1d 8913	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑛 → sup(ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) = sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ))
101	96, 100	mpteq12dv 5154	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑛 → (𝑥 ∈ (𝐸‘𝑘) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < )) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < )))
102		fvex 6686	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐸‘𝑛) ∈ V
103	102	mptex 6989	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < )) ∈ V
104	101, 34, 103	fvmpt 6771	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ 𝑍 → (𝐻‘𝑛) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < )))
105	104	adantl 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐻‘𝑛) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < )))
106	105	fneq1d 6449	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐻‘𝑛) Fn (𝐸‘𝑛) ↔ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < )) Fn (𝐸‘𝑛)))
107	95, 106	mpbird 259	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐻‘𝑛) Fn (𝐸‘𝑛))
108	107	fndmd 6459	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom (𝐻‘𝑛) = (𝐸‘𝑛))
109	97	iineq1d 41362	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑛 → ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚) = ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
110	109	eleq2d 2901	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑛 → (𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚) ↔ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)))
111	100	eleq1d 2900	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑛 → (sup(ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ ↔ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ))
112	110, 111	anbi12d 632	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑛 → ((𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚) ∧ sup(ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ) ↔ (𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∧ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ)))
113	112	rabbidva2 3479	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑛 → {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ} = {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ})
114		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ 𝑍)
115		fveq2 6673	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑚)‘𝑥) = ((𝐹‘𝑚)‘𝑦))
116	115	mpteq2dv 5165	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑦 → (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)))
117	116	rneqd 5811	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) = ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)))
118	117	supeq1d 8913	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) = sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)), ℝ^, < ))
119	118	eleq1d 2900	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → (sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ ↔ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)), ℝ^, < ) ∈ ℝ))
120	119	cbvrabv 3494	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ} = {𝑦 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)), ℝ^, < ) ∈ ℝ}
121	88	ne0d 4304	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ 𝑍 → (ℤ_≥‘𝑛) ≠ ∅)
122		fvex 6686	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹‘𝑚) ∈ V
123	122	dmex 7619	. . . . . . . . . . . . . . . . . . . . 21 ⊢ dom (𝐹‘𝑚) ∈ V
124	123	rgenw 3153	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∀𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∈ V
125	124	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ 𝑍 → ∀𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∈ V)
126	121, 125	iinexd 41406	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ 𝑍 → ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∈ V)
127	120, 126	rabexd 5239	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ 𝑍 → {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < ) ∈ ℝ} ∈ V)
128	33, 113, 114, 127	fvmptd3 6794	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ 𝑍 → (𝐸‘𝑛) = {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < ) ∈ ℝ})
129	128	adantl 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) = {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < ) ∈ ℝ})
130		ssrab2 4059	. . . . . . . . . . . . . . . 16 ⊢ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < ) ∈ ℝ} ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)
131	130	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < ) ∈ ℝ} ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
132	129, 131	eqsstrd 4008	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
133	108, 132	eqsstrd 4008	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom (𝐻‘𝑛) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
134		fveq2 6673	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑛 → (𝐻‘𝑘) = (𝐻‘𝑛))
135	134	dmeqd 5777	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑛 → dom (𝐻‘𝑘) = dom (𝐻‘𝑛))
136	135	sseq1d 4001	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → (dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ↔ dom (𝐻‘𝑛) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)))
137	136	rspcev 3626	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ (ℤ_≥‘𝑛) ∧ dom (𝐻‘𝑛) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → ∃𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
138	89, 133, 137	syl2anc 586	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∃𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
139		iinss 4983	. . . . . . . . . . . 12 ⊢ (∃𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) → ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
140	138, 139	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
141	140	ralrimiva 3185	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
142		ss2iun 4940	. . . . . . . . . 10 ⊢ (∀𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) → ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
143	141, 142	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
144	86, 143	sstrd 3980	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
145	82	simplbi 500	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
146	54	biimpi 218	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
147	145, 146	syl 17	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
148	147	adantl 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
149		nfiu1 4956	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)
150	67, 149	nfrabw 3388	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛{𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }
151	61, 150	nfel 2995	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }
152	60, 151	nfan 1899	. . . . . . . . . . 11 ⊢ Ⅎ𝑛(𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ })
153	82	simprbi 499	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ )
154		nfv 1914	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘𝜑
155		nfmpt1 5167	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘(𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥))
156		nfcv 2980	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘dom ⇝
157	155, 156	nfel 2995	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘(𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝
158	154, 157	nfan 1899	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘(𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ )
159		nfv 1914	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘 𝑛 ∈ 𝑍
160		nfcv 2980	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘𝑥
161		nfii1 4957	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)
162	160, 161	nfel 2995	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)
163	158, 159, 162	nf3an 1901	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
164	26	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑀 ∈ ℤ)
165	164	3adant3 1128	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → 𝑀 ∈ ℤ)
166	165	3adant1r 1173	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → 𝑀 ∈ ℤ)
167	29	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑆 ∈ SAlg)
168	167	3adant3 1128	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → 𝑆 ∈ SAlg)
169	168	3adant1r 1173	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → 𝑆 ∈ SAlg)
170	31	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝐹:𝑍⟶(SMblFn‘𝑆))
171	170	3adant3 1128	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → 𝐹:𝑍⟶(SMblFn‘𝑆))
172	171	3adant1r 1173	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → 𝐹:𝑍⟶(SMblFn‘𝑆))
173		simp2 1133	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → 𝑛 ∈ 𝑍)
174		simp3 1134	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
175		simp1r 1194	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ )
176	163, 166, 28, 169, 172, 33, 34, 173, 174, 175	smflimsuplem4 43104	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
177	176	3exp 1115	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) → (𝑛 ∈ 𝑍 → (𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)))
178	153, 177	sylan2 594	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }) → (𝑛 ∈ 𝑍 → (𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)))
179	152, 62, 178	rexlimd 3320	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }) → (∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ))
180	148, 179	mpd 15	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
181	180	ralrimiva 3185	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
182	144, 181	jca 514	. . . . . . 7 ⊢ (𝜑 → ({𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∧ ∀𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ))
183		nfrab1 3387	. . . . . . . 8 ⊢ Ⅎ𝑥{𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }
184		nfcv 2980	. . . . . . . 8 ⊢ Ⅎ𝑥∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)
185	183, 184	ssrabf 41387	. . . . . . 7 ⊢ ({𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} ↔ ({𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∧ ∀𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ))
186	182, 185	sylibr 236	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ})
187	186	sseld 3969	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } → 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}))
188	84, 187	impbid 214	. . . 4 ⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} ↔ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }))
189	188	alrimiv 1927	. . 3 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} ↔ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }))
190		nfrab1 3387	. . . 4 ⊢ Ⅎ𝑥{𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}
191	190, 183	cleqf 3013	. . 3 ⊢ ({𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ↔ ∀𝑥(𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} ↔ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }))
192	189, 191	sylibr 236	. 2 ⊢ (𝜑 → {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ })
193	2, 192	eqtrd 2859	1 ⊢ (𝜑 → 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ })

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 ∀wal 1534 = wceq 1536 ∈ wcel 2113 ∀wral 3141 ∃wrex 3142 {crab 3145 Vcvv 3497 ⊆ wss 3939 ∪ ciun 4922 ∩ ciin 4923 ↦ cmpt 5149 Or wor 5476 dom cdm 5558 ran crn 5559 Fn wfn 6353 ⟶wf 6354 ‘cfv 6358 supcsup 8907 ℝcr 10539 ℝ^*cxr 10677 < clt 10678 ℤcz 11984 ℤ_≥cuz 12246 lim supclsp 14830 ⇝ cli 14844 SAlgcsalg 42600 SMblFncsmblfn 42984

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 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 ax-rep 5193 ax-sep 5206 ax-nul 5213 ax-pow 5269 ax-pr 5333 ax-un 7464 ax-cnex 10596 ax-resscn 10597 ax-1cn 10598 ax-icn 10599 ax-addcl 10600 ax-addrcl 10601 ax-mulcl 10602 ax-mulrcl 10603 ax-mulcom 10604 ax-addass 10605 ax-mulass 10606 ax-distr 10607 ax-i2m1 10608 ax-1ne0 10609 ax-1rid 10610 ax-rnegex 10611 ax-rrecex 10612 ax-cnre 10613 ax-pre-lttri 10614 ax-pre-lttrn 10615 ax-pre-ltadd 10616 ax-pre-mulgt0 10617 ax-pre-sup 10618

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-mo 2621 df-eu 2653 df-clab 2803 df-cleq 2817 df-clel 2896 df-nfc 2966 df-ne 3020 df-nel 3127 df-ral 3146 df-rex 3147 df-reu 3148 df-rmo 3149 df-rab 3150 df-v 3499 df-sbc 3776 df-csb 3887 df-dif 3942 df-un 3944 df-in 3946 df-ss 3955 df-pss 3957 df-nul 4295 df-if 4471 df-pw 4544 df-sn 4571 df-pr 4573 df-tp 4575 df-op 4577 df-uni 4842 df-int 4880 df-iun 4924 df-iin 4925 df-br 5070 df-opab 5132 df-mpt 5150 df-tr 5176 df-id 5463 df-eprel 5468 df-po 5477 df-so 5478 df-fr 5517 df-we 5519 df-xp 5564 df-rel 5565 df-cnv 5566 df-co 5567 df-dm 5568 df-rn 5569 df-res 5570 df-ima 5571 df-pred 6151 df-ord 6197 df-on 6198 df-lim 6199 df-suc 6200 df-iota 6317 df-fun 6360 df-fn 6361 df-f 6362 df-f1 6363 df-fo 6364 df-f1o 6365 df-fv 6366 df-riota 7117 df-ov 7162 df-oprab 7163 df-mpo 7164 df-om 7584 df-1st 7692 df-2nd 7693 df-wrecs 7950 df-recs 8011 df-rdg 8049 df-1o 8105 df-oadd 8109 df-er 8292 df-pm 8412 df-en 8513 df-dom 8514 df-sdom 8515 df-fin 8516 df-sup 8909 df-inf 8910 df-pnf 10680 df-mnf 10681 df-xr 10682 df-ltxr 10683 df-le 10684 df-sub 10875 df-neg 10876 df-div 11301 df-nn 11642 df-2 11703 df-3 11704 df-n0 11901 df-z 11985 df-uz 12247 df-q 12352 df-rp 12393 df-ioo 12745 df-ico 12747 df-fz 12896 df-fl 13165 df-ceil 13166 df-seq 13373 df-exp 13433 df-cj 14461 df-re 14462 df-im 14463 df-sqrt 14597 df-abs 14598 df-limsup 14831 df-clim 14848 df-rlim 14849 df-smblfn 42985

This theorem is referenced by: smflimsuplem8 43108

W3C validator