Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  smflimsuplem2 Structured version   Visualization version   GIF version

Theorem smflimsuplem2 41599
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
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
Ref Expression
smflimsuplem2 (𝜑𝑋 ∈ dom (𝐻𝑛))
Distinct variable groups:   𝑥,𝐹   𝑚,𝑀   𝑚,𝑋   𝑚,𝑍,𝑛,𝑥
Allowed substitution hints:   𝜑(𝑥,𝑚,𝑛)   𝑆(𝑥,𝑚,𝑛)   𝐸(𝑥,𝑚,𝑛)   𝐹(𝑚,𝑛)   𝐻(𝑥,𝑚,𝑛)   𝑀(𝑥,𝑛)   𝑋(𝑥,𝑛)

Proof of Theorem smflimsuplem2
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 smflimsuplem2.x . . . 4 (𝜑𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
2 smflimsuplem2.p . . . . . 6 𝑚𝜑
3 eqid 2764 . . . . . 6 (ℤ𝑛) = (ℤ𝑛)
4 smflimsuplem2.n . . . . . . . . . . . . 13 (𝜑𝑛𝑍)
5 smflimsuplem2.z . . . . . . . . . . . . 13 𝑍 = (ℤ𝑀)
64, 5syl6eleq 2853 . . . . . . . . . . . 12 (𝜑𝑛 ∈ (ℤ𝑀))
7 uzss 11906 . . . . . . . . . . . 12 (𝑛 ∈ (ℤ𝑀) → (ℤ𝑛) ⊆ (ℤ𝑀))
86, 7syl 17 . . . . . . . . . . 11 (𝜑 → (ℤ𝑛) ⊆ (ℤ𝑀))
98, 5syl6sseqr 3811 . . . . . . . . . 10 (𝜑 → (ℤ𝑛) ⊆ 𝑍)
109adantr 472 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ𝑛)) → (ℤ𝑛) ⊆ 𝑍)
11 simpr 477 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ𝑛)) → 𝑚 ∈ (ℤ𝑛))
1210, 11sseldd 3761 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ𝑛)) → 𝑚𝑍)
13 smflimsuplem2.s . . . . . . . . . 10 (𝜑𝑆 ∈ SAlg)
1413adantr 472 . . . . . . . . 9 ((𝜑𝑚𝑍) → 𝑆 ∈ SAlg)
15 smflimsuplem2.f . . . . . . . . . 10 (𝜑𝐹:𝑍⟶(SMblFn‘𝑆))
1615ffvelrnda 6548 . . . . . . . . 9 ((𝜑𝑚𝑍) → (𝐹𝑚) ∈ (SMblFn‘𝑆))
17 eqid 2764 . . . . . . . . 9 dom (𝐹𝑚) = dom (𝐹𝑚)
1814, 16, 17smff 41513 . . . . . . . 8 ((𝜑𝑚𝑍) → (𝐹𝑚):dom (𝐹𝑚)⟶ℝ)
1912, 18syldan 585 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ𝑛)) → (𝐹𝑚):dom (𝐹𝑚)⟶ℝ)
20 iinss2 4727 . . . . . . . . 9 (𝑚 ∈ (ℤ𝑛) → 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ⊆ dom (𝐹𝑚))
2120adantl 473 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ𝑛)) → 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ⊆ dom (𝐹𝑚))
221adantr 472 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ𝑛)) → 𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
2321, 22sseldd 3761 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ𝑛)) → 𝑋 ∈ dom (𝐹𝑚))
2419, 23ffvelrnd 6549 . . . . . 6 ((𝜑𝑚 ∈ (ℤ𝑛)) → ((𝐹𝑚)‘𝑋) ∈ ℝ)
25 nfmpt1 4905 . . . . . . . . 9 𝑚(𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋))
26 nfmpt1 4905 . . . . . . . . 9 𝑚(𝑚 ∈ (ℤ𝑀) ↦ ((𝐹𝑚)‘𝑋))
27 eluzelz 11895 . . . . . . . . . 10 (𝑛 ∈ (ℤ𝑀) → 𝑛 ∈ ℤ)
286, 27syl 17 . . . . . . . . 9 (𝜑𝑛 ∈ ℤ)
29 eqid 2764 . . . . . . . . . . 11 (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋)) = (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋))
302, 24, 29fmptdf 6576 . . . . . . . . . 10 (𝜑 → (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋)):(ℤ𝑛)⟶ℝ)
3130ffnd 6223 . . . . . . . . 9 (𝜑 → (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋)) Fn (ℤ𝑛))
32 smflimsuplem2.m . . . . . . . . 9 (𝜑𝑀 ∈ ℤ)
33 nfcv 2906 . . . . . . . . . 10 𝑚(ℤ𝑀)
34 fvexd 6389 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ𝑀)) → ((𝐹𝑚)‘𝑋) ∈ V)
3533, 2, 34mptfnd 40025 . . . . . . . . 9 (𝜑 → (𝑚 ∈ (ℤ𝑀) ↦ ((𝐹𝑚)‘𝑋)) Fn (ℤ𝑀))
3629a1i 11 . . . . . . . . . . 11 (𝜑 → (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋)) = (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋)))
37 fvexd 6389 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ𝑛)) → ((𝐹𝑚)‘𝑋) ∈ V)
3836, 37fvmpt2d 6481 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ𝑛)) → ((𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋))‘𝑚) = ((𝐹𝑚)‘𝑋))
3912, 5syl6eleq 2853 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ𝑛)) → 𝑚 ∈ (ℤ𝑀))
40 eqid 2764 . . . . . . . . . . . 12 (𝑚 ∈ (ℤ𝑀) ↦ ((𝐹𝑚)‘𝑋)) = (𝑚 ∈ (ℤ𝑀) ↦ ((𝐹𝑚)‘𝑋))
4140fvmpt2 6479 . . . . . . . . . . 11 ((𝑚 ∈ (ℤ𝑀) ∧ ((𝐹𝑚)‘𝑋) ∈ V) → ((𝑚 ∈ (ℤ𝑀) ↦ ((𝐹𝑚)‘𝑋))‘𝑚) = ((𝐹𝑚)‘𝑋))
4239, 37, 41syl2anc 579 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ𝑛)) → ((𝑚 ∈ (ℤ𝑀) ↦ ((𝐹𝑚)‘𝑋))‘𝑚) = ((𝐹𝑚)‘𝑋))
4338, 42eqtr4d 2801 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ𝑛)) → ((𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋))‘𝑚) = ((𝑚 ∈ (ℤ𝑀) ↦ ((𝐹𝑚)‘𝑋))‘𝑚))
442, 25, 26, 28, 31, 32, 35, 28, 43limsupequz 40525 . . . . . . . 8 (𝜑 → (lim sup‘(𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋))) = (lim sup‘(𝑚 ∈ (ℤ𝑀) ↦ ((𝐹𝑚)‘𝑋))))
455eqcomi 2773 . . . . . . . . . . 11 (ℤ𝑀) = 𝑍
4645mpteq1i 4897 . . . . . . . . . 10 (𝑚 ∈ (ℤ𝑀) ↦ ((𝐹𝑚)‘𝑋)) = (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋))
4746fveq2i 6377 . . . . . . . . 9 (lim sup‘(𝑚 ∈ (ℤ𝑀) ↦ ((𝐹𝑚)‘𝑋))) = (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋)))
4847a1i 11 . . . . . . . 8 (𝜑 → (lim sup‘(𝑚 ∈ (ℤ𝑀) ↦ ((𝐹𝑚)‘𝑋))) = (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋))))
4944, 48eqtrd 2798 . . . . . . 7 (𝜑 → (lim sup‘(𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋))) = (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋))))
50 smflimsuplem2.r . . . . . . . 8 (𝜑 → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋))) ∈ ℝ)
5150renepnfd 10343 . . . . . . 7 (𝜑 → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑋))) ≠ +∞)
5249, 51eqnetrd 3003 . . . . . 6 (𝜑 → (lim sup‘(𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋))) ≠ +∞)
532, 3, 24, 52limsupubuzmpt 40521 . . . . 5 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑚 ∈ (ℤ𝑛)((𝐹𝑚)‘𝑋) ≤ 𝑦)
54 uzid 11900 . . . . . . 7 (𝑛 ∈ ℤ → 𝑛 ∈ (ℤ𝑛))
55 ne0i 4084 . . . . . . 7 (𝑛 ∈ (ℤ𝑛) → (ℤ𝑛) ≠ ∅)
5628, 54, 553syl 18 . . . . . 6 (𝜑 → (ℤ𝑛) ≠ ∅)
572, 56, 24supxrre3rnmpt 40225 . . . . 5 (𝜑 → (sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋)), ℝ*, < ) ∈ ℝ ↔ ∃𝑦 ∈ ℝ ∀𝑚 ∈ (ℤ𝑛)((𝐹𝑚)‘𝑋) ≤ 𝑦))
5853, 57mpbird 248 . . . 4 (𝜑 → sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋)), ℝ*, < ) ∈ ℝ)
591, 58jca 507 . . 3 (𝜑 → (𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∧ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋)), ℝ*, < ) ∈ ℝ))
60 fveq2 6374 . . . . . . . . . 10 (𝑥 = 𝑦 → ((𝐹𝑚)‘𝑥) = ((𝐹𝑚)‘𝑦))
6160mpteq2dv 4903 . . . . . . . . 9 (𝑥 = 𝑦 → (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)) = (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑦)))
6261rneqd 5520 . . . . . . . 8 (𝑥 = 𝑦 → ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)) = ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑦)))
6362supeq1d 8558 . . . . . . 7 (𝑥 = 𝑦 → sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) = sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑦)), ℝ*, < ))
6463eleq1d 2828 . . . . . 6 (𝑥 = 𝑦 → (sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ ↔ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑦)), ℝ*, < ) ∈ ℝ))
6564cbvrabv 3347 . . . . 5 {𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ} = {𝑦 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑦)), ℝ*, < ) ∈ ℝ}
6665eleq2i 2835 . . . 4 (𝑋 ∈ {𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ} ↔ 𝑋 ∈ {𝑦 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑦)), ℝ*, < ) ∈ ℝ})
67 fveq2 6374 . . . . . . . . 9 (𝑦 = 𝑋 → ((𝐹𝑚)‘𝑦) = ((𝐹𝑚)‘𝑋))
6867mpteq2dv 4903 . . . . . . . 8 (𝑦 = 𝑋 → (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑦)) = (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋)))
6968rneqd 5520 . . . . . . 7 (𝑦 = 𝑋 → ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑦)) = ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋)))
7069supeq1d 8558 . . . . . 6 (𝑦 = 𝑋 → sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑦)), ℝ*, < ) = sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋)), ℝ*, < ))
7170eleq1d 2828 . . . . 5 (𝑦 = 𝑋 → (sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑦)), ℝ*, < ) ∈ ℝ ↔ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋)), ℝ*, < ) ∈ ℝ))
7271elrab 3518 . . . 4 (𝑋 ∈ {𝑦 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑦)), ℝ*, < ) ∈ ℝ} ↔ (𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∧ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋)), ℝ*, < ) ∈ ℝ))
7366, 72bitri 266 . . 3 (𝑋 ∈ {𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ} ↔ (𝑋 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∧ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑋)), ℝ*, < ) ∈ ℝ))
7459, 73sylibr 225 . 2 (𝜑𝑋 ∈ {𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ})
75 id 22 . . . . 5 (𝜑𝜑)
76 smflimsuplem2.h . . . . . . 7 𝐻 = (𝑛𝑍 ↦ (𝑥 ∈ (𝐸𝑛) ↦ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < )))
7776a1i 11 . . . . . 6 (𝜑𝐻 = (𝑛𝑍 ↦ (𝑥 ∈ (𝐸𝑛) ↦ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ))))
78 smflimsuplem2.e . . . . . . . . . 10 𝐸 = (𝑛𝑍 ↦ {𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ})
79 nfcv 2906 . . . . . . . . . . 11 𝑥𝑍
80 nfrab1 3269 . . . . . . . . . . 11 𝑥{𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ}
8179, 80nfmpt 4904 . . . . . . . . . 10 𝑥(𝑛𝑍 ↦ {𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ})
8278, 81nfcxfr 2904 . . . . . . . . 9 𝑥𝐸
83 nfcv 2906 . . . . . . . . 9 𝑥𝑛
8482, 83nffv 6384 . . . . . . . 8 𝑥(𝐸𝑛)
85 fvex 6387 . . . . . . . 8 (𝐸𝑛) ∈ V
8684, 85mptexf 40018 . . . . . . 7 (𝑥 ∈ (𝐸𝑛) ↦ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < )) ∈ V
8786a1i 11 . . . . . 6 ((𝜑𝑛𝑍) → (𝑥 ∈ (𝐸𝑛) ↦ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < )) ∈ V)
8877, 87fvmpt2d 6481 . . . . 5 ((𝜑𝑛𝑍) → (𝐻𝑛) = (𝑥 ∈ (𝐸𝑛) ↦ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < )))
8975, 4, 88syl2anc 579 . . . 4 (𝜑 → (𝐻𝑛) = (𝑥 ∈ (𝐸𝑛) ↦ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < )))
9089dmeqd 5493 . . 3 (𝜑 → dom (𝐻𝑛) = dom (𝑥 ∈ (𝐸𝑛) ↦ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < )))
91 nfcv 2906 . . . . 5 𝑦(𝐸𝑛)
92 nfcv 2906 . . . . 5 𝑦sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < )
93 nfcv 2906 . . . . 5 𝑥sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑦)), ℝ*, < )
9484, 91, 92, 93, 63cbvmptf 4906 . . . 4 (𝑥 ∈ (𝐸𝑛) ↦ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < )) = (𝑦 ∈ (𝐸𝑛) ↦ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑦)), ℝ*, < ))
95 xrltso 12173 . . . . . 6 < Or ℝ*
9695supex 8575 . . . . 5 sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑦)), ℝ*, < ) ∈ V
9796a1i 11 . . . 4 ((𝜑𝑦 ∈ (𝐸𝑛)) → sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑦)), ℝ*, < ) ∈ V)
9894, 97dmmptd 6201 . . 3 (𝜑 → dom (𝑥 ∈ (𝐸𝑛) ↦ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < )) = (𝐸𝑛))
99 eqid 2764 . . . . 5 {𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ} = {𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ}
100 fvex 6387 . . . . . . . . 9 (𝐹𝑚) ∈ V
101100dmex 7296 . . . . . . . 8 dom (𝐹𝑚) ∈ V
102101rgenw 3070 . . . . . . 7 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∈ V
103102a1i 11 . . . . . 6 (𝜑 → ∀𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∈ V)
10456, 103iinexd 39899 . . . . 5 (𝜑 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∈ V)
10599, 104rabexd 4973 . . . 4 (𝜑 → {𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ} ∈ V)
10678fvmpt2 6479 . . . 4 ((𝑛𝑍 ∧ {𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ} ∈ V) → (𝐸𝑛) = {𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ})
1074, 105, 106syl2anc 579 . . 3 (𝜑 → (𝐸𝑛) = {𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ})
10890, 98, 1073eqtrrd 2803 . 2 (𝜑 → {𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ} = dom (𝐻𝑛))
10974, 108eleqtrd 2845 1 (𝜑𝑋 ∈ dom (𝐻𝑛))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1652  wnf 1878  wcel 2155  wne 2936  wral 3054  wrex 3055  {crab 3058  Vcvv 3349  wss 3731  c0 4078   ciin 4676   class class class wbr 4808  cmpt 4887  dom cdm 5276  ran crn 5277  wf 6063  cfv 6067  supcsup 8552  cr 10187  +∞cpnf 10324  *cxr 10326   < clt 10327  cle 10328  cz 11623  cuz 11885  lim supclsp 14487  SAlgcsalg 41097  SMblFncsmblfn 41481
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-rep 4929  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146  ax-cnex 10244  ax-resscn 10245  ax-1cn 10246  ax-icn 10247  ax-addcl 10248  ax-addrcl 10249  ax-mulcl 10250  ax-mulrcl 10251  ax-mulcom 10252  ax-addass 10253  ax-mulass 10254  ax-distr 10255  ax-i2m1 10256  ax-1ne0 10257  ax-1rid 10258  ax-rnegex 10259  ax-rrecex 10260  ax-cnre 10261  ax-pre-lttri 10262  ax-pre-lttrn 10263  ax-pre-ltadd 10264  ax-pre-mulgt0 10265  ax-pre-sup 10266
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-pss 3747  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-tp 4338  df-op 4340  df-uni 4594  df-int 4633  df-iun 4677  df-iin 4678  df-br 4809  df-opab 4871  df-mpt 4888  df-tr 4911  df-id 5184  df-eprel 5189  df-po 5197  df-so 5198  df-fr 5235  df-we 5237  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-pred 5864  df-ord 5910  df-on 5911  df-lim 5912  df-suc 5913  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-riota 6802  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-om 7263  df-1st 7365  df-2nd 7366  df-wrecs 7609  df-recs 7671  df-rdg 7709  df-1o 7763  df-oadd 7767  df-er 7946  df-pm 8062  df-en 8160  df-dom 8161  df-sdom 8162  df-fin 8163  df-sup 8554  df-inf 8555  df-pnf 10329  df-mnf 10330  df-xr 10331  df-ltxr 10332  df-le 10333  df-sub 10521  df-neg 10522  df-div 10938  df-nn 11274  df-n0 11538  df-z 11624  df-uz 11886  df-q 11989  df-ioo 12380  df-ico 12382  df-fz 12533  df-fl 12800  df-ceil 12801  df-limsup 14488  df-smblfn 41482
This theorem is referenced by:  smflimsuplem7  41604
  Copyright terms: Public domain W3C validator