| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nfcv 2905 | . . 3
⊢
Ⅎ𝑛𝐹 | 
| 2 |  | smfsuplem2.z | . . 3
⊢ 𝑍 =
(ℤ≥‘𝑀) | 
| 3 |  | smfsuplem2.s | . . 3
⊢ (𝜑 → 𝑆 ∈ SAlg) | 
| 4 |  | smfsuplem2.f | . . 3
⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) | 
| 5 |  | eqid 2737 | . . 3
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) | 
| 6 |  | eqid 2737 | . . 3
⊢
(SalGen‘(topGen‘ran (,))) = (SalGen‘(topGen‘ran
(,))) | 
| 7 |  | mnfxr 11318 | . . . . 5
⊢ -∞
∈ ℝ* | 
| 8 | 7 | a1i 11 | . . . 4
⊢ (𝜑 → -∞ ∈
ℝ*) | 
| 9 |  | smfsuplem2.8 | . . . 4
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 10 | 8, 9, 5, 6 | iocborel 46371 | . . 3
⊢ (𝜑 → (-∞(,]𝐴) ∈
(SalGen‘(topGen‘ran (,)))) | 
| 11 | 1, 2, 3, 4, 5, 6, 10 | smfpimcc 46823 | . 2
⊢ (𝜑 → ∃ℎ(ℎ:𝑍⟶𝑆 ∧ ∀𝑛 ∈ 𝑍 (◡(𝐹‘𝑛) “ (-∞(,]𝐴)) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛)))) | 
| 12 |  | smfsuplem2.m | . . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 13 | 12 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (ℎ:𝑍⟶𝑆 ∧ ∀𝑛 ∈ 𝑍 (◡(𝐹‘𝑛) “ (-∞(,]𝐴)) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛)))) → 𝑀 ∈ ℤ) | 
| 14 | 3 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (ℎ:𝑍⟶𝑆 ∧ ∀𝑛 ∈ 𝑍 (◡(𝐹‘𝑛) “ (-∞(,]𝐴)) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛)))) → 𝑆 ∈ SAlg) | 
| 15 | 4 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (ℎ:𝑍⟶𝑆 ∧ ∀𝑛 ∈ 𝑍 (◡(𝐹‘𝑛) “ (-∞(,]𝐴)) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛)))) → 𝐹:𝑍⟶(SMblFn‘𝑆)) | 
| 16 |  | smfsuplem2.d | . . . . . 6
⊢ 𝐷 = {𝑥 ∈ ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦} | 
| 17 |  | fveq2 6906 | . . . . . . . . . 10
⊢ (𝑛 = 𝑚 → (𝐹‘𝑛) = (𝐹‘𝑚)) | 
| 18 | 17 | dmeqd 5916 | . . . . . . . . 9
⊢ (𝑛 = 𝑚 → dom (𝐹‘𝑛) = dom (𝐹‘𝑚)) | 
| 19 | 18 | cbviinv 5041 | . . . . . . . 8
⊢ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) = ∩ 𝑚 ∈ 𝑍 dom (𝐹‘𝑚) | 
| 20 | 19 | a1i 11 | . . . . . . 7
⊢ (𝑥 = 𝑤 → ∩
𝑛 ∈ 𝑍 dom (𝐹‘𝑛) = ∩ 𝑚 ∈ 𝑍 dom (𝐹‘𝑚)) | 
| 21 |  | fveq2 6906 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑤 → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑛)‘𝑤)) | 
| 22 | 21 | breq1d 5153 | . . . . . . . . . 10
⊢ (𝑥 = 𝑤 → (((𝐹‘𝑛)‘𝑥) ≤ 𝑦 ↔ ((𝐹‘𝑛)‘𝑤) ≤ 𝑦)) | 
| 23 | 22 | ralbidv 3178 | . . . . . . . . 9
⊢ (𝑥 = 𝑤 → (∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦 ↔ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑤) ≤ 𝑦)) | 
| 24 | 17 | fveq1d 6908 | . . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → ((𝐹‘𝑛)‘𝑤) = ((𝐹‘𝑚)‘𝑤)) | 
| 25 | 24 | breq1d 5153 | . . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → (((𝐹‘𝑛)‘𝑤) ≤ 𝑦 ↔ ((𝐹‘𝑚)‘𝑤) ≤ 𝑦)) | 
| 26 | 25 | cbvralvw 3237 | . . . . . . . . . 10
⊢
(∀𝑛 ∈
𝑍 ((𝐹‘𝑛)‘𝑤) ≤ 𝑦 ↔ ∀𝑚 ∈ 𝑍 ((𝐹‘𝑚)‘𝑤) ≤ 𝑦) | 
| 27 | 26 | a1i 11 | . . . . . . . . 9
⊢ (𝑥 = 𝑤 → (∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑤) ≤ 𝑦 ↔ ∀𝑚 ∈ 𝑍 ((𝐹‘𝑚)‘𝑤) ≤ 𝑦)) | 
| 28 | 23, 27 | bitrd 279 | . . . . . . . 8
⊢ (𝑥 = 𝑤 → (∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦 ↔ ∀𝑚 ∈ 𝑍 ((𝐹‘𝑚)‘𝑤) ≤ 𝑦)) | 
| 29 | 28 | rexbidv 3179 | . . . . . . 7
⊢ (𝑥 = 𝑤 → (∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑚 ∈ 𝑍 ((𝐹‘𝑚)‘𝑤) ≤ 𝑦)) | 
| 30 | 20, 29 | cbvrabv2w 45133 | . . . . . 6
⊢ {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦} = {𝑤 ∈ ∩
𝑚 ∈ 𝑍 dom (𝐹‘𝑚) ∣ ∃𝑦 ∈ ℝ ∀𝑚 ∈ 𝑍 ((𝐹‘𝑚)‘𝑤) ≤ 𝑦} | 
| 31 | 16, 30 | eqtri 2765 | . . . . 5
⊢ 𝐷 = {𝑤 ∈ ∩
𝑚 ∈ 𝑍 dom (𝐹‘𝑚) ∣ ∃𝑦 ∈ ℝ ∀𝑚 ∈ 𝑍 ((𝐹‘𝑚)‘𝑤) ≤ 𝑦} | 
| 32 |  | smfsuplem2.g | . . . . . 6
⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) | 
| 33 | 21 | mpteq2dv 5244 | . . . . . . . . . 10
⊢ (𝑥 = 𝑤 → (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)) = (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))) | 
| 34 | 24 | cbvmptv 5255 | . . . . . . . . . . 11
⊢ (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤)) = (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑤)) | 
| 35 | 34 | a1i 11 | . . . . . . . . . 10
⊢ (𝑥 = 𝑤 → (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤)) = (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑤))) | 
| 36 | 33, 35 | eqtrd 2777 | . . . . . . . . 9
⊢ (𝑥 = 𝑤 → (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)) = (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑤))) | 
| 37 | 36 | rneqd 5949 | . . . . . . . 8
⊢ (𝑥 = 𝑤 → ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)) = ran (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑤))) | 
| 38 | 37 | supeq1d 9486 | . . . . . . 7
⊢ (𝑥 = 𝑤 → sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) = sup(ran (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑤)), ℝ, < )) | 
| 39 | 38 | cbvmptv 5255 | . . . . . 6
⊢ (𝑥 ∈ 𝐷 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) = (𝑤 ∈ 𝐷 ↦ sup(ran (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑤)), ℝ, < )) | 
| 40 | 32, 39 | eqtri 2765 | . . . . 5
⊢ 𝐺 = (𝑤 ∈ 𝐷 ↦ sup(ran (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑤)), ℝ, < )) | 
| 41 | 9 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (ℎ:𝑍⟶𝑆 ∧ ∀𝑛 ∈ 𝑍 (◡(𝐹‘𝑛) “ (-∞(,]𝐴)) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛)))) → 𝐴 ∈ ℝ) | 
| 42 |  | simprl 771 | . . . . 5
⊢ ((𝜑 ∧ (ℎ:𝑍⟶𝑆 ∧ ∀𝑛 ∈ 𝑍 (◡(𝐹‘𝑛) “ (-∞(,]𝐴)) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛)))) → ℎ:𝑍⟶𝑆) | 
| 43 |  | simplrr 778 | . . . . . 6
⊢ (((𝜑 ∧ (ℎ:𝑍⟶𝑆 ∧ ∀𝑛 ∈ 𝑍 (◡(𝐹‘𝑛) “ (-∞(,]𝐴)) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛)))) ∧ 𝑚 ∈ 𝑍) → ∀𝑛 ∈ 𝑍 (◡(𝐹‘𝑛) “ (-∞(,]𝐴)) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛))) | 
| 44 | 17 | cnveqd 5886 | . . . . . . . . 9
⊢ (𝑛 = 𝑚 → ◡(𝐹‘𝑛) = ◡(𝐹‘𝑚)) | 
| 45 | 44 | imaeq1d 6077 | . . . . . . . 8
⊢ (𝑛 = 𝑚 → (◡(𝐹‘𝑛) “ (-∞(,]𝐴)) = (◡(𝐹‘𝑚) “ (-∞(,]𝐴))) | 
| 46 |  | fveq2 6906 | . . . . . . . . 9
⊢ (𝑛 = 𝑚 → (ℎ‘𝑛) = (ℎ‘𝑚)) | 
| 47 | 46, 18 | ineq12d 4221 | . . . . . . . 8
⊢ (𝑛 = 𝑚 → ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛)) = ((ℎ‘𝑚) ∩ dom (𝐹‘𝑚))) | 
| 48 | 45, 47 | eqeq12d 2753 | . . . . . . 7
⊢ (𝑛 = 𝑚 → ((◡(𝐹‘𝑛) “ (-∞(,]𝐴)) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛)) ↔ (◡(𝐹‘𝑚) “ (-∞(,]𝐴)) = ((ℎ‘𝑚) ∩ dom (𝐹‘𝑚)))) | 
| 49 | 48 | rspccva 3621 | . . . . . 6
⊢
((∀𝑛 ∈
𝑍 (◡(𝐹‘𝑛) “ (-∞(,]𝐴)) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛)) ∧ 𝑚 ∈ 𝑍) → (◡(𝐹‘𝑚) “ (-∞(,]𝐴)) = ((ℎ‘𝑚) ∩ dom (𝐹‘𝑚))) | 
| 50 | 43, 49 | sylancom 588 | . . . . 5
⊢ (((𝜑 ∧ (ℎ:𝑍⟶𝑆 ∧ ∀𝑛 ∈ 𝑍 (◡(𝐹‘𝑛) “ (-∞(,]𝐴)) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛)))) ∧ 𝑚 ∈ 𝑍) → (◡(𝐹‘𝑚) “ (-∞(,]𝐴)) = ((ℎ‘𝑚) ∩ dom (𝐹‘𝑚))) | 
| 51 | 13, 2, 14, 15, 31, 40, 41, 42, 50 | smfsuplem1 46826 | . . . 4
⊢ ((𝜑 ∧ (ℎ:𝑍⟶𝑆 ∧ ∀𝑛 ∈ 𝑍 (◡(𝐹‘𝑛) “ (-∞(,]𝐴)) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛)))) → (◡𝐺 “ (-∞(,]𝐴)) ∈ (𝑆 ↾t 𝐷)) | 
| 52 | 51 | ex 412 | . . 3
⊢ (𝜑 → ((ℎ:𝑍⟶𝑆 ∧ ∀𝑛 ∈ 𝑍 (◡(𝐹‘𝑛) “ (-∞(,]𝐴)) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛))) → (◡𝐺 “ (-∞(,]𝐴)) ∈ (𝑆 ↾t 𝐷))) | 
| 53 | 52 | exlimdv 1933 | . 2
⊢ (𝜑 → (∃ℎ(ℎ:𝑍⟶𝑆 ∧ ∀𝑛 ∈ 𝑍 (◡(𝐹‘𝑛) “ (-∞(,]𝐴)) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛))) → (◡𝐺 “ (-∞(,]𝐴)) ∈ (𝑆 ↾t 𝐷))) | 
| 54 | 11, 53 | mpd 15 | 1
⊢ (𝜑 → (◡𝐺 “ (-∞(,]𝐴)) ∈ (𝑆 ↾t 𝐷)) |