Metamath Proof Explorer

Theorem smflimsuplem2

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 smflimsuplem2.p ⊢ Ⅎ 𝑚 𝜑
smflimsuplem2.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
smflimsuplem2.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
smflimsuplem2.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
smflimsuplem2.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
smflimsuplem2.e ⊢ 𝐸 = ( 𝑛 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
smflimsuplem2.h ⊢ 𝐻 = ( 𝑛 ∈ 𝑍 ↦ ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) )
smflimsuplem2.n ⊢ ( 𝜑 → 𝑛 ∈ 𝑍 )
smflimsuplem2.r ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) ∈ ℝ )
smflimsuplem2.x ⊢ ( 𝜑 → 𝑋 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
Assertion smflimsuplem2 ( 𝜑 → 𝑋 ∈ dom ( 𝐻 ‘ 𝑛 ) )

Proof

Step Hyp Ref Expression
1 smflimsuplem2.p ⊢ Ⅎ 𝑚 𝜑
2 smflimsuplem2.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 smflimsuplem2.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4 smflimsuplem2.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
5 smflimsuplem2.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
6 smflimsuplem2.e ⊢ 𝐸 = ( 𝑛 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
7 smflimsuplem2.h ⊢ 𝐻 = ( 𝑛 ∈ 𝑍 ↦ ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) )
8 smflimsuplem2.n ⊢ ( 𝜑 → 𝑛 ∈ 𝑍 )
9 smflimsuplem2.r ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) ∈ ℝ )
10 smflimsuplem2.x ⊢ ( 𝜑 → 𝑋 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
11 eqid ⊢ ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ 𝑛 )
12 8 3 eleqtrdi ⊢ ( 𝜑 → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
13 uzss ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ 𝑛 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
14 12 13 syl ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝑛 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
15 14 3 sseqtrrdi ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝑛 ) ⊆ 𝑍 )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ℤ≥ ‘ 𝑛 ) ⊆ 𝑍 )
17 simpr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) )
18 16 17 sseldd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ 𝑍 )
19 4 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → 𝑆 ∈ SAlg )
20 5 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) ∈ ( SMblFn ‘ 𝑆 ) )
21 eqid ⊢ dom ( 𝐹 ‘ 𝑚 ) = dom ( 𝐹 ‘ 𝑚 )
22 19 20 21 smff ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) : dom ( 𝐹 ‘ 𝑚 ) ⟶ ℝ )
23 18 22 syldan ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( 𝐹 ‘ 𝑚 ) : dom ( 𝐹 ‘ 𝑚 ) ⟶ ℝ )
24 iinss2 ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ⊆ dom ( 𝐹 ‘ 𝑚 ) )
25 24 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ⊆ dom ( 𝐹 ‘ 𝑚 ) )
26 10 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑋 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
27 25 26 sseldd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑋 ∈ dom ( 𝐹 ‘ 𝑚 ) )
28 23 27 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ∈ ℝ )
29 nfmpt1 ⊢ Ⅎ 𝑚 ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) )
30 nfmpt1 ⊢ Ⅎ 𝑚 ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) )
31 eluzelz ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑛 ∈ ℤ )
32 12 31 syl ⊢ ( 𝜑 → 𝑛 ∈ ℤ )
33 eqid ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) = ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) )
34 1 28 33 fmptdf ⊢ ( 𝜑 → ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) : ( ℤ≥ ‘ 𝑛 ) ⟶ ℝ )
35 34 ffnd ⊢ ( 𝜑 → ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) Fn ( ℤ≥ ‘ 𝑛 ) )
36 nfcv ⊢ Ⅎ 𝑚 ( ℤ≥ ‘ 𝑀 )
37 fvexd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ∈ V )
38 36 1 37 mptfnd ⊢ ( 𝜑 → ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) Fn ( ℤ≥ ‘ 𝑀 ) )
39 33 a1i ⊢ ( 𝜑 → ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) = ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) )
40 fvexd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ∈ V )
41 39 40 fvmpt2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ‘ 𝑚 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) )
42 18 3 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) )
43 eqid ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) = ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) )
44 43 fvmpt2 ⊢ ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ∈ V ) → ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ‘ 𝑚 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) )
45 42 40 44 syl2anc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ‘ 𝑚 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) )
46 41 45 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ‘ 𝑚 ) = ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ‘ 𝑚 ) )
47 1 29 30 32 35 2 38 32 46 limsupequz ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) = ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) )
48 3 eqcomi ⊢ ( ℤ≥ ‘ 𝑀 ) = 𝑍
49 48 mpteq1i ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) )
50 49 fveq2i ⊢ ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) = ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) )
51 50 a1i ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) = ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) )
52 47 51 eqtrd ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) = ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) )
53 9 renepnfd ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) ≠ +∞ )
54 52 53 eqnetrd ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) ≠ +∞ )
55 1 11 28 54 limsupubuzmpt ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ≤ 𝑦 )
56 uzid ⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ( ℤ≥ ‘ 𝑛 ) )
57 ne0i ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑛 ) → ( ℤ≥ ‘ 𝑛 ) ≠ ∅ )
58 32 56 57 3syl ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝑛 ) ≠ ∅ )
59 1 58 28 supxrre3rnmpt ⊢ ( 𝜑 → ( sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) , ℝ* , < ) ∈ ℝ ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ≤ 𝑦 ) )
60 55 59 mpbird ⊢ ( 𝜑 → sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) , ℝ* , < ) ∈ ℝ )
61 10 60 jca ⊢ ( 𝜑 → ( 𝑋 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∧ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) , ℝ* , < ) ∈ ℝ ) )
62 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) )
63 62 mpteq2dv ⊢ ( 𝑥 = 𝑦 → ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) )
64 63 rneqd ⊢ ( 𝑥 = 𝑦 → ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) )
65 64 supeq1d ⊢ ( 𝑥 = 𝑦 → sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) = sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) , ℝ* , < ) )
66 65 eleq1d ⊢ ( 𝑥 = 𝑦 → ( sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ ↔ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) , ℝ* , < ) ∈ ℝ ) )
67 66 cbvrabv ⊢ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } = { 𝑦 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) , ℝ* , < ) ∈ ℝ }
68 67 eleq2i ⊢ ( 𝑋 ∈ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ↔ 𝑋 ∈ { 𝑦 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) , ℝ* , < ) ∈ ℝ } )
69 fveq2 ⊢ ( 𝑦 = 𝑋 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) )
70 69 mpteq2dv ⊢ ( 𝑦 = 𝑋 → ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) = ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) )
71 70 rneqd ⊢ ( 𝑦 = 𝑋 → ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) = ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) )
72 71 supeq1d ⊢ ( 𝑦 = 𝑋 → sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) , ℝ* , < ) = sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) , ℝ* , < ) )
73 72 eleq1d ⊢ ( 𝑦 = 𝑋 → ( sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) , ℝ* , < ) ∈ ℝ ↔ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) , ℝ* , < ) ∈ ℝ ) )
74 73 elrab ⊢ ( 𝑋 ∈ { 𝑦 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) , ℝ* , < ) ∈ ℝ } ↔ ( 𝑋 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∧ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) , ℝ* , < ) ∈ ℝ ) )
75 68 74 bitri ⊢ ( 𝑋 ∈ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ↔ ( 𝑋 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∧ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) , ℝ* , < ) ∈ ℝ ) )
76 61 75 sylibr ⊢ ( 𝜑 → 𝑋 ∈ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
77 id ⊢ ( 𝜑 → 𝜑 )
78 7 a1i ⊢ ( 𝜑 → 𝐻 = ( 𝑛 ∈ 𝑍 ↦ ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) ) )
79 nfcv ⊢ Ⅎ 𝑥 𝑍
80 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ }
81 79 80 nfmpt ⊢ Ⅎ 𝑥 ( 𝑛 ∈ 𝑍 ↦ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
82 6 81 nfcxfr ⊢ Ⅎ 𝑥 𝐸
83 nfcv ⊢ Ⅎ 𝑥 𝑛
84 82 83 nffv ⊢ Ⅎ 𝑥 ( 𝐸 ‘ 𝑛 )
85 fvex ⊢ ( 𝐸 ‘ 𝑛 ) ∈ V
86 84 85 mptexf ⊢ ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) ∈ V
87 86 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) ∈ V )
88 78 87 fvmpt2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑛 ) = ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) )
89 77 8 88 syl2anc ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑛 ) = ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) )
90 89 dmeqd ⊢ ( 𝜑 → dom ( 𝐻 ‘ 𝑛 ) = dom ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) )
91 nfcv ⊢ Ⅎ 𝑦 ( 𝐸 ‘ 𝑛 )
92 nfcv ⊢ Ⅎ 𝑦 sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < )
93 nfcv ⊢ Ⅎ 𝑥 sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) , ℝ* , < )
94 84 91 92 93 65 cbvmptf ⊢ ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) = ( 𝑦 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) , ℝ* , < ) )
95 xrltso ⊢ < Or ℝ*
96 95 supex ⊢ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) , ℝ* , < ) ∈ V
97 96 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐸 ‘ 𝑛 ) ) → sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) , ℝ* , < ) ∈ V )
98 94 97 dmmptd ⊢ ( 𝜑 → dom ( 𝑥 ∈ ( 𝐸 ‘ 𝑛 ) ↦ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ) = ( 𝐸 ‘ 𝑛 ) )
99 eqid ⊢ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } = { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ }
100 fvex ⊢ ( 𝐹 ‘ 𝑚 ) ∈ V
101 100 dmex ⊢ dom ( 𝐹 ‘ 𝑚 ) ∈ V
102 101 rgenw ⊢ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V
103 102 a1i ⊢ ( 𝜑 → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V )
104 58 103 iinexd ⊢ ( 𝜑 → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V )
105 99 104 rabexd ⊢ ( 𝜑 → { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ∈ V )
106 6 fvmpt2 ⊢ ( ( 𝑛 ∈ 𝑍 ∧ { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ∈ V ) → ( 𝐸 ‘ 𝑛 ) = { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
107 8 105 106 syl2anc ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑛 ) = { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
108 90 98 107 3eqtrrd ⊢ ( 𝜑 → { 𝑥 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } = dom ( 𝐻 ‘ 𝑛 ) )
109 76 108 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ dom ( 𝐻 ‘ 𝑛 ) )