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 46817

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 45090	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
5	4	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
6		rabidim1 3417	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
7		eliun 4945	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ↔ ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
8	6, 7	sylib 218	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
9	8	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
10		nfv 1914	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛(𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
11		nfv 1914	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑚𝜑
12		nfcv 2891	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑚lim sup
13		nfmpt1 5191	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑚(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))
14	12, 13	nffv 6832	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑚(lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))
15		nfcv 2891	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑚ℝ
16	14, 15	nfel 2906	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑚(lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ
17	11, 16	nfan 1899	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑚(𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
18		nfv 1914	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑚 𝑛 ∈ 𝑍
19		nfcv 2891	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑚𝑥
20		nfii1 4979	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑚∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)
21	19, 20	nfel 2906	. . . . . . . . . . . . . . . . . 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 1225	. . . . . . . . . . . . . . . . 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 12754	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑘 ∈ 𝑍)
36	35	3ad2antl2 1187	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑘 ∈ 𝑍)
37		simpl1r 1226	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
38		uzss 12758	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (ℤ_≥‘𝑛) → (ℤ_≥‘𝑘) ⊆ (ℤ_≥‘𝑛))
39		iinss1 4957	. . . . . . . . . . . . . . . . . . . 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 1188	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚))
45	24, 27, 28, 30, 32, 33, 34, 36, 37, 44	smflimsuplem2 46812	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑥 ∈ dom (𝐻‘𝑘))
46	45	ralrimiva 3121	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → ∀𝑘 ∈ (ℤ_≥‘𝑛)𝑥 ∈ dom (𝐻‘𝑘))
47		vex 3440	. . . . . . . . . . . . . . 15 ⊢ 𝑥 ∈ V
48		eliin 4946	. . . . . . . . . . . . . . 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 1119	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) → (𝑛 ∈ 𝑍 → (𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) → 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))))
52	10, 51	reximdai 3231	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) → (∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)))
53	52	imp 406	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
54		eliun 4945	. . . . . . . . . 10 ⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ↔ ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
55	53, 54	sylibr 234	. . . . . . . . 9 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
56	3, 5, 9, 55	syl21anc 837	. . . . . . . 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 1914	. . . . . . . . . . 11 ⊢ Ⅎ𝑛𝜑
61		nfcv 2891	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛𝑥
62		nfv 1914	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛(lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ
63		nfiu1 4977	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)
64	62, 63	nfrabw 3432	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛{𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}
65	61, 64	nfel 2906	. . . . . . . . . . 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 1198	. . . . . . . . . . . . . 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 1199	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
74		simp2 1137	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → 𝑛 ∈ 𝑍)
75		simp3 1138	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
76	68, 22, 70, 28, 71, 72, 33, 34, 73, 74, 75	smflimsuplem6 46816	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ )
77	76	3exp 1119	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) → (𝑛 ∈ 𝑍 → (𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ )))
78	5, 77	syldan 591	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → (𝑛 ∈ 𝑍 → (𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ )))
79	66, 67, 78	rexlimd 3236	. . . . . . . . 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 3416	. . . . . . 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 4031	. . . . . . . . . 10 ⊢ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)
86	85	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
87	28	eluzelz2 45392	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ)
88	87	uzidd 12751	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (ℤ_≥‘𝑛))
89	88	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ (ℤ_≥‘𝑛))
90		nfv 1914	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑛 ∈ 𝑍)
91		xrltso 13043	. . . . . . . . . . . . . . . . . . 19 ⊢ < Or ℝ^*
92	91	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ (𝐸‘𝑛)) → < Or ℝ^*)
93	92	supexd 9343	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ (𝐸‘𝑛)) → sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < ) ∈ V)
94		eqid 2729	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < )) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ))
95	90, 93, 94	fnmptd 6623	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < )) Fn (𝐸‘𝑛))
96		fveq2 6822	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑛 → (𝐸‘𝑘) = (𝐸‘𝑛))
97		fveq2 6822	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑛 → (ℤ_≥‘𝑘) = (ℤ_≥‘𝑛))
98	97	mpteq1d 5182	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 𝑛 → (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)))
99	98	rneqd 5880	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑛 → ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)) = ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)))
100	99	supeq1d 9336	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑛 → sup(ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) = sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ))
101	96, 100	mpteq12dv 5179	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑛 → (𝑥 ∈ (𝐸‘𝑘) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < )) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < )))
102		fvex 6835	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐸‘𝑛) ∈ V
103	102	mptex 7159	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < )) ∈ V
104	101, 34, 103	fvmpt 6930	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ 𝑍 → (𝐻‘𝑛) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < )))
105	104	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐻‘𝑛) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < )))
106	105	fneq1d 6575	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐻‘𝑛) Fn (𝐸‘𝑛) ↔ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < )) Fn (𝐸‘𝑛)))
107	95, 106	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐻‘𝑛) Fn (𝐸‘𝑛))
108	107	fndmd 6587	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom (𝐻‘𝑛) = (𝐸‘𝑛))
109	97	iineq1d 45078	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑛 → ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚) = ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
110	109	eleq2d 2814	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑛 → (𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚) ↔ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)))
111	100	eleq1d 2813	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑛 → (sup(ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ ↔ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ))
112	110, 111	anbi12d 632	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑛 → ((𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚) ∧ sup(ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ) ↔ (𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∧ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ)))
113	112	rabbidva2 3396	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑛 → {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ} = {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ})
114		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ 𝑍)
115		fveq2 6822	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑚)‘𝑥) = ((𝐹‘𝑚)‘𝑦))
116	115	mpteq2dv 5186	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑦 → (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)))
117	116	rneqd 5880	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) = ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)))
118	117	supeq1d 9336	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) = sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)), ℝ^, < ))
119	118	eleq1d 2813	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → (sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ ↔ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)), ℝ^, < ) ∈ ℝ))
120	119	cbvrabv 3405	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ} = {𝑦 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)), ℝ^, < ) ∈ ℝ}
121	88	ne0d 4293	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ 𝑍 → (ℤ_≥‘𝑛) ≠ ∅)
122		fvex 6835	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹‘𝑚) ∈ V
123	122	dmex 7842	. . . . . . . . . . . . . . . . . . . . 21 ⊢ dom (𝐹‘𝑚) ∈ V
124	123	rgenw 3048	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∀𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∈ V
125	124	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ 𝑍 → ∀𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∈ V)
126	121, 125	iinexd 45121	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ 𝑍 → ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∈ V)
127	120, 126	rabexd 5279	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ 𝑍 → {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < ) ∈ ℝ} ∈ V)
128	33, 113, 114, 127	fvmptd3 6953	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ 𝑍 → (𝐸‘𝑛) = {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < ) ∈ ℝ})
129	128	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) = {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < ) ∈ ℝ})
130		ssrab2 4031	. . . . . . . . . . . . . . . 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 6822	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑛 → (𝐻‘𝑘) = (𝐻‘𝑛))
135	134	dmeqd 5848	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑛 → dom (𝐻‘𝑘) = dom (𝐻‘𝑛))
136	135	sseq1d 3967	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → (dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ↔ dom (𝐻‘𝑛) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)))
137	136	rspcev 3577	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ (ℤ_≥‘𝑛) ∧ dom (𝐻‘𝑛) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → ∃𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
138	89, 133, 137	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∃𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
139		iinss 5005	. . . . . . . . . . . 12 ⊢ (∃𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) → ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
140	138, 139	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
141	140	ralrimiva 3121	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
142		ss2iun 4960	. . . . . . . . . 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 497	. . . . . . . . . . . 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 4977	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)
150	67, 149	nfrabw 3432	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛{𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }
151	61, 150	nfel 2906	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }
152	60, 151	nfan 1899	. . . . . . . . . . 11 ⊢ Ⅎ𝑛(𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ })
153	82	simprbi 496	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ )
154		nfv 1914	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘𝜑
155		nfmpt1 5191	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘(𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥))
156		nfcv 2891	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘dom ⇝
157	155, 156	nfel 2906	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘(𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝
158	154, 157	nfan 1899	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘(𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ )
159		nfv 1914	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘 𝑛 ∈ 𝑍
160		nfcv 2891	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘𝑥
161		nfii1 4979	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)
162	160, 161	nfel 2906	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)
163	158, 159, 162	nf3an 1901	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
164	26	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑀 ∈ ℤ)
165	164	3adant3 1132	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → 𝑀 ∈ ℤ)
166	165	3adant1r 1178	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → 𝑀 ∈ ℤ)
167	29	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑆 ∈ SAlg)
168	167	3adant3 1132	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → 𝑆 ∈ SAlg)
169	168	3adant1r 1178	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → 𝑆 ∈ SAlg)
170	31	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝐹:𝑍⟶(SMblFn‘𝑆))
171	170	3adant3 1132	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → 𝐹:𝑍⟶(SMblFn‘𝑆))
172	171	3adant1r 1178	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → 𝐹:𝑍⟶(SMblFn‘𝑆))
173		simp2 1137	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → 𝑛 ∈ 𝑍)
174		simp3 1138	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
175		simp1r 1199	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ )
176	163, 166, 28, 169, 172, 33, 34, 173, 174, 175	smflimsuplem4 46814	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
177	176	3exp 1119	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) → (𝑛 ∈ 𝑍 → (𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)))
178	153, 177	sylan2 593	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }) → (𝑛 ∈ 𝑍 → (𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)))
179	152, 62, 178	rexlimd 3236	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }) → (∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ))
180	148, 179	mpd 15	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
181	180	ralrimiva 3121	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
182	144, 181	jca 511	. . . . . . 7 ⊢ (𝜑 → ({𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∧ ∀𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ))
183		nfrab1 3415	. . . . . . . 8 ⊢ Ⅎ𝑥{𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }
184		nfcv 2891	. . . . . . . 8 ⊢ Ⅎ𝑥∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)
185	183, 184	ssrabf 45102	. . . . . . 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 1927	. . 3 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} ↔ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }))
190		nfrab1 3415	. . . 4 ⊢ Ⅎ𝑥{𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}
191	190, 183	cleqf 2920	. . 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 2764	1 ⊢ (𝜑 → 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ })

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 ∀wal 1538 = wceq 1540 ∈ wcel 2109 ∀wral 3044 ∃wrex 3053 {crab 3394 Vcvv 3436 ⊆ wss 3903 ∪ ciun 4941 ∩ ciin 4942 ↦ cmpt 5173 Or wor 5526 dom cdm 5619 ran crn 5620 Fn wfn 6477 ⟶wf 6478 ‘cfv 6482 supcsup 9330 ℝcr 11008 ℝ^*cxr 11148 < clt 11149 ℤcz 12471 ℤ_≥cuz 12735 lim supclsp 15377 ⇝ cli 15391 SAlgcsalg 46299 SMblFncsmblfn 46686

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 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 ax-cnex 11065 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-addrcl 11070 ax-mulcl 11071 ax-mulrcl 11072 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-i2m1 11077 ax-1ne0 11078 ax-1rid 11079 ax-rnegex 11080 ax-rrecex 11081 ax-cnre 11082 ax-pre-lttri 11083 ax-pre-lttrn 11084 ax-pre-ltadd 11085 ax-pre-mulgt0 11086 ax-pre-sup 11087

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 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3343 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-tp 4582 df-op 4584 df-uni 4859 df-int 4897 df-iun 4943 df-iin 4944 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6249 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-om 7800 df-1st 7924 df-2nd 7925 df-frecs 8214 df-wrecs 8245 df-recs 8294 df-rdg 8332 df-1o 8388 df-2o 8389 df-er 8625 df-pm 8756 df-en 8873 df-dom 8874 df-sdom 8875 df-fin 8876 df-sup 9332 df-inf 9333 df-pnf 11151 df-mnf 11152 df-xr 11153 df-ltxr 11154 df-le 11155 df-sub 11349 df-neg 11350 df-div 11778 df-nn 12129 df-2 12191 df-3 12192 df-n0 12385 df-z 12472 df-uz 12736 df-q 12850 df-rp 12894 df-ioo 13252 df-ico 13254 df-fz 13411 df-fl 13696 df-ceil 13697 df-seq 13909 df-exp 13969 df-cj 15006 df-re 15007 df-im 15008 df-sqrt 15142 df-abs 15143 df-limsup 15378 df-clim 15395 df-rlim 15396 df-smblfn 46687

This theorem is referenced by: smflimsuplem8 46818

W3C validator