Proof of Theorem smfsuplem1
| Step | Hyp | Ref
| Expression |
| 1 | | smfsuplem1.s |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ∈ SAlg) |
| 2 | 1 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑆 ∈ SAlg) |
| 3 | | smfsuplem1.f |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) |
| 4 | 3 | ffvelcdmda 7104 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ (SMblFn‘𝑆)) |
| 5 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ dom
(𝐹‘𝑛) = dom (𝐹‘𝑛) |
| 6 | 2, 4, 5 | smff 46747 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛):dom (𝐹‘𝑛)⟶ℝ) |
| 7 | 6 | ffnd 6737 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) Fn dom (𝐹‘𝑛)) |
| 8 | 7 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ (◡𝐺 “ (-∞(,]𝐴))) → (𝐹‘𝑛) Fn dom (𝐹‘𝑛)) |
| 9 | | smfsuplem1.d |
. . . . . . . . . . . . 13
⊢ 𝐷 = {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦} |
| 10 | | ssrab2 4080 |
. . . . . . . . . . . . 13
⊢ {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦} ⊆ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) |
| 11 | 9, 10 | eqsstri 4030 |
. . . . . . . . . . . 12
⊢ 𝐷 ⊆ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) |
| 12 | | iinss2 5057 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ 𝑍 → ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ⊆ dom (𝐹‘𝑛)) |
| 13 | 11, 12 | sstrid 3995 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ 𝑍 → 𝐷 ⊆ dom (𝐹‘𝑛)) |
| 14 | 13 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ (◡𝐺 “ (-∞(,]𝐴))) → 𝐷 ⊆ dom (𝐹‘𝑛)) |
| 15 | | cnvimass 6100 |
. . . . . . . . . . . . 13
⊢ (◡𝐺 “ (-∞(,]𝐴)) ⊆ dom 𝐺 |
| 16 | 15 | sseli 3979 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (◡𝐺 “ (-∞(,]𝐴)) → 𝑥 ∈ dom 𝐺) |
| 17 | 16 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ (◡𝐺 “ (-∞(,]𝐴))) → 𝑥 ∈ dom 𝐺) |
| 18 | | nfv 1914 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛(𝜑 ∧ 𝑥 ∈ 𝐷) |
| 19 | | smfsuplem1.m |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 20 | | uzid 12893 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
| 21 | 19, 20 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀)) |
| 22 | | smfsuplem1.z |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 23 | 21, 22 | eleqtrrdi 2852 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑀 ∈ 𝑍) |
| 24 | 23 | ne0d 4342 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑍 ≠ ∅) |
| 25 | 24 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑍 ≠ ∅) |
| 26 | 6 | adantlr 715 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛):dom (𝐹‘𝑛)⟶ℝ) |
| 27 | 12 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑛 ∈ 𝑍) → ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ⊆ dom (𝐹‘𝑛)) |
| 28 | 11 | sseli 3979 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) |
| 29 | 28 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛)) |
| 30 | 27, 29 | sseldd 3984 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ dom (𝐹‘𝑛)) |
| 31 | 30 | adantll 714 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ dom (𝐹‘𝑛)) |
| 32 | 26, 31 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑛)‘𝑥) ∈ ℝ) |
| 33 | 9 | reqabi 3460 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∧ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦)) |
| 34 | 33 | simprbi 496 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝐷 → ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) |
| 35 | 34 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) |
| 36 | 18, 25, 32, 35 | suprclrnmpt 45258 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ∈
ℝ) |
| 37 | | smfsuplem1.g |
. . . . . . . . . . . . . 14
⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) |
| 38 | 36, 37 | fmptd 7134 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺:𝐷⟶ℝ) |
| 39 | 38 | fdmd 6746 |
. . . . . . . . . . . 12
⊢ (𝜑 → dom 𝐺 = 𝐷) |
| 40 | 39 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ (◡𝐺 “ (-∞(,]𝐴))) → dom 𝐺 = 𝐷) |
| 41 | 17, 40 | eleqtrd 2843 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ (◡𝐺 “ (-∞(,]𝐴))) → 𝑥 ∈ 𝐷) |
| 42 | 14, 41 | sseldd 3984 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ (◡𝐺 “ (-∞(,]𝐴))) → 𝑥 ∈ dom (𝐹‘𝑛)) |
| 43 | | mnfxr 11318 |
. . . . . . . . . . 11
⊢ -∞
∈ ℝ* |
| 44 | 43 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ (◡𝐺 “ (-∞(,]𝐴))) → -∞ ∈
ℝ*) |
| 45 | | smfsuplem1.a |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 46 | 45 | rexrd 11311 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
| 47 | 46 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ (◡𝐺 “ (-∞(,]𝐴))) → 𝐴 ∈
ℝ*) |
| 48 | 32 | an32s 652 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ 𝐷) → ((𝐹‘𝑛)‘𝑥) ∈ ℝ) |
| 49 | 41, 48 | syldan 591 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ (◡𝐺 “ (-∞(,]𝐴))) → ((𝐹‘𝑛)‘𝑥) ∈ ℝ) |
| 50 | 49 | rexrd 11311 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ (◡𝐺 “ (-∞(,]𝐴))) → ((𝐹‘𝑛)‘𝑥) ∈
ℝ*) |
| 51 | 49 | mnfltd 13166 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ (◡𝐺 “ (-∞(,]𝐴))) → -∞ < ((𝐹‘𝑛)‘𝑥)) |
| 52 | 16 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (◡𝐺 “ (-∞(,]𝐴))) → 𝑥 ∈ dom 𝐺) |
| 53 | 38 | ffdmd 6766 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺:dom 𝐺⟶ℝ) |
| 54 | 53 | ffvelcdmda 7104 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) ∈ ℝ) |
| 55 | 52, 54 | syldan 591 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (◡𝐺 “ (-∞(,]𝐴))) → (𝐺‘𝑥) ∈ ℝ) |
| 56 | 55 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ (◡𝐺 “ (-∞(,]𝐴))) → (𝐺‘𝑥) ∈ ℝ) |
| 57 | 45 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ (◡𝐺 “ (-∞(,]𝐴))) → 𝐴 ∈ ℝ) |
| 58 | | an32 646 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ 𝐷) ↔ ((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍)) |
| 59 | 58 | biimpi 216 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ 𝐷) → ((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍)) |
| 60 | 18, 32, 35 | suprubrnmpt 45260 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑛)‘𝑥) ≤ sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) |
| 61 | 59, 60 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ 𝐷) → ((𝐹‘𝑛)‘𝑥) ≤ sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) |
| 62 | 37 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐷 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))) |
| 63 | 62, 36 | fvmpt2d 7029 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝐺‘𝑥) = sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) |
| 64 | 63 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ 𝐷) → (𝐺‘𝑥) = sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) |
| 65 | 61, 64 | breqtrrd 5171 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ 𝐷) → ((𝐹‘𝑛)‘𝑥) ≤ (𝐺‘𝑥)) |
| 66 | 41, 65 | syldan 591 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ (◡𝐺 “ (-∞(,]𝐴))) → ((𝐹‘𝑛)‘𝑥) ≤ (𝐺‘𝑥)) |
| 67 | 43 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (◡𝐺 “ (-∞(,]𝐴))) → -∞ ∈
ℝ*) |
| 68 | 46 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (◡𝐺 “ (-∞(,]𝐴))) → 𝐴 ∈
ℝ*) |
| 69 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (◡𝐺 “ (-∞(,]𝐴))) → 𝑥 ∈ (◡𝐺 “ (-∞(,]𝐴))) |
| 70 | 38 | ffnd 6737 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐺 Fn 𝐷) |
| 71 | | elpreima 7078 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 Fn 𝐷 → (𝑥 ∈ (◡𝐺 “ (-∞(,]𝐴)) ↔ (𝑥 ∈ 𝐷 ∧ (𝐺‘𝑥) ∈ (-∞(,]𝐴)))) |
| 72 | 70, 71 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑥 ∈ (◡𝐺 “ (-∞(,]𝐴)) ↔ (𝑥 ∈ 𝐷 ∧ (𝐺‘𝑥) ∈ (-∞(,]𝐴)))) |
| 73 | 72 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (◡𝐺 “ (-∞(,]𝐴))) → (𝑥 ∈ (◡𝐺 “ (-∞(,]𝐴)) ↔ (𝑥 ∈ 𝐷 ∧ (𝐺‘𝑥) ∈ (-∞(,]𝐴)))) |
| 74 | 69, 73 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (◡𝐺 “ (-∞(,]𝐴))) → (𝑥 ∈ 𝐷 ∧ (𝐺‘𝑥) ∈ (-∞(,]𝐴))) |
| 75 | 74 | simprd 495 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (◡𝐺 “ (-∞(,]𝐴))) → (𝐺‘𝑥) ∈ (-∞(,]𝐴)) |
| 76 | 67, 68, 75 | iocleubd 45572 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (◡𝐺 “ (-∞(,]𝐴))) → (𝐺‘𝑥) ≤ 𝐴) |
| 77 | 76 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ (◡𝐺 “ (-∞(,]𝐴))) → (𝐺‘𝑥) ≤ 𝐴) |
| 78 | 49, 56, 57, 66, 77 | letrd 11418 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ (◡𝐺 “ (-∞(,]𝐴))) → ((𝐹‘𝑛)‘𝑥) ≤ 𝐴) |
| 79 | 44, 47, 50, 51, 78 | eliocd 45520 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ (◡𝐺 “ (-∞(,]𝐴))) → ((𝐹‘𝑛)‘𝑥) ∈ (-∞(,]𝐴)) |
| 80 | 8, 42, 79 | elpreimad 7079 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ (◡𝐺 “ (-∞(,]𝐴))) → 𝑥 ∈ (◡(𝐹‘𝑛) “ (-∞(,]𝐴))) |
| 81 | 80 | ssd 45085 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (◡𝐺 “ (-∞(,]𝐴)) ⊆ (◡(𝐹‘𝑛) “ (-∞(,]𝐴))) |
| 82 | | smfsuplem1.i |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (◡(𝐹‘𝑛) “ (-∞(,]𝐴)) = ((𝐻‘𝑛) ∩ dom (𝐹‘𝑛))) |
| 83 | | inss1 4237 |
. . . . . . . 8
⊢ ((𝐻‘𝑛) ∩ dom (𝐹‘𝑛)) ⊆ (𝐻‘𝑛) |
| 84 | 82, 83 | eqsstrdi 4028 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (◡(𝐹‘𝑛) “ (-∞(,]𝐴)) ⊆ (𝐻‘𝑛)) |
| 85 | 81, 84 | sstrd 3994 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (◡𝐺 “ (-∞(,]𝐴)) ⊆ (𝐻‘𝑛)) |
| 86 | 85 | ralrimiva 3146 |
. . . . 5
⊢ (𝜑 → ∀𝑛 ∈ 𝑍 (◡𝐺 “ (-∞(,]𝐴)) ⊆ (𝐻‘𝑛)) |
| 87 | | ssiin 5055 |
. . . . 5
⊢ ((◡𝐺 “ (-∞(,]𝐴)) ⊆ ∩ 𝑛 ∈ 𝑍 (𝐻‘𝑛) ↔ ∀𝑛 ∈ 𝑍 (◡𝐺 “ (-∞(,]𝐴)) ⊆ (𝐻‘𝑛)) |
| 88 | 86, 87 | sylibr 234 |
. . . 4
⊢ (𝜑 → (◡𝐺 “ (-∞(,]𝐴)) ⊆ ∩ 𝑛 ∈ 𝑍 (𝐻‘𝑛)) |
| 89 | 15, 38 | fssdm 6755 |
. . . 4
⊢ (𝜑 → (◡𝐺 “ (-∞(,]𝐴)) ⊆ 𝐷) |
| 90 | 88, 89 | ssind 4241 |
. . 3
⊢ (𝜑 → (◡𝐺 “ (-∞(,]𝐴)) ⊆ (∩ 𝑛 ∈ 𝑍 (𝐻‘𝑛) ∩ 𝐷)) |
| 91 | | iniin1 45130 |
. . . . 5
⊢ (𝑍 ≠ ∅ → (∩ 𝑛 ∈ 𝑍 (𝐻‘𝑛) ∩ 𝐷) = ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛) ∩ 𝐷)) |
| 92 | 24, 91 | syl 17 |
. . . 4
⊢ (𝜑 → (∩ 𝑛 ∈ 𝑍 (𝐻‘𝑛) ∩ 𝐷) = ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛) ∩ 𝐷)) |
| 93 | 70 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛) ∩ 𝐷)) → 𝐺 Fn 𝐷) |
| 94 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛) ∩ 𝐷)) → 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛) ∩ 𝐷)) |
| 95 | 23 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛) ∩ 𝐷)) → 𝑀 ∈ 𝑍) |
| 96 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑀 → (𝐻‘𝑛) = (𝐻‘𝑀)) |
| 97 | 96 | ineq1d 4219 |
. . . . . . . . 9
⊢ (𝑛 = 𝑀 → ((𝐻‘𝑛) ∩ 𝐷) = ((𝐻‘𝑀) ∩ 𝐷)) |
| 98 | 97 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝑛 = 𝑀 → (𝑥 ∈ ((𝐻‘𝑛) ∩ 𝐷) ↔ 𝑥 ∈ ((𝐻‘𝑀) ∩ 𝐷))) |
| 99 | 94, 95, 98 | eliind 45076 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛) ∩ 𝐷)) → 𝑥 ∈ ((𝐻‘𝑀) ∩ 𝐷)) |
| 100 | | elinel2 4202 |
. . . . . . 7
⊢ (𝑥 ∈ ((𝐻‘𝑀) ∩ 𝐷) → 𝑥 ∈ 𝐷) |
| 101 | 99, 100 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛) ∩ 𝐷)) → 𝑥 ∈ 𝐷) |
| 102 | 43 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛) ∩ 𝐷)) → -∞ ∈
ℝ*) |
| 103 | 46 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛) ∩ 𝐷)) → 𝐴 ∈
ℝ*) |
| 104 | 63, 36 | eqeltrd 2841 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝐺‘𝑥) ∈ ℝ) |
| 105 | 104 | rexrd 11311 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝐺‘𝑥) ∈
ℝ*) |
| 106 | 101, 105 | syldan 591 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛) ∩ 𝐷)) → (𝐺‘𝑥) ∈
ℝ*) |
| 107 | 100 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐻‘𝑀) ∩ 𝐷)) → 𝑥 ∈ 𝐷) |
| 108 | 107, 104 | syldan 591 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐻‘𝑀) ∩ 𝐷)) → (𝐺‘𝑥) ∈ ℝ) |
| 109 | 108 | mnfltd 13166 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐻‘𝑀) ∩ 𝐷)) → -∞ < (𝐺‘𝑥)) |
| 110 | 99, 109 | syldan 591 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛) ∩ 𝐷)) → -∞ < (𝐺‘𝑥)) |
| 111 | 101, 63 | syldan 591 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛) ∩ 𝐷)) → (𝐺‘𝑥) = sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) |
| 112 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛𝜑 |
| 113 | | nfcv 2905 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛𝑥 |
| 114 | | nfii1 5029 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛) ∩ 𝐷) |
| 115 | 113, 114 | nfel 2920 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛) ∩ 𝐷) |
| 116 | 112, 115 | nfan 1899 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛) ∩ 𝐷)) |
| 117 | | simpll 767 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛) ∩ 𝐷)) ∧ 𝑛 ∈ 𝑍) → 𝜑) |
| 118 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛) ∩ 𝐷)) ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ 𝑍) |
| 119 | | eliinid 45116 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛) ∩ 𝐷) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ ((𝐻‘𝑛) ∩ 𝐷)) |
| 120 | 119 | adantll 714 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛) ∩ 𝐷)) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ ((𝐻‘𝑛) ∩ 𝐷)) |
| 121 | | elinel1 4201 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ((𝐻‘𝑛) ∩ 𝐷) → 𝑥 ∈ (𝐻‘𝑛)) |
| 122 | 121 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ((𝐻‘𝑛) ∩ 𝐷)) → 𝑥 ∈ (𝐻‘𝑛)) |
| 123 | | elinel2 4202 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ((𝐻‘𝑛) ∩ 𝐷) → 𝑥 ∈ 𝐷) |
| 124 | 123 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ((𝐻‘𝑛) ∩ 𝐷)) → 𝑥 ∈ 𝐷) |
| 125 | 30 | ancoms 458 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ dom (𝐹‘𝑛)) |
| 126 | 124, 125 | syldan 591 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ((𝐻‘𝑛) ∩ 𝐷)) → 𝑥 ∈ dom (𝐹‘𝑛)) |
| 127 | 126 | 3adant1 1131 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ((𝐻‘𝑛) ∩ 𝐷)) → 𝑥 ∈ dom (𝐹‘𝑛)) |
| 128 | 122, 127 | elind 4200 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ((𝐻‘𝑛) ∩ 𝐷)) → 𝑥 ∈ ((𝐻‘𝑛) ∩ dom (𝐹‘𝑛))) |
| 129 | 82 | 3adant3 1133 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ((𝐻‘𝑛) ∩ 𝐷)) → (◡(𝐹‘𝑛) “ (-∞(,]𝐴)) = ((𝐻‘𝑛) ∩ dom (𝐹‘𝑛))) |
| 130 | 128, 129 | eleqtrrd 2844 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ((𝐻‘𝑛) ∩ 𝐷)) → 𝑥 ∈ (◡(𝐹‘𝑛) “ (-∞(,]𝐴))) |
| 131 | 43 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ (◡(𝐹‘𝑛) “ (-∞(,]𝐴))) → -∞ ∈
ℝ*) |
| 132 | 46 | 3ad2ant1 1134 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ (◡(𝐹‘𝑛) “ (-∞(,]𝐴))) → 𝐴 ∈
ℝ*) |
| 133 | | simp3 1139 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ (◡(𝐹‘𝑛) “ (-∞(,]𝐴))) → 𝑥 ∈ (◡(𝐹‘𝑛) “ (-∞(,]𝐴))) |
| 134 | | elpreima 7078 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑛) Fn dom (𝐹‘𝑛) → (𝑥 ∈ (◡(𝐹‘𝑛) “ (-∞(,]𝐴)) ↔ (𝑥 ∈ dom (𝐹‘𝑛) ∧ ((𝐹‘𝑛)‘𝑥) ∈ (-∞(,]𝐴)))) |
| 135 | 7, 134 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ (◡(𝐹‘𝑛) “ (-∞(,]𝐴)) ↔ (𝑥 ∈ dom (𝐹‘𝑛) ∧ ((𝐹‘𝑛)‘𝑥) ∈ (-∞(,]𝐴)))) |
| 136 | 135 | 3adant3 1133 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ (◡(𝐹‘𝑛) “ (-∞(,]𝐴))) → (𝑥 ∈ (◡(𝐹‘𝑛) “ (-∞(,]𝐴)) ↔ (𝑥 ∈ dom (𝐹‘𝑛) ∧ ((𝐹‘𝑛)‘𝑥) ∈ (-∞(,]𝐴)))) |
| 137 | 133, 136 | mpbid 232 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ (◡(𝐹‘𝑛) “ (-∞(,]𝐴))) → (𝑥 ∈ dom (𝐹‘𝑛) ∧ ((𝐹‘𝑛)‘𝑥) ∈ (-∞(,]𝐴))) |
| 138 | 137 | simprd 495 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ (◡(𝐹‘𝑛) “ (-∞(,]𝐴))) → ((𝐹‘𝑛)‘𝑥) ∈ (-∞(,]𝐴)) |
| 139 | 131, 132,
138 | iocleubd 45572 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ (◡(𝐹‘𝑛) “ (-∞(,]𝐴))) → ((𝐹‘𝑛)‘𝑥) ≤ 𝐴) |
| 140 | 130, 139 | syld3an3 1411 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ((𝐻‘𝑛) ∩ 𝐷)) → ((𝐹‘𝑛)‘𝑥) ≤ 𝐴) |
| 141 | 117, 118,
120, 140 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛) ∩ 𝐷)) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑛)‘𝑥) ≤ 𝐴) |
| 142 | 141 | ex 412 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛) ∩ 𝐷)) → (𝑛 ∈ 𝑍 → ((𝐹‘𝑛)‘𝑥) ≤ 𝐴)) |
| 143 | 116, 142 | ralrimi 3257 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛) ∩ 𝐷)) → ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝐴) |
| 144 | 24 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛) ∩ 𝐷)) → 𝑍 ≠ ∅) |
| 145 | 101, 32 | syldanl 602 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛) ∩ 𝐷)) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑛)‘𝑥) ∈ ℝ) |
| 146 | 101, 34 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛) ∩ 𝐷)) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) |
| 147 | 45 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛) ∩ 𝐷)) → 𝐴 ∈ ℝ) |
| 148 | 116, 144,
145, 146, 147 | suprleubrnmpt 45433 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛) ∩ 𝐷)) → (sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ≤ 𝐴 ↔ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝐴)) |
| 149 | 143, 148 | mpbird 257 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛) ∩ 𝐷)) → sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ≤ 𝐴) |
| 150 | 111, 149 | eqbrtrd 5165 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛) ∩ 𝐷)) → (𝐺‘𝑥) ≤ 𝐴) |
| 151 | 102, 103,
106, 110, 150 | eliocd 45520 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛) ∩ 𝐷)) → (𝐺‘𝑥) ∈ (-∞(,]𝐴)) |
| 152 | 93, 101, 151 | elpreimad 7079 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∩
𝑛 ∈ 𝑍 ((𝐻‘𝑛) ∩ 𝐷)) → 𝑥 ∈ (◡𝐺 “ (-∞(,]𝐴))) |
| 153 | 152 | ssd 45085 |
. . . 4
⊢ (𝜑 → ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛) ∩ 𝐷) ⊆ (◡𝐺 “ (-∞(,]𝐴))) |
| 154 | 92, 153 | eqsstrd 4018 |
. . 3
⊢ (𝜑 → (∩ 𝑛 ∈ 𝑍 (𝐻‘𝑛) ∩ 𝐷) ⊆ (◡𝐺 “ (-∞(,]𝐴))) |
| 155 | 90, 154 | eqssd 4001 |
. 2
⊢ (𝜑 → (◡𝐺 “ (-∞(,]𝐴)) = (∩
𝑛 ∈ 𝑍 (𝐻‘𝑛) ∩ 𝐷)) |
| 156 | | eqid 2737 |
. . . . 5
⊢ {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦} = {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦} |
| 157 | | fvex 6919 |
. . . . . . . . 9
⊢ (𝐹‘𝑛) ∈ V |
| 158 | 157 | dmex 7931 |
. . . . . . . 8
⊢ dom
(𝐹‘𝑛) ∈ V |
| 159 | 158 | rgenw 3065 |
. . . . . . 7
⊢
∀𝑛 ∈
𝑍 dom (𝐹‘𝑛) ∈ V |
| 160 | 159 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ∀𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∈ V) |
| 161 | 24, 160 | iinexd 45138 |
. . . . 5
⊢ (𝜑 → ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∈ V) |
| 162 | 156, 161 | rabexd 5340 |
. . . 4
⊢ (𝜑 → {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦} ∈ V) |
| 163 | 9, 162 | eqeltrid 2845 |
. . 3
⊢ (𝜑 → 𝐷 ∈ V) |
| 164 | 22 | uzct 45068 |
. . . . 5
⊢ 𝑍 ≼
ω |
| 165 | 164 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑍 ≼ ω) |
| 166 | | smfsuplem1.h |
. . . . 5
⊢ (𝜑 → 𝐻:𝑍⟶𝑆) |
| 167 | 166 | ffvelcdmda 7104 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐻‘𝑛) ∈ 𝑆) |
| 168 | 1, 165, 24, 167 | saliincl 46342 |
. . 3
⊢ (𝜑 → ∩ 𝑛 ∈ 𝑍 (𝐻‘𝑛) ∈ 𝑆) |
| 169 | | eqid 2737 |
. . 3
⊢ (∩ 𝑛 ∈ 𝑍 (𝐻‘𝑛) ∩ 𝐷) = (∩
𝑛 ∈ 𝑍 (𝐻‘𝑛) ∩ 𝐷) |
| 170 | 1, 163, 168, 169 | elrestd 45113 |
. 2
⊢ (𝜑 → (∩ 𝑛 ∈ 𝑍 (𝐻‘𝑛) ∩ 𝐷) ∈ (𝑆 ↾t 𝐷)) |
| 171 | 155, 170 | eqeltrd 2841 |
1
⊢ (𝜑 → (◡𝐺 “ (-∞(,]𝐴)) ∈ (𝑆 ↾t 𝐷)) |