Metamath Proof Explorer

Theorem smflimsuplem1

Description: If H converges, the limsup of F is real. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses smflimsuplem1.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
smflimsuplem1.e ⊢ 𝐸 = ( 𝑛 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
smflimsuplem1.h ⊢ 𝐻 = ( 𝑛 ∈ 𝑍 ↦ ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) )
smflimsuplem1.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑍 )
Assertion smflimsuplem1 ( 𝜑 → dom ( 𝐻 ‘ 𝐾 ) ⊆ dom ( 𝐹 ‘ 𝐾 ) )

Proof

Step Hyp Ref Expression
1 smflimsuplem1.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 smflimsuplem1.e ⊢ 𝐸 = ( 𝑛 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
3 smflimsuplem1.h ⊢ 𝐻 = ( 𝑛 ∈ 𝑍 ↦ ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) )
4 smflimsuplem1.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑍 )
5 fveq2 ⊢ ( 𝑚 = 𝑗 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑗 ) )
6 5 fveq1d ⊢ ( 𝑚 = 𝑗 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) )
7 6 cbvmptv ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) )
8 7 rneqi ⊢ ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) )
9 8 supeq1i ⊢ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) = sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < )
10 9 mpteq2i ⊢ ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) = ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) )
11 10 a1i ⊢ ( 𝑛 = 𝐾 → ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) = ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) ) )
12 fveq2 ⊢ ( 𝑛 = 𝐾 → ( 𝐸 ‘ 𝑛 ) = ( 𝐸 ‘ 𝐾 ) )
13 fveq2 ⊢ ( 𝑛 = 𝐾 → ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ 𝐾 ) )
14 13 mpteq1d ⊢ ( 𝑛 = 𝐾 → ( 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) = ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) )
15 14 rneqd ⊢ ( 𝑛 = 𝐾 → ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) = ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) )
16 15 supeq1d ⊢ ( 𝑛 = 𝐾 → sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) = sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) )
17 12 16 mpteq12dv ⊢ ( 𝑛 = 𝐾 → ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) ) = ( 𝑥 ∈ ( 𝐸 ‘ 𝐾 ) ↦ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) ) )
18 11 17 eqtrd ⊢ ( 𝑛 = 𝐾 → ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) = ( 𝑥 ∈ ( 𝐸 ‘ 𝐾 ) ↦ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) ) )
19 fvex ⊢ ( 𝐸 ‘ 𝐾 ) ∈ V
20 19 mptex ⊢ ( 𝑥 ∈ ( 𝐸 ‘ 𝐾 ) ↦ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) ) ∈ V
21 20 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐸 ‘ 𝐾 ) ↦ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) ) ∈ V )
22 3 18 4 21 fvmptd3 ⊢ ( 𝜑 → ( 𝐻 ‘ 𝐾 ) = ( 𝑥 ∈ ( 𝐸 ‘ 𝐾 ) ↦ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) ) )
23 22 dmeqd ⊢ ( 𝜑 → dom ( 𝐻 ‘ 𝐾 ) = dom ( 𝑥 ∈ ( 𝐸 ‘ 𝐾 ) ↦ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) ) )
24 xrltso ⊢ < Or ℝ*
25 24 supex ⊢ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ V
26 eqid ⊢ ( 𝑥 ∈ ( 𝐸 ‘ 𝐾 ) ↦ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) ) = ( 𝑥 ∈ ( 𝐸 ‘ 𝐾 ) ↦ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) )
27 25 26 dmmpti ⊢ dom ( 𝑥 ∈ ( 𝐸 ‘ 𝐾 ) ↦ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) ) = ( 𝐸 ‘ 𝐾 )
28 27 a1i ⊢ ( 𝜑 → dom ( 𝑥 ∈ ( 𝐸 ‘ 𝐾 ) ↦ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) ) = ( 𝐸 ‘ 𝐾 ) )
29 5 dmeqd ⊢ ( 𝑚 = 𝑗 → dom ( 𝐹 ‘ 𝑚 ) = dom ( 𝐹 ‘ 𝑗 ) )
30 29 cbviinv ⊢ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) = ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑗 )
31 30 eleq2i ⊢ ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ↔ 𝑥 ∈ ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑗 ) )
32 9 eleq1i ⊢ ( sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ ↔ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ )
33 31 32 anbi12i ⊢ ( ( 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∧ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ ) ↔ ( 𝑥 ∈ ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑗 ) ∧ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ ) )
34 33 rabbia2 ⊢ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } = { 𝑥 ∈ ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑗 ) ∣ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ }
35 34 a1i ⊢ ( 𝑛 = 𝐾 → { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } = { 𝑥 ∈ ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑗 ) ∣ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
36 13 iineq1d ⊢ ( 𝑛 = 𝐾 → ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑗 ) = ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) dom ( 𝐹 ‘ 𝑗 ) )
37 36 eleq2d ⊢ ( 𝑛 = 𝐾 → ( 𝑥 ∈ ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑗 ) ↔ 𝑥 ∈ ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) dom ( 𝐹 ‘ 𝑗 ) ) )
38 16 eleq1d ⊢ ( 𝑛 = 𝐾 → ( sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ ↔ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ ) )
39 37 38 anbi12d ⊢ ( 𝑛 = 𝐾 → ( ( 𝑥 ∈ ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑗 ) ∧ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ ) ↔ ( 𝑥 ∈ ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) dom ( 𝐹 ‘ 𝑗 ) ∧ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ ) ) )
40 39 rabbidva2 ⊢ ( 𝑛 = 𝐾 → { 𝑥 ∈ ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑗 ) ∣ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } = { 𝑥 ∈ ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) dom ( 𝐹 ‘ 𝑗 ) ∣ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
41 35 40 eqtrd ⊢ ( 𝑛 = 𝐾 → { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } = { 𝑥 ∈ ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) dom ( 𝐹 ‘ 𝑗 ) ∣ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
42 eqid ⊢ { 𝑥 ∈ ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) dom ( 𝐹 ‘ 𝑗 ) ∣ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } = { 𝑥 ∈ ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) dom ( 𝐹 ‘ 𝑗 ) ∣ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ }
43 1 4 eluzelz2d ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
44 uzid ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ( ℤ≥ ‘ 𝐾 ) )
45 ne0i ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝐾 ) → ( ℤ≥ ‘ 𝐾 ) ≠ ∅ )
46 43 44 45 3syl ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝐾 ) ≠ ∅ )
47 fvex ⊢ ( 𝐹 ‘ 𝑗 ) ∈ V
48 47 dmex ⊢ dom ( 𝐹 ‘ 𝑗 ) ∈ V
49 48 rgenw ⊢ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) dom ( 𝐹 ‘ 𝑗 ) ∈ V
50 49 a1i ⊢ ( 𝜑 → ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) dom ( 𝐹 ‘ 𝑗 ) ∈ V )
51 46 50 iinexd ⊢ ( 𝜑 → ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) dom ( 𝐹 ‘ 𝑗 ) ∈ V )
52 42 51 rabexd ⊢ ( 𝜑 → { 𝑥 ∈ ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) dom ( 𝐹 ‘ 𝑗 ) ∣ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ∈ V )
53 2 41 4 52 fvmptd3 ⊢ ( 𝜑 → ( 𝐸 ‘ 𝐾 ) = { 𝑥 ∈ ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) dom ( 𝐹 ‘ 𝑗 ) ∣ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
54 23 28 53 3eqtrd ⊢ ( 𝜑 → dom ( 𝐻 ‘ 𝐾 ) = { 𝑥 ∈ ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) dom ( 𝐹 ‘ 𝑗 ) ∣ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
55 ssrab2 ⊢ { 𝑥 ∈ ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) dom ( 𝐹 ‘ 𝑗 ) ∣ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ⊆ ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) dom ( 𝐹 ‘ 𝑗 )
56 55 a1i ⊢ ( 𝜑 → { 𝑥 ∈ ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) dom ( 𝐹 ‘ 𝑗 ) ∣ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ⊆ ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) dom ( 𝐹 ‘ 𝑗 ) )
57 43 44 syl ⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 𝐾 ) )
58 fveq2 ⊢ ( 𝑗 = 𝐾 → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ 𝐾 ) )
59 58 dmeqd ⊢ ( 𝑗 = 𝐾 → dom ( 𝐹 ‘ 𝑗 ) = dom ( 𝐹 ‘ 𝐾 ) )
60 ssid ⊢ dom ( 𝐹 ‘ 𝐾 ) ⊆ dom ( 𝐹 ‘ 𝐾 )
61 60 a1i ⊢ ( 𝜑 → dom ( 𝐹 ‘ 𝐾 ) ⊆ dom ( 𝐹 ‘ 𝐾 ) )
62 57 59 61 iinssd ⊢ ( 𝜑 → ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) dom ( 𝐹 ‘ 𝑗 ) ⊆ dom ( 𝐹 ‘ 𝐾 ) )
63 56 62 sstrd ⊢ ( 𝜑 → { 𝑥 ∈ ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) dom ( 𝐹 ‘ 𝑗 ) ∣ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ⊆ dom ( 𝐹 ‘ 𝐾 ) )
64 54 63 eqsstrd ⊢ ( 𝜑 → dom ( 𝐻 ‘ 𝐾 ) ⊆ dom ( 𝐹 ‘ 𝐾 ) )