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

Theorem smfsuplem1 46766
Description: The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
Hypotheses
Ref Expression
smfsuplem1.m (𝜑𝑀 ∈ ℤ)
smfsuplem1.z 𝑍 = (ℤ𝑀)
smfsuplem1.s (𝜑𝑆 ∈ SAlg)
smfsuplem1.f (𝜑𝐹:𝑍⟶(SMblFn‘𝑆))
smfsuplem1.d 𝐷 = {𝑥 𝑛𝑍 dom (𝐹𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛𝑍 ((𝐹𝑛)‘𝑥) ≤ 𝑦}
smfsuplem1.g 𝐺 = (𝑥𝐷 ↦ sup(ran (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑥)), ℝ, < ))
smfsuplem1.a (𝜑𝐴 ∈ ℝ)
smfsuplem1.h (𝜑𝐻:𝑍𝑆)
smfsuplem1.i ((𝜑𝑛𝑍) → ((𝐹𝑛) “ (-∞(,]𝐴)) = ((𝐻𝑛) ∩ dom (𝐹𝑛)))
Assertion
Ref Expression
smfsuplem1 (𝜑 → (𝐺 “ (-∞(,]𝐴)) ∈ (𝑆t 𝐷))
Distinct variable groups:   𝐴,𝑛,𝑥   𝐷,𝑛,𝑥,𝑦   𝑥,𝐹,𝑦   𝑛,𝐺,𝑥   𝑛,𝐻,𝑥,𝑦   𝑛,𝑀   𝑆,𝑛   𝑛,𝑍,𝑥,𝑦   𝜑,𝑛,𝑥,𝑦
Allowed substitution hints:   𝐴(𝑦)   𝑆(𝑥,𝑦)   𝐹(𝑛)   𝐺(𝑦)   𝑀(𝑥,𝑦)

Proof of Theorem smfsuplem1
StepHypRef Expression
1 smfsuplem1.s . . . . . . . . . . . . 13 (𝜑𝑆 ∈ SAlg)
21adantr 480 . . . . . . . . . . . 12 ((𝜑𝑛𝑍) → 𝑆 ∈ SAlg)
3 smfsuplem1.f . . . . . . . . . . . . 13 (𝜑𝐹:𝑍⟶(SMblFn‘𝑆))
43ffvelcdmda 7103 . . . . . . . . . . . 12 ((𝜑𝑛𝑍) → (𝐹𝑛) ∈ (SMblFn‘𝑆))
5 eqid 2734 . . . . . . . . . . . 12 dom (𝐹𝑛) = dom (𝐹𝑛)
62, 4, 5smff 46687 . . . . . . . . . . 11 ((𝜑𝑛𝑍) → (𝐹𝑛):dom (𝐹𝑛)⟶ℝ)
76ffnd 6737 . . . . . . . . . 10 ((𝜑𝑛𝑍) → (𝐹𝑛) Fn dom (𝐹𝑛))
87adantr 480 . . . . . . . . 9 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ (𝐺 “ (-∞(,]𝐴))) → (𝐹𝑛) Fn dom (𝐹𝑛))
9 smfsuplem1.d . . . . . . . . . . . . 13 𝐷 = {𝑥 𝑛𝑍 dom (𝐹𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛𝑍 ((𝐹𝑛)‘𝑥) ≤ 𝑦}
10 ssrab2 4089 . . . . . . . . . . . . 13 {𝑥 𝑛𝑍 dom (𝐹𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛𝑍 ((𝐹𝑛)‘𝑥) ≤ 𝑦} ⊆ 𝑛𝑍 dom (𝐹𝑛)
119, 10eqsstri 4029 . . . . . . . . . . . 12 𝐷 𝑛𝑍 dom (𝐹𝑛)
12 iinss2 5061 . . . . . . . . . . . 12 (𝑛𝑍 𝑛𝑍 dom (𝐹𝑛) ⊆ dom (𝐹𝑛))
1311, 12sstrid 4006 . . . . . . . . . . 11 (𝑛𝑍𝐷 ⊆ dom (𝐹𝑛))
1413ad2antlr 727 . . . . . . . . . 10 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ (𝐺 “ (-∞(,]𝐴))) → 𝐷 ⊆ dom (𝐹𝑛))
15 cnvimass 6101 . . . . . . . . . . . . 13 (𝐺 “ (-∞(,]𝐴)) ⊆ dom 𝐺
1615sseli 3990 . . . . . . . . . . . 12 (𝑥 ∈ (𝐺 “ (-∞(,]𝐴)) → 𝑥 ∈ dom 𝐺)
1716adantl 481 . . . . . . . . . . 11 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ (𝐺 “ (-∞(,]𝐴))) → 𝑥 ∈ dom 𝐺)
18 nfv 1911 . . . . . . . . . . . . . . 15 𝑛(𝜑𝑥𝐷)
19 smfsuplem1.m . . . . . . . . . . . . . . . . . . 19 (𝜑𝑀 ∈ ℤ)
20 uzid 12890 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ𝑀))
2119, 20syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝑀 ∈ (ℤ𝑀))
22 smfsuplem1.z . . . . . . . . . . . . . . . . . 18 𝑍 = (ℤ𝑀)
2321, 22eleqtrrdi 2849 . . . . . . . . . . . . . . . . 17 (𝜑𝑀𝑍)
2423ne0d 4347 . . . . . . . . . . . . . . . 16 (𝜑𝑍 ≠ ∅)
2524adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐷) → 𝑍 ≠ ∅)
266adantlr 715 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐷) ∧ 𝑛𝑍) → (𝐹𝑛):dom (𝐹𝑛)⟶ℝ)
2712adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝑥𝐷𝑛𝑍) → 𝑛𝑍 dom (𝐹𝑛) ⊆ dom (𝐹𝑛))
2811sseli 3990 . . . . . . . . . . . . . . . . . . 19 (𝑥𝐷𝑥 𝑛𝑍 dom (𝐹𝑛))
2928adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝑥𝐷𝑛𝑍) → 𝑥 𝑛𝑍 dom (𝐹𝑛))
3027, 29sseldd 3995 . . . . . . . . . . . . . . . . 17 ((𝑥𝐷𝑛𝑍) → 𝑥 ∈ dom (𝐹𝑛))
3130adantll 714 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐷) ∧ 𝑛𝑍) → 𝑥 ∈ dom (𝐹𝑛))
3226, 31ffvelcdmd 7104 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐷) ∧ 𝑛𝑍) → ((𝐹𝑛)‘𝑥) ∈ ℝ)
339reqabi 3456 . . . . . . . . . . . . . . . . 17 (𝑥𝐷 ↔ (𝑥 𝑛𝑍 dom (𝐹𝑛) ∧ ∃𝑦 ∈ ℝ ∀𝑛𝑍 ((𝐹𝑛)‘𝑥) ≤ 𝑦))
3433simprbi 496 . . . . . . . . . . . . . . . 16 (𝑥𝐷 → ∃𝑦 ∈ ℝ ∀𝑛𝑍 ((𝐹𝑛)‘𝑥) ≤ 𝑦)
3534adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐷) → ∃𝑦 ∈ ℝ ∀𝑛𝑍 ((𝐹𝑛)‘𝑥) ≤ 𝑦)
3618, 25, 32, 35suprclrnmpt 45195 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐷) → sup(ran (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑥)), ℝ, < ) ∈ ℝ)
37 smfsuplem1.g . . . . . . . . . . . . . 14 𝐺 = (𝑥𝐷 ↦ sup(ran (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑥)), ℝ, < ))
3836, 37fmptd 7133 . . . . . . . . . . . . 13 (𝜑𝐺:𝐷⟶ℝ)
3938fdmd 6746 . . . . . . . . . . . 12 (𝜑 → dom 𝐺 = 𝐷)
4039ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ (𝐺 “ (-∞(,]𝐴))) → dom 𝐺 = 𝐷)
4117, 40eleqtrd 2840 . . . . . . . . . 10 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ (𝐺 “ (-∞(,]𝐴))) → 𝑥𝐷)
4214, 41sseldd 3995 . . . . . . . . 9 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ (𝐺 “ (-∞(,]𝐴))) → 𝑥 ∈ dom (𝐹𝑛))
43 mnfxr 11315 . . . . . . . . . . 11 -∞ ∈ ℝ*
4443a1i 11 . . . . . . . . . 10 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ (𝐺 “ (-∞(,]𝐴))) → -∞ ∈ ℝ*)
45 smfsuplem1.a . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℝ)
4645rexrd 11308 . . . . . . . . . . 11 (𝜑𝐴 ∈ ℝ*)
4746ad2antrr 726 . . . . . . . . . 10 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ (𝐺 “ (-∞(,]𝐴))) → 𝐴 ∈ ℝ*)
4832an32s 652 . . . . . . . . . . . 12 (((𝜑𝑛𝑍) ∧ 𝑥𝐷) → ((𝐹𝑛)‘𝑥) ∈ ℝ)
4941, 48syldan 591 . . . . . . . . . . 11 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ (𝐺 “ (-∞(,]𝐴))) → ((𝐹𝑛)‘𝑥) ∈ ℝ)
5049rexrd 11308 . . . . . . . . . 10 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ (𝐺 “ (-∞(,]𝐴))) → ((𝐹𝑛)‘𝑥) ∈ ℝ*)
5149mnfltd 13163 . . . . . . . . . 10 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ (𝐺 “ (-∞(,]𝐴))) → -∞ < ((𝐹𝑛)‘𝑥))
5216adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐺 “ (-∞(,]𝐴))) → 𝑥 ∈ dom 𝐺)
5338ffdmd 6766 . . . . . . . . . . . . . 14 (𝜑𝐺:dom 𝐺⟶ℝ)
5453ffvelcdmda 7103 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ dom 𝐺) → (𝐺𝑥) ∈ ℝ)
5552, 54syldan 591 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐺 “ (-∞(,]𝐴))) → (𝐺𝑥) ∈ ℝ)
5655adantlr 715 . . . . . . . . . . 11 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ (𝐺 “ (-∞(,]𝐴))) → (𝐺𝑥) ∈ ℝ)
5745ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ (𝐺 “ (-∞(,]𝐴))) → 𝐴 ∈ ℝ)
58 an32 646 . . . . . . . . . . . . . . 15 (((𝜑𝑛𝑍) ∧ 𝑥𝐷) ↔ ((𝜑𝑥𝐷) ∧ 𝑛𝑍))
5958biimpi 216 . . . . . . . . . . . . . 14 (((𝜑𝑛𝑍) ∧ 𝑥𝐷) → ((𝜑𝑥𝐷) ∧ 𝑛𝑍))
6018, 32, 35suprubrnmpt 45197 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐷) ∧ 𝑛𝑍) → ((𝐹𝑛)‘𝑥) ≤ sup(ran (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑥)), ℝ, < ))
6159, 60syl 17 . . . . . . . . . . . . 13 (((𝜑𝑛𝑍) ∧ 𝑥𝐷) → ((𝐹𝑛)‘𝑥) ≤ sup(ran (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑥)), ℝ, < ))
6237a1i 11 . . . . . . . . . . . . . . 15 (𝜑𝐺 = (𝑥𝐷 ↦ sup(ran (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑥)), ℝ, < )))
6362, 36fvmpt2d 7028 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐷) → (𝐺𝑥) = sup(ran (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑥)), ℝ, < ))
6463adantlr 715 . . . . . . . . . . . . 13 (((𝜑𝑛𝑍) ∧ 𝑥𝐷) → (𝐺𝑥) = sup(ran (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑥)), ℝ, < ))
6561, 64breqtrrd 5175 . . . . . . . . . . . 12 (((𝜑𝑛𝑍) ∧ 𝑥𝐷) → ((𝐹𝑛)‘𝑥) ≤ (𝐺𝑥))
6641, 65syldan 591 . . . . . . . . . . 11 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ (𝐺 “ (-∞(,]𝐴))) → ((𝐹𝑛)‘𝑥) ≤ (𝐺𝑥))
6743a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐺 “ (-∞(,]𝐴))) → -∞ ∈ ℝ*)
6846adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐺 “ (-∞(,]𝐴))) → 𝐴 ∈ ℝ*)
69 simpr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐺 “ (-∞(,]𝐴))) → 𝑥 ∈ (𝐺 “ (-∞(,]𝐴)))
7038ffnd 6737 . . . . . . . . . . . . . . . . 17 (𝜑𝐺 Fn 𝐷)
71 elpreima 7077 . . . . . . . . . . . . . . . . 17 (𝐺 Fn 𝐷 → (𝑥 ∈ (𝐺 “ (-∞(,]𝐴)) ↔ (𝑥𝐷 ∧ (𝐺𝑥) ∈ (-∞(,]𝐴))))
7270, 71syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑥 ∈ (𝐺 “ (-∞(,]𝐴)) ↔ (𝑥𝐷 ∧ (𝐺𝑥) ∈ (-∞(,]𝐴))))
7372adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐺 “ (-∞(,]𝐴))) → (𝑥 ∈ (𝐺 “ (-∞(,]𝐴)) ↔ (𝑥𝐷 ∧ (𝐺𝑥) ∈ (-∞(,]𝐴))))
7469, 73mpbid 232 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐺 “ (-∞(,]𝐴))) → (𝑥𝐷 ∧ (𝐺𝑥) ∈ (-∞(,]𝐴)))
7574simprd 495 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐺 “ (-∞(,]𝐴))) → (𝐺𝑥) ∈ (-∞(,]𝐴))
7667, 68, 75iocleubd 45511 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐺 “ (-∞(,]𝐴))) → (𝐺𝑥) ≤ 𝐴)
7776adantlr 715 . . . . . . . . . . 11 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ (𝐺 “ (-∞(,]𝐴))) → (𝐺𝑥) ≤ 𝐴)
7849, 56, 57, 66, 77letrd 11415 . . . . . . . . . 10 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ (𝐺 “ (-∞(,]𝐴))) → ((𝐹𝑛)‘𝑥) ≤ 𝐴)
7944, 47, 50, 51, 78eliocd 45459 . . . . . . . . 9 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ (𝐺 “ (-∞(,]𝐴))) → ((𝐹𝑛)‘𝑥) ∈ (-∞(,]𝐴))
808, 42, 79elpreimad 7078 . . . . . . . 8 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ (𝐺 “ (-∞(,]𝐴))) → 𝑥 ∈ ((𝐹𝑛) “ (-∞(,]𝐴)))
8180ssd 45019 . . . . . . 7 ((𝜑𝑛𝑍) → (𝐺 “ (-∞(,]𝐴)) ⊆ ((𝐹𝑛) “ (-∞(,]𝐴)))
82 smfsuplem1.i . . . . . . . 8 ((𝜑𝑛𝑍) → ((𝐹𝑛) “ (-∞(,]𝐴)) = ((𝐻𝑛) ∩ dom (𝐹𝑛)))
83 inss1 4244 . . . . . . . 8 ((𝐻𝑛) ∩ dom (𝐹𝑛)) ⊆ (𝐻𝑛)
8482, 83eqsstrdi 4049 . . . . . . 7 ((𝜑𝑛𝑍) → ((𝐹𝑛) “ (-∞(,]𝐴)) ⊆ (𝐻𝑛))
8581, 84sstrd 4005 . . . . . 6 ((𝜑𝑛𝑍) → (𝐺 “ (-∞(,]𝐴)) ⊆ (𝐻𝑛))
8685ralrimiva 3143 . . . . 5 (𝜑 → ∀𝑛𝑍 (𝐺 “ (-∞(,]𝐴)) ⊆ (𝐻𝑛))
87 ssiin 5059 . . . . 5 ((𝐺 “ (-∞(,]𝐴)) ⊆ 𝑛𝑍 (𝐻𝑛) ↔ ∀𝑛𝑍 (𝐺 “ (-∞(,]𝐴)) ⊆ (𝐻𝑛))
8886, 87sylibr 234 . . . 4 (𝜑 → (𝐺 “ (-∞(,]𝐴)) ⊆ 𝑛𝑍 (𝐻𝑛))
8915, 38fssdm 6755 . . . 4 (𝜑 → (𝐺 “ (-∞(,]𝐴)) ⊆ 𝐷)
9088, 89ssind 4248 . . 3 (𝜑 → (𝐺 “ (-∞(,]𝐴)) ⊆ ( 𝑛𝑍 (𝐻𝑛) ∩ 𝐷))
91 iniin1 45064 . . . . 5 (𝑍 ≠ ∅ → ( 𝑛𝑍 (𝐻𝑛) ∩ 𝐷) = 𝑛𝑍 ((𝐻𝑛) ∩ 𝐷))
9224, 91syl 17 . . . 4 (𝜑 → ( 𝑛𝑍 (𝐻𝑛) ∩ 𝐷) = 𝑛𝑍 ((𝐻𝑛) ∩ 𝐷))
9370adantr 480 . . . . . 6 ((𝜑𝑥 𝑛𝑍 ((𝐻𝑛) ∩ 𝐷)) → 𝐺 Fn 𝐷)
94 simpr 484 . . . . . . . 8 ((𝜑𝑥 𝑛𝑍 ((𝐻𝑛) ∩ 𝐷)) → 𝑥 𝑛𝑍 ((𝐻𝑛) ∩ 𝐷))
9523adantr 480 . . . . . . . 8 ((𝜑𝑥 𝑛𝑍 ((𝐻𝑛) ∩ 𝐷)) → 𝑀𝑍)
96 fveq2 6906 . . . . . . . . . 10 (𝑛 = 𝑀 → (𝐻𝑛) = (𝐻𝑀))
9796ineq1d 4226 . . . . . . . . 9 (𝑛 = 𝑀 → ((𝐻𝑛) ∩ 𝐷) = ((𝐻𝑀) ∩ 𝐷))
9897eleq2d 2824 . . . . . . . 8 (𝑛 = 𝑀 → (𝑥 ∈ ((𝐻𝑛) ∩ 𝐷) ↔ 𝑥 ∈ ((𝐻𝑀) ∩ 𝐷)))
9994, 95, 98eliind 45010 . . . . . . 7 ((𝜑𝑥 𝑛𝑍 ((𝐻𝑛) ∩ 𝐷)) → 𝑥 ∈ ((𝐻𝑀) ∩ 𝐷))
100 elinel2 4211 . . . . . . 7 (𝑥 ∈ ((𝐻𝑀) ∩ 𝐷) → 𝑥𝐷)
10199, 100syl 17 . . . . . 6 ((𝜑𝑥 𝑛𝑍 ((𝐻𝑛) ∩ 𝐷)) → 𝑥𝐷)
10243a1i 11 . . . . . . 7 ((𝜑𝑥 𝑛𝑍 ((𝐻𝑛) ∩ 𝐷)) → -∞ ∈ ℝ*)
10346adantr 480 . . . . . . 7 ((𝜑𝑥 𝑛𝑍 ((𝐻𝑛) ∩ 𝐷)) → 𝐴 ∈ ℝ*)
10463, 36eqeltrd 2838 . . . . . . . . 9 ((𝜑𝑥𝐷) → (𝐺𝑥) ∈ ℝ)
105104rexrd 11308 . . . . . . . 8 ((𝜑𝑥𝐷) → (𝐺𝑥) ∈ ℝ*)
106101, 105syldan 591 . . . . . . 7 ((𝜑𝑥 𝑛𝑍 ((𝐻𝑛) ∩ 𝐷)) → (𝐺𝑥) ∈ ℝ*)
107100adantl 481 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐻𝑀) ∩ 𝐷)) → 𝑥𝐷)
108107, 104syldan 591 . . . . . . . . 9 ((𝜑𝑥 ∈ ((𝐻𝑀) ∩ 𝐷)) → (𝐺𝑥) ∈ ℝ)
109108mnfltd 13163 . . . . . . . 8 ((𝜑𝑥 ∈ ((𝐻𝑀) ∩ 𝐷)) → -∞ < (𝐺𝑥))
11099, 109syldan 591 . . . . . . 7 ((𝜑𝑥 𝑛𝑍 ((𝐻𝑛) ∩ 𝐷)) → -∞ < (𝐺𝑥))
111101, 63syldan 591 . . . . . . . 8 ((𝜑𝑥 𝑛𝑍 ((𝐻𝑛) ∩ 𝐷)) → (𝐺𝑥) = sup(ran (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑥)), ℝ, < ))
112 nfv 1911 . . . . . . . . . . 11 𝑛𝜑
113 nfcv 2902 . . . . . . . . . . . 12 𝑛𝑥
114 nfii1 5033 . . . . . . . . . . . 12 𝑛 𝑛𝑍 ((𝐻𝑛) ∩ 𝐷)
115113, 114nfel 2917 . . . . . . . . . . 11 𝑛 𝑥 𝑛𝑍 ((𝐻𝑛) ∩ 𝐷)
116112, 115nfan 1896 . . . . . . . . . 10 𝑛(𝜑𝑥 𝑛𝑍 ((𝐻𝑛) ∩ 𝐷))
117 simpll 767 . . . . . . . . . . . 12 (((𝜑𝑥 𝑛𝑍 ((𝐻𝑛) ∩ 𝐷)) ∧ 𝑛𝑍) → 𝜑)
118 simpr 484 . . . . . . . . . . . 12 (((𝜑𝑥 𝑛𝑍 ((𝐻𝑛) ∩ 𝐷)) ∧ 𝑛𝑍) → 𝑛𝑍)
119 eliinid 45050 . . . . . . . . . . . . 13 ((𝑥 𝑛𝑍 ((𝐻𝑛) ∩ 𝐷) ∧ 𝑛𝑍) → 𝑥 ∈ ((𝐻𝑛) ∩ 𝐷))
120119adantll 714 . . . . . . . . . . . 12 (((𝜑𝑥 𝑛𝑍 ((𝐻𝑛) ∩ 𝐷)) ∧ 𝑛𝑍) → 𝑥 ∈ ((𝐻𝑛) ∩ 𝐷))
121 elinel1 4210 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((𝐻𝑛) ∩ 𝐷) → 𝑥 ∈ (𝐻𝑛))
1221213ad2ant3 1134 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝑍𝑥 ∈ ((𝐻𝑛) ∩ 𝐷)) → 𝑥 ∈ (𝐻𝑛))
123 elinel2 4211 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((𝐻𝑛) ∩ 𝐷) → 𝑥𝐷)
124123adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑛𝑍𝑥 ∈ ((𝐻𝑛) ∩ 𝐷)) → 𝑥𝐷)
12530ancoms 458 . . . . . . . . . . . . . . . . 17 ((𝑛𝑍𝑥𝐷) → 𝑥 ∈ dom (𝐹𝑛))
126124, 125syldan 591 . . . . . . . . . . . . . . . 16 ((𝑛𝑍𝑥 ∈ ((𝐻𝑛) ∩ 𝐷)) → 𝑥 ∈ dom (𝐹𝑛))
1271263adant1 1129 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝑍𝑥 ∈ ((𝐻𝑛) ∩ 𝐷)) → 𝑥 ∈ dom (𝐹𝑛))
128122, 127elind 4209 . . . . . . . . . . . . . 14 ((𝜑𝑛𝑍𝑥 ∈ ((𝐻𝑛) ∩ 𝐷)) → 𝑥 ∈ ((𝐻𝑛) ∩ dom (𝐹𝑛)))
129823adant3 1131 . . . . . . . . . . . . . 14 ((𝜑𝑛𝑍𝑥 ∈ ((𝐻𝑛) ∩ 𝐷)) → ((𝐹𝑛) “ (-∞(,]𝐴)) = ((𝐻𝑛) ∩ dom (𝐹𝑛)))
130128, 129eleqtrrd 2841 . . . . . . . . . . . . 13 ((𝜑𝑛𝑍𝑥 ∈ ((𝐻𝑛) ∩ 𝐷)) → 𝑥 ∈ ((𝐹𝑛) “ (-∞(,]𝐴)))
13143a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑛𝑍𝑥 ∈ ((𝐹𝑛) “ (-∞(,]𝐴))) → -∞ ∈ ℝ*)
132463ad2ant1 1132 . . . . . . . . . . . . . 14 ((𝜑𝑛𝑍𝑥 ∈ ((𝐹𝑛) “ (-∞(,]𝐴))) → 𝐴 ∈ ℝ*)
133 simp3 1137 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝑍𝑥 ∈ ((𝐹𝑛) “ (-∞(,]𝐴))) → 𝑥 ∈ ((𝐹𝑛) “ (-∞(,]𝐴)))
134 elpreima 7077 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑛) Fn dom (𝐹𝑛) → (𝑥 ∈ ((𝐹𝑛) “ (-∞(,]𝐴)) ↔ (𝑥 ∈ dom (𝐹𝑛) ∧ ((𝐹𝑛)‘𝑥) ∈ (-∞(,]𝐴))))
1357, 134syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝑍) → (𝑥 ∈ ((𝐹𝑛) “ (-∞(,]𝐴)) ↔ (𝑥 ∈ dom (𝐹𝑛) ∧ ((𝐹𝑛)‘𝑥) ∈ (-∞(,]𝐴))))
1361353adant3 1131 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝑍𝑥 ∈ ((𝐹𝑛) “ (-∞(,]𝐴))) → (𝑥 ∈ ((𝐹𝑛) “ (-∞(,]𝐴)) ↔ (𝑥 ∈ dom (𝐹𝑛) ∧ ((𝐹𝑛)‘𝑥) ∈ (-∞(,]𝐴))))
137133, 136mpbid 232 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝑍𝑥 ∈ ((𝐹𝑛) “ (-∞(,]𝐴))) → (𝑥 ∈ dom (𝐹𝑛) ∧ ((𝐹𝑛)‘𝑥) ∈ (-∞(,]𝐴)))
138137simprd 495 . . . . . . . . . . . . . 14 ((𝜑𝑛𝑍𝑥 ∈ ((𝐹𝑛) “ (-∞(,]𝐴))) → ((𝐹𝑛)‘𝑥) ∈ (-∞(,]𝐴))
139131, 132, 138iocleubd 45511 . . . . . . . . . . . . 13 ((𝜑𝑛𝑍𝑥 ∈ ((𝐹𝑛) “ (-∞(,]𝐴))) → ((𝐹𝑛)‘𝑥) ≤ 𝐴)
140130, 139syld3an3 1408 . . . . . . . . . . . 12 ((𝜑𝑛𝑍𝑥 ∈ ((𝐻𝑛) ∩ 𝐷)) → ((𝐹𝑛)‘𝑥) ≤ 𝐴)
141117, 118, 120, 140syl3anc 1370 . . . . . . . . . . 11 (((𝜑𝑥 𝑛𝑍 ((𝐻𝑛) ∩ 𝐷)) ∧ 𝑛𝑍) → ((𝐹𝑛)‘𝑥) ≤ 𝐴)
142141ex 412 . . . . . . . . . 10 ((𝜑𝑥 𝑛𝑍 ((𝐻𝑛) ∩ 𝐷)) → (𝑛𝑍 → ((𝐹𝑛)‘𝑥) ≤ 𝐴))
143116, 142ralrimi 3254 . . . . . . . . 9 ((𝜑𝑥 𝑛𝑍 ((𝐻𝑛) ∩ 𝐷)) → ∀𝑛𝑍 ((𝐹𝑛)‘𝑥) ≤ 𝐴)
14424adantr 480 . . . . . . . . . 10 ((𝜑𝑥 𝑛𝑍 ((𝐻𝑛) ∩ 𝐷)) → 𝑍 ≠ ∅)
145101, 32syldanl 602 . . . . . . . . . 10 (((𝜑𝑥 𝑛𝑍 ((𝐻𝑛) ∩ 𝐷)) ∧ 𝑛𝑍) → ((𝐹𝑛)‘𝑥) ∈ ℝ)
146101, 34syl 17 . . . . . . . . . 10 ((𝜑𝑥 𝑛𝑍 ((𝐻𝑛) ∩ 𝐷)) → ∃𝑦 ∈ ℝ ∀𝑛𝑍 ((𝐹𝑛)‘𝑥) ≤ 𝑦)
14745adantr 480 . . . . . . . . . 10 ((𝜑𝑥 𝑛𝑍 ((𝐻𝑛) ∩ 𝐷)) → 𝐴 ∈ ℝ)
148116, 144, 145, 146, 147suprleubrnmpt 45371 . . . . . . . . 9 ((𝜑𝑥 𝑛𝑍 ((𝐻𝑛) ∩ 𝐷)) → (sup(ran (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑥)), ℝ, < ) ≤ 𝐴 ↔ ∀𝑛𝑍 ((𝐹𝑛)‘𝑥) ≤ 𝐴))
149143, 148mpbird 257 . . . . . . . 8 ((𝜑𝑥 𝑛𝑍 ((𝐻𝑛) ∩ 𝐷)) → sup(ran (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑥)), ℝ, < ) ≤ 𝐴)
150111, 149eqbrtrd 5169 . . . . . . 7 ((𝜑𝑥 𝑛𝑍 ((𝐻𝑛) ∩ 𝐷)) → (𝐺𝑥) ≤ 𝐴)
151102, 103, 106, 110, 150eliocd 45459 . . . . . 6 ((𝜑𝑥 𝑛𝑍 ((𝐻𝑛) ∩ 𝐷)) → (𝐺𝑥) ∈ (-∞(,]𝐴))
15293, 101, 151elpreimad 7078 . . . . 5 ((𝜑𝑥 𝑛𝑍 ((𝐻𝑛) ∩ 𝐷)) → 𝑥 ∈ (𝐺 “ (-∞(,]𝐴)))
153152ssd 45019 . . . 4 (𝜑 𝑛𝑍 ((𝐻𝑛) ∩ 𝐷) ⊆ (𝐺 “ (-∞(,]𝐴)))
15492, 153eqsstrd 4033 . . 3 (𝜑 → ( 𝑛𝑍 (𝐻𝑛) ∩ 𝐷) ⊆ (𝐺 “ (-∞(,]𝐴)))
15590, 154eqssd 4012 . 2 (𝜑 → (𝐺 “ (-∞(,]𝐴)) = ( 𝑛𝑍 (𝐻𝑛) ∩ 𝐷))
156 eqid 2734 . . . . 5 {𝑥 𝑛𝑍 dom (𝐹𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛𝑍 ((𝐹𝑛)‘𝑥) ≤ 𝑦} = {𝑥 𝑛𝑍 dom (𝐹𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛𝑍 ((𝐹𝑛)‘𝑥) ≤ 𝑦}
157 fvex 6919 . . . . . . . . 9 (𝐹𝑛) ∈ V
158157dmex 7931 . . . . . . . 8 dom (𝐹𝑛) ∈ V
159158rgenw 3062 . . . . . . 7 𝑛𝑍 dom (𝐹𝑛) ∈ V
160159a1i 11 . . . . . 6 (𝜑 → ∀𝑛𝑍 dom (𝐹𝑛) ∈ V)
16124, 160iinexd 45072 . . . . 5 (𝜑 𝑛𝑍 dom (𝐹𝑛) ∈ V)
162156, 161rabexd 5345 . . . 4 (𝜑 → {𝑥 𝑛𝑍 dom (𝐹𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛𝑍 ((𝐹𝑛)‘𝑥) ≤ 𝑦} ∈ V)
1639, 162eqeltrid 2842 . . 3 (𝜑𝐷 ∈ V)
16422uzct 45002 . . . . 5 𝑍 ≼ ω
165164a1i 11 . . . 4 (𝜑𝑍 ≼ ω)
166 smfsuplem1.h . . . . 5 (𝜑𝐻:𝑍𝑆)
167166ffvelcdmda 7103 . . . 4 ((𝜑𝑛𝑍) → (𝐻𝑛) ∈ 𝑆)
1681, 165, 24, 167saliincl 46282 . . 3 (𝜑 𝑛𝑍 (𝐻𝑛) ∈ 𝑆)
169 eqid 2734 . . 3 ( 𝑛𝑍 (𝐻𝑛) ∩ 𝐷) = ( 𝑛𝑍 (𝐻𝑛) ∩ 𝐷)
1701, 163, 168, 169elrestd 45047 . 2 (𝜑 → ( 𝑛𝑍 (𝐻𝑛) ∩ 𝐷) ∈ (𝑆t 𝐷))
171155, 170eqeltrd 2838 1 (𝜑 → (𝐺 “ (-∞(,]𝐴)) ∈ (𝑆t 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086   = wceq 1536  wcel 2105  wne 2937  wral 3058  wrex 3067  {crab 3432  Vcvv 3477  cin 3961  wss 3962  c0 4338   ciin 4996   class class class wbr 5147  cmpt 5230  ccnv 5687  dom cdm 5688  ran crn 5689  cima 5691   Fn wfn 6557  wf 6558  cfv 6562  (class class class)co 7430  ωcom 7886  cdom 8981  supcsup 9477  cr 11151  -∞cmnf 11290  *cxr 11291   < clt 11292  cle 11293  cz 12610  cuz 12875  (,]cioc 13384  t crest 17466  SAlgcsalg 46263  SMblFncsmblfn 46650
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-iin 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-oadd 8508  df-omul 8509  df-er 8743  df-map 8866  df-pm 8867  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-sup 9479  df-oi 9547  df-card 9976  df-acn 9979  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-nn 12264  df-n0 12524  df-z 12611  df-uz 12876  df-ioo 13387  df-ioc 13388  df-ico 13389  df-rest 17468  df-salg 46264  df-smblfn 46651
This theorem is referenced by:  smfsuplem2  46767
  Copyright terms: Public domain W3C validator