| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nfv 1914 | . 2
⊢
Ⅎ𝑎𝜑 | 
| 2 |  | decsmf.j | . . . . 5
⊢ 𝐽 = (topGen‘ran
(,)) | 
| 3 |  | retop 24782 | . . . . 5
⊢
(topGen‘ran (,)) ∈ Top | 
| 4 | 2, 3 | eqeltri 2837 | . . . 4
⊢ 𝐽 ∈ Top | 
| 5 | 4 | a1i 11 | . . 3
⊢ (𝜑 → 𝐽 ∈ Top) | 
| 6 |  | decsmf.b | . . 3
⊢ 𝐵 = (SalGen‘𝐽) | 
| 7 | 5, 6 | salgencld 46364 | . 2
⊢ (𝜑 → 𝐵 ∈ SAlg) | 
| 8 |  | decsmf.a | . . 3
⊢ (𝜑 → 𝐴 ⊆ ℝ) | 
| 9 | 5, 6 | unisalgen2 46369 | . . . 4
⊢ (𝜑 → ∪ 𝐵 =
∪ 𝐽) | 
| 10 | 2 | unieqi 4919 | . . . . 5
⊢ ∪ 𝐽 =
∪ (topGen‘ran (,)) | 
| 11 | 10 | a1i 11 | . . . 4
⊢ (𝜑 → ∪ 𝐽 =
∪ (topGen‘ran (,))) | 
| 12 |  | uniretop 24783 | . . . . . 6
⊢ ℝ =
∪ (topGen‘ran (,)) | 
| 13 | 12 | eqcomi 2746 | . . . . 5
⊢ ∪ (topGen‘ran (,)) = ℝ | 
| 14 | 13 | a1i 11 | . . . 4
⊢ (𝜑 → ∪ (topGen‘ran (,)) = ℝ) | 
| 15 | 9, 11, 14 | 3eqtrrd 2782 | . . 3
⊢ (𝜑 → ℝ = ∪ 𝐵) | 
| 16 | 8, 15 | sseqtrd 4020 | . 2
⊢ (𝜑 → 𝐴 ⊆ ∪ 𝐵) | 
| 17 |  | decsmf.f | . 2
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) | 
| 18 |  | decsmf.x | . . . . 5
⊢
Ⅎ𝑥𝜑 | 
| 19 |  | nfv 1914 | . . . . 5
⊢
Ⅎ𝑥 𝑎 ∈ ℝ | 
| 20 | 18, 19 | nfan 1899 | . . . 4
⊢
Ⅎ𝑥(𝜑 ∧ 𝑎 ∈ ℝ) | 
| 21 |  | decsmf.y | . . . . 5
⊢
Ⅎ𝑦𝜑 | 
| 22 |  | nfv 1914 | . . . . 5
⊢
Ⅎ𝑦 𝑎 ∈ ℝ | 
| 23 | 21, 22 | nfan 1899 | . . . 4
⊢
Ⅎ𝑦(𝜑 ∧ 𝑎 ∈ ℝ) | 
| 24 | 8 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝐴 ⊆ ℝ) | 
| 25 | 17 | frexr 45396 | . . . . 5
⊢ (𝜑 → 𝐹:𝐴⟶ℝ*) | 
| 26 | 25 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝐹:𝐴⟶ℝ*) | 
| 27 |  | decsmf.i | . . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥))) | 
| 28 |  | breq1 5146 | . . . . . . . . 9
⊢ (𝑥 = 𝑤 → (𝑥 ≤ 𝑦 ↔ 𝑤 ≤ 𝑦)) | 
| 29 |  | fveq2 6906 | . . . . . . . . . 10
⊢ (𝑥 = 𝑤 → (𝐹‘𝑥) = (𝐹‘𝑤)) | 
| 30 | 29 | breq2d 5155 | . . . . . . . . 9
⊢ (𝑥 = 𝑤 → ((𝐹‘𝑦) ≤ (𝐹‘𝑥) ↔ (𝐹‘𝑦) ≤ (𝐹‘𝑤))) | 
| 31 | 28, 30 | imbi12d 344 | . . . . . . . 8
⊢ (𝑥 = 𝑤 → ((𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥)) ↔ (𝑤 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑤)))) | 
| 32 |  | breq2 5147 | . . . . . . . . 9
⊢ (𝑦 = 𝑧 → (𝑤 ≤ 𝑦 ↔ 𝑤 ≤ 𝑧)) | 
| 33 |  | fveq2 6906 | . . . . . . . . . 10
⊢ (𝑦 = 𝑧 → (𝐹‘𝑦) = (𝐹‘𝑧)) | 
| 34 | 33 | breq1d 5153 | . . . . . . . . 9
⊢ (𝑦 = 𝑧 → ((𝐹‘𝑦) ≤ (𝐹‘𝑤) ↔ (𝐹‘𝑧) ≤ (𝐹‘𝑤))) | 
| 35 | 32, 34 | imbi12d 344 | . . . . . . . 8
⊢ (𝑦 = 𝑧 → ((𝑤 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑤)) ↔ (𝑤 ≤ 𝑧 → (𝐹‘𝑧) ≤ (𝐹‘𝑤)))) | 
| 36 | 31, 35 | cbvral2vw 3241 | . . . . . . 7
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥)) ↔ ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑤 ≤ 𝑧 → (𝐹‘𝑧) ≤ (𝐹‘𝑤))) | 
| 37 | 27, 36 | sylib 218 | . . . . . 6
⊢ (𝜑 → ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑤 ≤ 𝑧 → (𝐹‘𝑧) ≤ (𝐹‘𝑤))) | 
| 38 | 37 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑤 ≤ 𝑧 → (𝐹‘𝑧) ≤ (𝐹‘𝑤))) | 
| 39 | 38, 36 | sylibr 234 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥))) | 
| 40 |  | rexr 11307 | . . . . 5
⊢ (𝑎 ∈ ℝ → 𝑎 ∈
ℝ*) | 
| 41 | 40 | adantl 481 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℝ*) | 
| 42 |  | eqid 2737 | . . . 4
⊢ {𝑥 ∈ 𝐴 ∣ 𝑎 < (𝐹‘𝑥)} = {𝑥 ∈ 𝐴 ∣ 𝑎 < (𝐹‘𝑥)} | 
| 43 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑤 = 𝑥 → (𝐹‘𝑤) = (𝐹‘𝑥)) | 
| 44 | 43 | breq2d 5155 | . . . . . 6
⊢ (𝑤 = 𝑥 → (𝑎 < (𝐹‘𝑤) ↔ 𝑎 < (𝐹‘𝑥))) | 
| 45 | 44 | cbvrabv 3447 | . . . . 5
⊢ {𝑤 ∈ 𝐴 ∣ 𝑎 < (𝐹‘𝑤)} = {𝑥 ∈ 𝐴 ∣ 𝑎 < (𝐹‘𝑥)} | 
| 46 | 45 | supeq1i 9487 | . . . 4
⊢
sup({𝑤 ∈ 𝐴 ∣ 𝑎 < (𝐹‘𝑤)}, ℝ*, < ) = sup({𝑥 ∈ 𝐴 ∣ 𝑎 < (𝐹‘𝑥)}, ℝ*, <
) | 
| 47 |  | eqid 2737 | . . . 4
⊢
(-∞(,)sup({𝑤
∈ 𝐴 ∣ 𝑎 < (𝐹‘𝑤)}, ℝ*, < )) =
(-∞(,)sup({𝑤 ∈
𝐴 ∣ 𝑎 < (𝐹‘𝑤)}, ℝ*, <
)) | 
| 48 |  | eqid 2737 | . . . 4
⊢
(-∞(,]sup({𝑤
∈ 𝐴 ∣ 𝑎 < (𝐹‘𝑤)}, ℝ*, < )) =
(-∞(,]sup({𝑤 ∈
𝐴 ∣ 𝑎 < (𝐹‘𝑤)}, ℝ*, <
)) | 
| 49 | 20, 23, 24, 26, 39, 2, 6, 41, 42, 46, 47, 48 | decsmflem 46781 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → ∃𝑏 ∈ 𝐵 {𝑥 ∈ 𝐴 ∣ 𝑎 < (𝐹‘𝑥)} = (𝑏 ∩ 𝐴)) | 
| 50 | 7 | elexd 3504 | . . . . 5
⊢ (𝜑 → 𝐵 ∈ V) | 
| 51 |  | reex 11246 | . . . . . . 7
⊢ ℝ
∈ V | 
| 52 | 51 | a1i 11 | . . . . . 6
⊢ (𝜑 → ℝ ∈
V) | 
| 53 | 52, 8 | ssexd 5324 | . . . . 5
⊢ (𝜑 → 𝐴 ∈ V) | 
| 54 |  | elrest 17472 | . . . . 5
⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ V) → ({𝑥 ∈ 𝐴 ∣ 𝑎 < (𝐹‘𝑥)} ∈ (𝐵 ↾t 𝐴) ↔ ∃𝑏 ∈ 𝐵 {𝑥 ∈ 𝐴 ∣ 𝑎 < (𝐹‘𝑥)} = (𝑏 ∩ 𝐴))) | 
| 55 | 50, 53, 54 | syl2anc 584 | . . . 4
⊢ (𝜑 → ({𝑥 ∈ 𝐴 ∣ 𝑎 < (𝐹‘𝑥)} ∈ (𝐵 ↾t 𝐴) ↔ ∃𝑏 ∈ 𝐵 {𝑥 ∈ 𝐴 ∣ 𝑎 < (𝐹‘𝑥)} = (𝑏 ∩ 𝐴))) | 
| 56 | 55 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → ({𝑥 ∈ 𝐴 ∣ 𝑎 < (𝐹‘𝑥)} ∈ (𝐵 ↾t 𝐴) ↔ ∃𝑏 ∈ 𝐵 {𝑥 ∈ 𝐴 ∣ 𝑎 < (𝐹‘𝑥)} = (𝑏 ∩ 𝐴))) | 
| 57 | 49, 56 | mpbird 257 | . 2
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐴 ∣ 𝑎 < (𝐹‘𝑥)} ∈ (𝐵 ↾t 𝐴)) | 
| 58 | 1, 7, 16, 17, 57 | issmfgtd 46776 | 1
⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝐵)) |