Metamath Proof Explorer

Theorem smflimsuplem7

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)

Ref Expression
Hypotheses 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 smflimsuplem7 ( 𝜑 → 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ } )

Proof

Step Hyp Ref Expression
1 smflimsuplem7.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2 smflimsuplem7.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 smflimsuplem7.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
4 smflimsuplem7.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
5 smflimsuplem7.d ⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ }
6 smflimsuplem7.e ⊢ 𝐸 = ( 𝑘 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
7 smflimsuplem7.h ⊢ 𝐻 = ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ ( 𝐸 ‘ 𝑘 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) )
8 5 a1i ⊢ ( 𝜑 → 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } )
9 simpl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ) → 𝜑 )
10 rabidim2 ⊢ ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
11 10 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
12 rabidim1 ⊢ ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
13 eliun ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ↔ ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
14 12 13 sylib ⊢ ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } → ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
15 14 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ) → ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
16 nfv ⊢ Ⅎ 𝑛 ( 𝜑 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
17 nfv ⊢ Ⅎ 𝑚 𝜑
18 nfcv ⊢ Ⅎ 𝑚 lim sup
19 nfmpt1 ⊢ Ⅎ 𝑚 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) )
20 18 19 nffv ⊢ Ⅎ 𝑚 ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) )
21 nfcv ⊢ Ⅎ 𝑚 ℝ
22 20 21 nfel ⊢ Ⅎ 𝑚 ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ
23 17 22 nfan ⊢ Ⅎ 𝑚 ( 𝜑 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
24 nfv ⊢ Ⅎ 𝑚 𝑛 ∈ 𝑍
25 nfcv ⊢ Ⅎ 𝑚 𝑥
26 nfii1 ⊢ Ⅎ 𝑚 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
27 25 26 nfel ⊢ Ⅎ 𝑚 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
28 23 24 27 nf3an ⊢ Ⅎ 𝑚 ( ( 𝜑 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
29 nfv ⊢ Ⅎ 𝑚 𝑘 ∈ ( ℤ≥ ‘ 𝑛 )
30 28 29 nfan ⊢ Ⅎ 𝑚 ( ( ( 𝜑 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) )
31 simpl1l ⊢ ( ( ( ( 𝜑 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝜑 )
32 31 1 syl ⊢ ( ( ( ( 𝜑 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑀 ∈ ℤ )
33 31 3 syl ⊢ ( ( ( ( 𝜑 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑆 ∈ SAlg )
34 31 4 syl ⊢ ( ( ( ( 𝜑 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
35 2 uztrn2 ⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑘 ∈ 𝑍 )
36 35 3ad2antl2 ⊢ ( ( ( ( 𝜑 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑘 ∈ 𝑍 )
37 simpl1r ⊢ ( ( ( ( 𝜑 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
38 uzss ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) → ( ℤ≥ ‘ 𝑘 ) ⊆ ( ℤ≥ ‘ 𝑛 ) )
39 iinss1 ⊢ ( ( ℤ≥ ‘ 𝑘 ) ⊆ ( ℤ≥ ‘ 𝑛 ) → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ⊆ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐹 ‘ 𝑚 ) )
40 38 39 syl ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ⊆ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐹 ‘ 𝑚 ) )
41 40 adantl ⊢ ( ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ⊆ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐹 ‘ 𝑚 ) )
42 simpl ⊢ ( ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
43 41 42 sseldd ⊢ ( ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐹 ‘ 𝑚 ) )
44 43 3ad2antl3 ⊢ ( ( ( ( 𝜑 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐹 ‘ 𝑚 ) )
45 30 32 2 33 34 6 7 36 37 44 smflimsuplem2 ⊢ ( ( ( ( 𝜑 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑥 ∈ dom ( 𝐻 ‘ 𝑘 ) )
46 45 ralrimiva ⊢ ( ( ( 𝜑 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ dom ( 𝐻 ‘ 𝑘 ) )
47 vex ⊢ 𝑥 ∈ V
48 eliin ⊢ ( 𝑥 ∈ V → ( 𝑥 ∈ ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ dom ( 𝐻 ‘ 𝑘 ) ) )
49 47 48 ax-mp ⊢ ( 𝑥 ∈ ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑥 ∈ dom ( 𝐻 ‘ 𝑘 ) )
50 46 49 sylibr ⊢ ( ( ( 𝜑 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → 𝑥 ∈ ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) )
51 50 3exp ⊢ ( ( 𝜑 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) → ( 𝑛 ∈ 𝑍 → ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) → 𝑥 ∈ ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ) ) )
52 16 51 reximdai ⊢ ( ( 𝜑 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) → ( ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) → ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ) )
53 52 imp ⊢ ( ( ( 𝜑 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ∧ ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) )
54 eliun ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ↔ ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) )
55 53 54 sylibr ⊢ ( ( ( 𝜑 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ∧ ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) )
56 9 11 15 55 syl21anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) )
57 13 biimpi ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) → ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
58 12 57 syl ⊢ ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } → ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
59 58 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ) → ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
60 nfv ⊢ Ⅎ 𝑛 𝜑
61 nfcv ⊢ Ⅎ 𝑛 𝑥
62 nfv ⊢ Ⅎ 𝑛 ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ
63 nfiu1 ⊢ Ⅎ 𝑛 ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
64 62 63 nfrabw ⊢ Ⅎ 𝑛 { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ }
65 61 64 nfel ⊢ Ⅎ 𝑛 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ }
66 60 65 nfan ⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } )
67 nfv ⊢ Ⅎ 𝑛 ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝
68 nfv ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
69 simp1l ⊢ ( ( ( 𝜑 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → 𝜑 )
70 69 1 syl ⊢ ( ( ( 𝜑 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → 𝑀 ∈ ℤ )
71 69 3 syl ⊢ ( ( ( 𝜑 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → 𝑆 ∈ SAlg )
72 69 4 syl ⊢ ( ( ( 𝜑 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
73 simp1r ⊢ ( ( ( 𝜑 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
74 simp2 ⊢ ( ( ( 𝜑 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → 𝑛 ∈ 𝑍 )
75 simp3 ⊢ ( ( ( 𝜑 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
76 68 28 70 2 71 72 6 7 73 74 75 smflimsuplem6 ⊢ ( ( ( 𝜑 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ )
77 76 3exp ⊢ ( ( 𝜑 ∧ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) → ( 𝑛 ∈ 𝑍 → ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) → ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) ) )
78 11 77 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ) → ( 𝑛 ∈ 𝑍 → ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) → ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) ) )
79 66 67 78 rexlimd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ) → ( ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) → ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) )
80 59 79 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ) → ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ )
81 56 80 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ) → ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∧ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) )
82 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ↔ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∧ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) )
83 81 82 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ) → 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ } )
84 83 ex ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } → 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ) )
85 ssrab2 ⊢ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 )
86 85 a1i ⊢ ( 𝜑 → { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) )
87 2 eluzelz2 ⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ )
88 87 uzidd ⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ( ℤ≥ ‘ 𝑛 ) )
89 88 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑛 ) )
90 nfv ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑛 ∈ 𝑍 )
91 xrltso ⊢ < Or ℝ*
92 91 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ) → < Or ℝ* )
93 92 supexd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ) → sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ V )
94 eqid ⊢ ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) = ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) )
95 90 93 94 fnmptd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) Fn ( 𝐸 ‘ 𝑛 ) )
96 fveq2 ⊢ ( 𝑘 = 𝑛 → ( 𝐸 ‘ 𝑘 ) = ( 𝐸 ‘ 𝑛 ) )
97 fveq2 ⊢ ( 𝑘 = 𝑛 → ( ℤ≥ ‘ 𝑘 ) = ( ℤ≥ ‘ 𝑛 ) )
98 97 mpteq1d ⊢ ( 𝑘 = 𝑛 → ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) )
99 98 rneqd ⊢ ( 𝑘 = 𝑛 → ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) )
100 99 supeq1d ⊢ ( 𝑘 = 𝑛 → sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) = sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) )
101 96 100 mpteq12dv ⊢ ( 𝑘 = 𝑛 → ( 𝑥 ∈ ( 𝐸 ‘ 𝑘 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) = ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) )
102 fvex ⊢ ( 𝐸 ‘ 𝑛 ) ∈ V
103 102 mptex ⊢ ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) ∈ V
104 101 7 103 fvmpt ⊢ ( 𝑛 ∈ 𝑍 → ( 𝐻 ‘ 𝑛 ) = ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) )
105 104 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑛 ) = ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) )
106 105 fneq1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐻 ‘ 𝑛 ) Fn ( 𝐸 ‘ 𝑛 ) ↔ ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) Fn ( 𝐸 ‘ 𝑛 ) ) )
107 95 106 mpbird ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑛 ) Fn ( 𝐸 ‘ 𝑛 ) )
108 107 fndmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → dom ( 𝐻 ‘ 𝑛 ) = ( 𝐸 ‘ 𝑛 ) )
109 97 iineq1d ⊢ ( 𝑘 = 𝑛 → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐹 ‘ 𝑚 ) = ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
110 109 eleq2d ⊢ ( 𝑘 = 𝑛 → ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐹 ‘ 𝑚 ) ↔ 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) )
111 100 eleq1d ⊢ ( 𝑘 = 𝑛 → ( sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ ↔ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ ) )
112 110 111 anbi12d ⊢ ( 𝑘 = 𝑛 → ( ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐹 ‘ 𝑚 ) ∧ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ ) ↔ ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∧ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ ) ) )
113 112 rabbidva2 ⊢ ( 𝑘 = 𝑛 → { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } = { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
114 id ⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ 𝑍 )
115 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) )
116 115 mpteq2dv ⊢ ( 𝑥 = 𝑦 → ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) )
117 116 rneqd ⊢ ( 𝑥 = 𝑦 → ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) )
118 117 supeq1d ⊢ ( 𝑥 = 𝑦 → sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) = sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) , ℝ* , < ) )
119 118 eleq1d ⊢ ( 𝑥 = 𝑦 → ( sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ ↔ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) , ℝ* , < ) ∈ ℝ ) )
120 119 cbvrabv ⊢ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } = { 𝑦 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) , ℝ* , < ) ∈ ℝ }
121 88 ne0d ⊢ ( 𝑛 ∈ 𝑍 → ( ℤ≥ ‘ 𝑛 ) ≠ ∅ )
122 fvex ⊢ ( 𝐹 ‘ 𝑚 ) ∈ V
123 122 dmex ⊢ dom ( 𝐹 ‘ 𝑚 ) ∈ V
124 123 rgenw ⊢ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V
125 124 a1i ⊢ ( 𝑛 ∈ 𝑍 → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V )
126 121 125 iinexd ⊢ ( 𝑛 ∈ 𝑍 → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V )
127 120 126 rabexd ⊢ ( 𝑛 ∈ 𝑍 → { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ∈ V )
128 6 113 114 127 fvmptd3 ⊢ ( 𝑛 ∈ 𝑍 → ( 𝐸 ‘ 𝑛 ) = { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
129 128 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) = { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
130 ssrab2 ⊢ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ⊆ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
131 130 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ⊆ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
132 129 131 eqsstrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) ⊆ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
133 108 132 eqsstrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → dom ( 𝐻 ‘ 𝑛 ) ⊆ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
134 fveq2 ⊢ ( 𝑘 = 𝑛 → ( 𝐻 ‘ 𝑘 ) = ( 𝐻 ‘ 𝑛 ) )
135 134 dmeqd ⊢ ( 𝑘 = 𝑛 → dom ( 𝐻 ‘ 𝑘 ) = dom ( 𝐻 ‘ 𝑛 ) )
136 135 sseq1d ⊢ ( 𝑘 = 𝑛 → ( dom ( 𝐻 ‘ 𝑘 ) ⊆ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ↔ dom ( 𝐻 ‘ 𝑛 ) ⊆ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) )
137 136 rspcev ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑛 ) ∧ dom ( 𝐻 ‘ 𝑛 ) ⊆ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ) → ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ⊆ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
138 89 133 137 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ⊆ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
139 iinss ⊢ ( ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ⊆ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) → ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ⊆ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
140 138 139 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ⊆ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
141 140 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ⊆ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
142 ss2iun ⊢ ( ∀ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ⊆ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) → ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
143 141 142 syl ⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
144 86 143 sstrd ⊢ ( 𝜑 → { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
145 82 simplbi ⊢ ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ } → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) )
146 54 biimpi ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) → ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) )
147 145 146 syl ⊢ ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ } → ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) )
148 147 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ) → ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) )
149 nfiu1 ⊢ Ⅎ 𝑛 ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 )
150 67 149 nfrabw ⊢ Ⅎ 𝑛 { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
151 61 150 nfel ⊢ Ⅎ 𝑛 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
152 60 151 nfan ⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ } )
153 82 simprbi ⊢ ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ } → ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ )
154 nfv ⊢ Ⅎ 𝑘 𝜑
155 nfmpt1 ⊢ Ⅎ 𝑘 ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) )
156 nfcv ⊢ Ⅎ 𝑘 dom ⇝
157 155 156 nfel ⊢ Ⅎ 𝑘 ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝
158 154 157 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ )
159 nfv ⊢ Ⅎ 𝑘 𝑛 ∈ 𝑍
160 nfcv ⊢ Ⅎ 𝑘 𝑥
161 nfii1 ⊢ Ⅎ 𝑘 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 )
162 160 161 nfel ⊢ Ⅎ 𝑘 𝑥 ∈ ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 )
163 158 159 162 nf3an ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) )
164 1 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑀 ∈ ℤ )
165 164 3adant3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ) → 𝑀 ∈ ℤ )
166 165 3adant1r ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ) → 𝑀 ∈ ℤ )
167 3 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑆 ∈ SAlg )
168 167 3adant3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ) → 𝑆 ∈ SAlg )
169 168 3adant1r ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ) → 𝑆 ∈ SAlg )
170 4 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
171 170 3adant3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ) → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
172 171 3adant1r ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ) → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
173 simp2 ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ) → 𝑛 ∈ 𝑍 )
174 simp3 ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ) → 𝑥 ∈ ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) )
175 simp1r ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ) → ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ )
176 163 166 2 169 172 6 7 173 174 175 smflimsuplem4 ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
177 176 3exp ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ ) → ( 𝑛 ∈ 𝑍 → ( 𝑥 ∈ ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ) )
178 153 177 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ) → ( 𝑛 ∈ 𝑍 → ( 𝑥 ∈ ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ) )
179 152 62 178 rexlimd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ) → ( ∃ 𝑛 ∈ 𝑍 𝑥 ∈ ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) )
180 148 179 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ) → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
181 180 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ )
182 144 181 jca ⊢ ( 𝜑 → ( { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∧ ∀ 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) )
183 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
184 nfcv ⊢ Ⅎ 𝑥 ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
185 183 184 ssrabf ⊢ ( { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ⊆ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ↔ ( { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ⊆ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∧ ∀ 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ ) )
186 182 185 sylibr ⊢ ( 𝜑 → { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ⊆ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } )
187 186 sseld ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ } → 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ) )
188 84 187 impbid ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ↔ 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ) )
189 188 alrimiv ⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ↔ 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ) )
190 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ }
191 190 183 cleqf ⊢ ( { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ↔ ∀ 𝑥 ( 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } ↔ 𝑥 ∈ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ) )
192 189 191 sylibr ⊢ ( 𝜑 → { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ } = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ } )
193 8 192 eqtrd ⊢ ( 𝜑 → 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐻 ‘ 𝑘 ) ∣ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ dom ⇝ } )