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 47662

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 488	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → 𝜑)
4		rabidim2 45942	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
5	4	adantl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
6		rabidim1 3436	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
7		eliun 4958	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ↔ ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
8	6, 7	sylib 221	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
9	8	adantl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
10		nfv 1947	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛(𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
11		nfv 1947	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑚𝜑
12		nfcv 2924	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑚lim sup
13		nfmpt1 5208	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑚(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))
14	12, 13	nffv 6892	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑚(lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))
15		nfcv 2924	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑚ℝ
16	14, 15	nfel 2938	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑚(lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ
17	11, 16	nfan 1932	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑚(𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
18		nfv 1947	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑚 𝑛 ∈ 𝑍
19		nfcv 2924	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑚𝑥
20		nfii1 4991	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑚∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)
21	19, 20	nfel 2938	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑚 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)
22	17, 18, 21	nf3an 1934	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑚((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
23		nfv 1947	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑚 𝑘 ∈ (ℤ_≥‘𝑛)
24	22, 23	nfan 1932	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑚(((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘𝑛))
25		simpl1l 1243	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝜑)
26		smflimsuplem7.m	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℤ)
27	25, 26	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑀 ∈ ℤ)
28		smflimsuplem7.z	. . . . . . . . . . . . . . . 16 ⊢ 𝑍 = (ℤ_≥‘𝑀)
29		smflimsuplem7.s	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑆 ∈ SAlg)
30	25, 29	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑆 ∈ SAlg)
31		smflimsuplem7.f	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))
32	25, 31	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝐹:𝑍⟶(SMblFn‘𝑆))
33		smflimsuplem7.e	. . . . . . . . . . . . . . . 16 ⊢ 𝐸 = (𝑘 ∈ 𝑍 ↦ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < ) ∈ ℝ})
34		smflimsuplem7.h	. . . . . . . . . . . . . . . 16 ⊢ 𝐻 = (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ (𝐸‘𝑘) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < )))
35	28	uztrn2 12910	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑘 ∈ 𝑍)
36	35	3ad2antl2 1205	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑘 ∈ 𝑍)
37		simpl1r 1244	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
38		uzss 12914	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (ℤ_≥‘𝑛) → (ℤ_≥‘𝑘) ⊆ (ℤ_≥‘𝑛))
39		iinss1 4970	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℤ_≥‘𝑘) ⊆ (ℤ_≥‘𝑛) → ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚))
40	38, 39	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (ℤ_≥‘𝑛) → ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚))
41	40	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚))
42		simpl 488	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
43	41, 42	sseldd 3935	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚))
44	43	3ad2antl3 1206	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚))
45	24, 27, 28, 30, 32, 33, 34, 36, 37, 44	smflimsuplem2 47657	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑥 ∈ dom (𝐻‘𝑘))
46	45	ralrimiva 3156	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → ∀𝑘 ∈ (ℤ_≥‘𝑛)𝑥 ∈ dom (𝐻‘𝑘))
47		vex 3457	. . . . . . . . . . . . . . 15 ⊢ 𝑥 ∈ V
48		eliin 4959	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ V → (𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ↔ ∀𝑘 ∈ (ℤ_≥‘𝑛)𝑥 ∈ dom (𝐻‘𝑘)))
49	47, 48	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ↔ ∀𝑘 ∈ (ℤ_≥‘𝑛)𝑥 ∈ dom (𝐻‘𝑘))
50	46, 49	sylibr 237	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
51	50	3exp 1137	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) → (𝑛 ∈ 𝑍 → (𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) → 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))))
52	10, 51	reximdai 3266	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) → (∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)))
53	52	imp 412	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
54		eliun 4958	. . . . . . . . . 10 ⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ↔ ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
55	53, 54	sylibr 237	. . . . . . . . 9 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
56	3, 5, 9, 55	syl21anc 851	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
57	7	biimpi 219	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
58	6, 57	syl 18	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
59	58	adantl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
60		nfv 1947	. . . . . . . . . . 11 ⊢ Ⅎ𝑛𝜑
61		nfcv 2924	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛𝑥
62		nfv 1947	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛(lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ
63		nfiu1 4990	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)
64	62, 63	nfrabw 3450	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛{𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}
65	61, 64	nfel 2938	. . . . . . . . . . 11 ⊢ Ⅎ𝑛 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}
66	60, 65	nfan 1932	. . . . . . . . . 10 ⊢ Ⅎ𝑛(𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ})
67		nfv 1947	. . . . . . . . . 10 ⊢ Ⅎ𝑛(𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝
68		nfv 1947	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
69		simp1l 1216	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → 𝜑)
70	69, 26	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → 𝑀 ∈ ℤ)
71	69, 29	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → 𝑆 ∈ SAlg)
72	69, 31	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → 𝐹:𝑍⟶(SMblFn‘𝑆))
73		simp1r 1217	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
74		simp2 1155	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → 𝑛 ∈ 𝑍)
75		simp3 1156	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
76	68, 22, 70, 28, 71, 72, 33, 34, 73, 74, 75	smflimsuplem6 47661	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ )
77	76	3exp 1137	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ) → (𝑛 ∈ 𝑍 → (𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ )))
78	5, 77	syldan 603	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → (𝑛 ∈ 𝑍 → (𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ )))
79	66, 67, 78	rexlimd 3271	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → (∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ))
80	59, 79	mpd 16	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ )
81	56, 80	jca 521	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ))
82		rabid 3435	. . . . . . 7 ⊢ (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ↔ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ))
83	81, 82	sylibr 237	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}) → 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ })
84	83	ex 418	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} → 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }))
85		ssrab2 4031	. . . . . . . . . 10 ⊢ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)
86	85	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
87	28	eluzelz2 46239	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ)
88	87	uzidd 12907	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (ℤ_≥‘𝑛))
89	88	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ (ℤ_≥‘𝑛))
90		nfv 1947	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑛 ∈ 𝑍)
91		xrltso 13196	. . . . . . . . . . . . . . . . . . 19 ⊢ < Or ℝ^*
92	91	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ (𝐸‘𝑛)) → < Or ℝ^*)
93	92	supexd 9427	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ (𝐸‘𝑛)) → sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < ) ∈ V)
94		eqid 2762	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < )) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ))
95	90, 93, 94	fnmptd 6677	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < )) Fn (𝐸‘𝑛))
96		fveq2 6882	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑛 → (𝐸‘𝑘) = (𝐸‘𝑛))
97		fveq2 6882	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑛 → (ℤ_≥‘𝑘) = (ℤ_≥‘𝑛))
98	97	mpteq1d 5199	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 𝑛 → (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)))
99	98	rneqd 5926	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑛 → ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)) = ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)))
100	99	supeq1d 9420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑛 → sup(ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) = sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ))
101	96, 100	mpteq12dv 5196	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑛 → (𝑥 ∈ (𝐸‘𝑘) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < )) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < )))
102		fvex 6895	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐸‘𝑛) ∈ V
103	102	mptex 7226	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < )) ∈ V
104	101, 34, 103	fvmpt 6990	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ 𝑍 → (𝐻‘𝑛) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < )))
105	104	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐻‘𝑛) = (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < )))
106	105	fneq1d 6629	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐻‘𝑛) Fn (𝐸‘𝑛) ↔ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < )) Fn (𝐸‘𝑛)))
107	95, 106	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐻‘𝑛) Fn (𝐸‘𝑛))
108	107	fndmd 6641	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom (𝐻‘𝑛) = (𝐸‘𝑛))
109	97	iineq1d 45930	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑛 → ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚) = ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
110	109	eleq2d 2848	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑛 → (𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚) ↔ 𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)))
111	100	eleq1d 2847	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑛 → (sup(ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ ↔ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ))
112	110, 111	anbi12d 644	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑛 → ((𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚) ∧ sup(ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ) ↔ (𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∧ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ)))
113	112	rabbidva2 3416	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑛 → {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑘)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ} = {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ})
114		id 23	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ 𝑍)
115		fveq2 6882	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑚)‘𝑥) = ((𝐹‘𝑚)‘𝑦))
116	115	mpteq2dv 5203	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑦 → (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) = (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)))
117	116	rneqd 5926	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)) = ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)))
118	117	supeq1d 9420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) = sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)), ℝ^, < ))
119	118	eleq1d 2847	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → (sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ ↔ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)), ℝ^, < ) ∈ ℝ))
120	119	cbvrabv 3424	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^, < ) ∈ ℝ} = {𝑦 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑦)), ℝ^, < ) ∈ ℝ}
121	88	ne0d 4291	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ 𝑍 → (ℤ_≥‘𝑛) ≠ ∅)
122		fvex 6895	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹‘𝑚) ∈ V
123	122	dmex 7910	. . . . . . . . . . . . . . . . . . . . 21 ⊢ dom (𝐹‘𝑚) ∈ V
124	123	rgenw 3082	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∀𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∈ V
125	124	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ 𝑍 → ∀𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∈ V)
126	121, 125	iinexd 45973	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ 𝑍 → ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∈ V)
127	120, 126	rabexd 5308	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ 𝑍 → {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < ) ∈ ℝ} ∈ V)
128	33, 113, 114, 127	fvmptd3 7014	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ 𝑍 → (𝐸‘𝑛) = {𝑥 ∈ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ^*, < ) ∈ ℝ})
129	128	adantl 487	. . . . . . . . . . . . . . 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 3968	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
133	108, 132	eqsstrd 3968	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom (𝐻‘𝑛) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
134		fveq2 6882	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑛 → (𝐻‘𝑘) = (𝐻‘𝑛))
135	134	dmeqd 5893	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑛 → dom (𝐻‘𝑘) = dom (𝐻‘𝑛))
136	135	sseq1d 3965	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → (dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ↔ dom (𝐻‘𝑛) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)))
137	136	rspcev 3579	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ (ℤ_≥‘𝑛) ∧ dom (𝐻‘𝑛) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)) → ∃𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
138	89, 133, 137	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∃𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
139		iinss 5019	. . . . . . . . . . . 12 ⊢ (∃𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) → ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
140	138, 139	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
141	140	ralrimiva 3156	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
142		ss2iun 4973	. . . . . . . . . 10 ⊢ (∀𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) → ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
143	141, 142	syl 18	. . . . . . . . 9 ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
144	86, 143	sstrd 3944	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚))
145	82	simplbi 502	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
146	54	biimpi 219	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
147	145, 146	syl 18	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
148	147	adantl 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
149		nfiu1 4990	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)
150	67, 149	nfrabw 3450	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛{𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }
151	61, 150	nfel 2938	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }
152	60, 151	nfan 1932	. . . . . . . . . . 11 ⊢ Ⅎ𝑛(𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ })
153	82	simprbi 503	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ )
154		nfv 1947	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘𝜑
155		nfmpt1 5208	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘(𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥))
156		nfcv 2924	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘dom ⇝
157	155, 156	nfel 2938	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘(𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝
158	154, 157	nfan 1932	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘(𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ )
159		nfv 1947	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘 𝑛 ∈ 𝑍
160		nfcv 2924	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘𝑥
161		nfii1 4991	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)
162	160, 161	nfel 2938	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)
163	158, 159, 162	nf3an 1934	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
164	26	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑀 ∈ ℤ)
165	164	3adant3 1150	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → 𝑀 ∈ ℤ)
166	165	3adant1r 1196	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → 𝑀 ∈ ℤ)
167	29	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑆 ∈ SAlg)
168	167	3adant3 1150	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → 𝑆 ∈ SAlg)
169	168	3adant1r 1196	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → 𝑆 ∈ SAlg)
170	31	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝐹:𝑍⟶(SMblFn‘𝑆))
171	170	3adant3 1150	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → 𝐹:𝑍⟶(SMblFn‘𝑆))
172	171	3adant1r 1196	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → 𝐹:𝑍⟶(SMblFn‘𝑆))
173		simp2 1155	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → 𝑛 ∈ 𝑍)
174		simp3 1156	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘))
175		simp1r 1217	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ )
176	163, 166, 28, 169, 172, 33, 34, 173, 174, 175	smflimsuplem4 47659	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘)) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
177	176	3exp 1137	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ ) → (𝑛 ∈ 𝑍 → (𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)))
178	153, 177	sylan2 605	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }) → (𝑛 ∈ 𝑍 → (𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)))
179	152, 62, 178	rexlimd 3271	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }) → (∃𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ))
180	148, 179	mpd 16	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }) → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
181	180	ralrimiva 3156	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
182	144, 181	jca 521	. . . . . . 7 ⊢ (𝜑 → ({𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∧ ∀𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ))
183		nfrab1 3434	. . . . . . . 8 ⊢ Ⅎ𝑥{𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }
184		nfcv 2924	. . . . . . . 8 ⊢ Ⅎ𝑥∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚)
185	183, 184	ssrabf 45954	. . . . . . 7 ⊢ ({𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} ↔ ({𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∧ ∀𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ))
186	182, 185	sylibr 237	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ⊆ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ})
187	186	sseld 3933	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } → 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}))
188	84, 187	impbid 215	. . . 4 ⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} ↔ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }))
189	188	alrimiv 1960	. . 3 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} ↔ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }))
190		nfrab1 3434	. . . 4 ⊢ Ⅎ𝑥{𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}
191	190, 183	cleqf 2952	. . 3 ⊢ ({𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ } ↔ ∀𝑥(𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} ↔ 𝑥 ∈ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ }))
192	189, 191	sylibr 237	. 2 ⊢ (𝜑 → {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ} = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ })
193	2, 192	eqtrd 2797	1 ⊢ (𝜑 → 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ_≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ })

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 ∀wal 1568 = wceq 1570 ∈ wcel 2145 ∀wral 3078 ∃wrex 3088 {crab 3414 Vcvv 3453 ⊆ wss 3902 ∪ ciun 4954 ∩ ciin 4955 ↦ cmpt 5190 Or wor 5566 dom cdm 5659 ran crn 5660 Fn wfn 6532 ⟶wf 6533 ‘cfv 6537 supcsup 9414 ℝcr 11127 ℝ^*cxr 11270 < clt 11271 ℤcz 12619 ℤ_≥cuz 12891 lim supclsp 15561 ⇝ cli 15575 SAlgcsalg 47144 SMblFncsmblfn 47531

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7740 ax-cnex 11184 ax-resscn 11185 ax-1cn 11186 ax-icn 11187 ax-addcl 11188 ax-addrcl 11189 ax-mulcl 11190 ax-mulrcl 11191 ax-mulcom 11192 ax-addass 11193 ax-mulass 11194 ax-distr 11195 ax-i2m1 11196 ax-1ne0 11197 ax-1rid 11198 ax-rnegex 11199 ax-rrecex 11200 ax-cnre 11201 ax-pre-lttri 11202 ax-pre-lttrn 11203 ax-pre-ltadd 11204 ax-pre-mulgt0 11205 ax-pre-sup 11206

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7374 df-ov 7420 df-oprab 7421 df-mpo 7422 df-om 7867 df-1st 7990 df-2nd 7991 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-2o 8460 df-er 8700 df-pm 8833 df-en 8957 df-dom 8958 df-sdom 8959 df-fin 8960 df-sup 9416 df-inf 9417 df-pnf 11273 df-mnf 11274 df-xr 11275 df-ltxr 11276 df-le 11277 df-sub 11471 df-neg 11472 df-div 11900 df-nn 12262 df-2 12331 df-3 12332 df-n0 12533 df-z 12620 df-uz 12892 df-q 13002 df-rp 13047 df-ioo 13406 df-ico 13408 df-fz 13566 df-fl 13857 df-ceil 13858 df-seq 14070 df-exp 14130 df-cj 15190 df-re 15191 df-im 15192 df-sqrt 15326 df-abs 15327 df-limsup 15562 df-clim 15579 df-rlim 15580 df-smblfn 47532

This theorem is used by: smflimsuplem8 47663

W3C validator