| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpr 484 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹 ∈ (SMblFn‘𝑆)) | 
| 2 |  | df-smblfn 46716 | . . . . . . . . 9
⊢ SMblFn =
(𝑠 ∈ SAlg ↦
{𝑓 ∈ (ℝ
↑pm ∪ 𝑠) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)}) | 
| 3 |  | unieq 4917 | . . . . . . . . . . . 12
⊢ (𝑠 = 𝑆 → ∪ 𝑠 = ∪
𝑆) | 
| 4 | 3 | oveq2d 7448 | . . . . . . . . . . 11
⊢ (𝑠 = 𝑆 → (ℝ ↑pm ∪ 𝑠) =
(ℝ ↑pm ∪ 𝑆)) | 
| 5 | 4 | rabeqdv 3451 | . . . . . . . . . 10
⊢ (𝑠 = 𝑆 → {𝑓 ∈ (ℝ ↑pm ∪ 𝑠)
∣ ∀𝑎 ∈
ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)} = {𝑓 ∈ (ℝ ↑pm ∪ 𝑆)
∣ ∀𝑎 ∈
ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)}) | 
| 6 |  | oveq1 7439 | . . . . . . . . . . . . 13
⊢ (𝑠 = 𝑆 → (𝑠 ↾t dom 𝑓) = (𝑆 ↾t dom 𝑓)) | 
| 7 | 6 | eleq2d 2826 | . . . . . . . . . . . 12
⊢ (𝑠 = 𝑆 → ((◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓) ↔ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓))) | 
| 8 | 7 | ralbidv 3177 | . . . . . . . . . . 11
⊢ (𝑠 = 𝑆 → (∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓) ↔ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓))) | 
| 9 | 8 | rabbidv 3443 | . . . . . . . . . 10
⊢ (𝑠 = 𝑆 → {𝑓 ∈ (ℝ ↑pm ∪ 𝑆)
∣ ∀𝑎 ∈
ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)} = {𝑓 ∈ (ℝ ↑pm ∪ 𝑆)
∣ ∀𝑎 ∈
ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)}) | 
| 10 | 5, 9 | eqtrd 2776 | . . . . . . . . 9
⊢ (𝑠 = 𝑆 → {𝑓 ∈ (ℝ ↑pm ∪ 𝑠)
∣ ∀𝑎 ∈
ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)} = {𝑓 ∈ (ℝ ↑pm ∪ 𝑆)
∣ ∀𝑎 ∈
ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)}) | 
| 11 |  | issmflem.s | . . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ SAlg) | 
| 12 |  | ovex 7465 | . . . . . . . . . . 11
⊢ (ℝ
↑pm ∪ 𝑆) ∈ V | 
| 13 | 12 | rabex 5338 | . . . . . . . . . 10
⊢ {𝑓 ∈ (ℝ
↑pm ∪ 𝑆) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} ∈ V | 
| 14 | 13 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → {𝑓 ∈ (ℝ ↑pm ∪ 𝑆)
∣ ∀𝑎 ∈
ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} ∈ V) | 
| 15 | 2, 10, 11, 14 | fvmptd3 7038 | . . . . . . . 8
⊢ (𝜑 → (SMblFn‘𝑆) = {𝑓 ∈ (ℝ ↑pm ∪ 𝑆)
∣ ∀𝑎 ∈
ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)}) | 
| 16 | 15 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → (SMblFn‘𝑆) = {𝑓 ∈ (ℝ ↑pm ∪ 𝑆)
∣ ∀𝑎 ∈
ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)}) | 
| 17 | 1, 16 | eleqtrd 2842 | . . . . . 6
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹 ∈ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆)
∣ ∀𝑎 ∈
ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)}) | 
| 18 |  | elrabi 3686 | . . . . . 6
⊢ (𝐹 ∈ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆)
∣ ∀𝑎 ∈
ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} → 𝐹 ∈ (ℝ ↑pm ∪ 𝑆)) | 
| 19 | 17, 18 | syl 17 | . . . . 5
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹 ∈ (ℝ ↑pm ∪ 𝑆)) | 
| 20 |  | issmflem.d | . . . . . . 7
⊢ 𝐷 = dom 𝐹 | 
| 21 |  | elpmi2 45235 | . . . . . . 7
⊢ (𝐹 ∈ (ℝ
↑pm ∪ 𝑆) → dom 𝐹 ⊆ ∪ 𝑆) | 
| 22 | 20, 21 | eqsstrid 4021 | . . . . . 6
⊢ (𝐹 ∈ (ℝ
↑pm ∪ 𝑆) → 𝐷 ⊆ ∪ 𝑆) | 
| 23 | 22 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ 𝐹 ∈ (ℝ ↑pm ∪ 𝑆))
→ 𝐷 ⊆ ∪ 𝑆) | 
| 24 | 19, 23 | syldan 591 | . . . 4
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐷 ⊆ ∪ 𝑆) | 
| 25 |  | elpmi 8887 | . . . . . . 7
⊢ (𝐹 ∈ (ℝ
↑pm ∪ 𝑆) → (𝐹:dom 𝐹⟶ℝ ∧ dom 𝐹 ⊆ ∪ 𝑆)) | 
| 26 | 19, 25 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → (𝐹:dom 𝐹⟶ℝ ∧ dom 𝐹 ⊆ ∪ 𝑆)) | 
| 27 | 26 | simpld 494 | . . . . 5
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹:dom 𝐹⟶ℝ) | 
| 28 | 20 | feq2i 6727 | . . . . . 6
⊢ (𝐹:𝐷⟶ℝ ↔ 𝐹:dom 𝐹⟶ℝ) | 
| 29 | 28 | a1i 11 | . . . . 5
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → (𝐹:𝐷⟶ℝ ↔ 𝐹:dom 𝐹⟶ℝ)) | 
| 30 | 27, 29 | mpbird 257 | . . . 4
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → 𝐹:𝐷⟶ℝ) | 
| 31 |  | cnveq 5883 | . . . . . . . . . . . . . 14
⊢ (𝑓 = 𝐹 → ◡𝑓 = ◡𝐹) | 
| 32 | 31 | imaeq1d 6076 | . . . . . . . . . . . . 13
⊢ (𝑓 = 𝐹 → (◡𝑓 “ (-∞(,)𝑎)) = (◡𝐹 “ (-∞(,)𝑎))) | 
| 33 |  | dmeq 5913 | . . . . . . . . . . . . . 14
⊢ (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹) | 
| 34 | 33 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (𝑓 = 𝐹 → (𝑆 ↾t dom 𝑓) = (𝑆 ↾t dom 𝐹)) | 
| 35 | 32, 34 | eleq12d 2834 | . . . . . . . . . . . 12
⊢ (𝑓 = 𝐹 → ((◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓) ↔ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))) | 
| 36 | 35 | ralbidv 3177 | . . . . . . . . . . 11
⊢ (𝑓 = 𝐹 → (∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓) ↔ ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))) | 
| 37 | 36 | elrab 3691 | . . . . . . . . . 10
⊢ (𝐹 ∈ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆)
∣ ∀𝑎 ∈
ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} ↔ (𝐹 ∈ (ℝ ↑pm ∪ 𝑆)
∧ ∀𝑎 ∈
ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))) | 
| 38 | 37 | simprbi 496 | . . . . . . . . 9
⊢ (𝐹 ∈ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆)
∣ ∀𝑎 ∈
ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)) | 
| 39 | 17, 38 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)) | 
| 40 | 39 | adantr 480 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)) | 
| 41 |  | simpr 484 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℝ) | 
| 42 |  | rspa 3247 | . . . . . . 7
⊢
((∀𝑎 ∈
ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹) ∧ 𝑎 ∈ ℝ) → (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)) | 
| 43 | 40, 41, 42 | syl2anc 584 | . . . . . 6
⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)) | 
| 44 | 30 | adantr 480 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → 𝐹:𝐷⟶ℝ) | 
| 45 |  | simpl 482 | . . . . . . . . . 10
⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → 𝐹:𝐷⟶ℝ) | 
| 46 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℝ) | 
| 47 | 46 | rexrd 11312 | . . . . . . . . . 10
⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℝ*) | 
| 48 | 45, 47 | preimaioomnf 46739 | . . . . . . . . 9
⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → (◡𝐹 “ (-∞(,)𝑎)) = {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎}) | 
| 49 | 48 | eqcomd 2742 | . . . . . . . 8
⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} = (◡𝐹 “ (-∞(,)𝑎))) | 
| 50 | 44, 41, 49 | syl2anc 584 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} = (◡𝐹 “ (-∞(,)𝑎))) | 
| 51 | 20 | oveq2i 7443 | . . . . . . . 8
⊢ (𝑆 ↾t 𝐷) = (𝑆 ↾t dom 𝐹) | 
| 52 | 51 | a1i 11 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → (𝑆 ↾t 𝐷) = (𝑆 ↾t dom 𝐹)) | 
| 53 | 50, 52 | eleq12d 2834 | . . . . . 6
⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → ({𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷) ↔ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))) | 
| 54 | 43, 53 | mpbird 257 | . . . . 5
⊢ (((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷)) | 
| 55 | 54 | ralrimiva 3145 | . . . 4
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷)) | 
| 56 | 24, 30, 55 | 3jca 1128 | . . 3
⊢ ((𝜑 ∧ 𝐹 ∈ (SMblFn‘𝑆)) → (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) | 
| 57 | 56 | ex 412 | . 2
⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) → (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷)))) | 
| 58 |  | reex 11247 | . . . . . . . . 9
⊢ ℝ
∈ V | 
| 59 | 58 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → ℝ ∈
V) | 
| 60 | 11 | uniexd 7763 | . . . . . . . . 9
⊢ (𝜑 → ∪ 𝑆
∈ V) | 
| 61 | 60 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → ∪ 𝑆
∈ V) | 
| 62 |  | simprr 772 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → 𝐹:𝐷⟶ℝ) | 
| 63 |  | fssxp 6762 | . . . . . . . . . . . 12
⊢ (𝐹:𝐷⟶ℝ → 𝐹 ⊆ (𝐷 × ℝ)) | 
| 64 | 63 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝐷 ⊆ ∪ 𝑆
∧ 𝐹:𝐷⟶ℝ) → 𝐹 ⊆ (𝐷 × ℝ)) | 
| 65 |  | xpss1 5703 | . . . . . . . . . . . 12
⊢ (𝐷 ⊆ ∪ 𝑆
→ (𝐷 × ℝ)
⊆ (∪ 𝑆 × ℝ)) | 
| 66 | 65 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝐷 ⊆ ∪ 𝑆
∧ 𝐹:𝐷⟶ℝ) → (𝐷 × ℝ) ⊆ (∪ 𝑆
× ℝ)) | 
| 67 | 64, 66 | sstrd 3993 | . . . . . . . . . 10
⊢ ((𝐷 ⊆ ∪ 𝑆
∧ 𝐹:𝐷⟶ℝ) → 𝐹 ⊆ (∪ 𝑆 ×
ℝ)) | 
| 68 | 67 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → 𝐹 ⊆ (∪ 𝑆 ×
ℝ)) | 
| 69 |  | dmss 5912 | . . . . . . . . . . . 12
⊢ (𝐹 ⊆ (∪ 𝑆
× ℝ) → dom 𝐹 ⊆ dom (∪
𝑆 ×
ℝ)) | 
| 70 |  | dmxpss 6190 | . . . . . . . . . . . . 13
⊢ dom
(∪ 𝑆 × ℝ) ⊆ ∪ 𝑆 | 
| 71 | 70 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝐹 ⊆ (∪ 𝑆
× ℝ) → dom (∪ 𝑆 × ℝ) ⊆ ∪ 𝑆) | 
| 72 | 69, 71 | sstrd 3993 | . . . . . . . . . . 11
⊢ (𝐹 ⊆ (∪ 𝑆
× ℝ) → dom 𝐹 ⊆ ∪ 𝑆) | 
| 73 | 72 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ⊆ (∪ 𝑆 × ℝ)) → dom
𝐹 ⊆ ∪ 𝑆) | 
| 74 | 20, 73 | eqsstrid 4021 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹 ⊆ (∪ 𝑆 × ℝ)) → 𝐷 ⊆ ∪ 𝑆) | 
| 75 | 68, 74 | syldan 591 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → 𝐷 ⊆ ∪ 𝑆) | 
| 76 |  | elpm2r 8886 | . . . . . . . 8
⊢
(((ℝ ∈ V ∧ ∪ 𝑆 ∈ V) ∧ (𝐹:𝐷⟶ℝ ∧ 𝐷 ⊆ ∪ 𝑆)) → 𝐹 ∈ (ℝ ↑pm ∪ 𝑆)) | 
| 77 | 59, 61, 62, 75, 76 | syl22anc 838 | . . . . . . 7
⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ)) → 𝐹 ∈ (ℝ ↑pm ∪ 𝑆)) | 
| 78 | 77 | 3adantr3 1171 | . . . . . 6
⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → 𝐹 ∈ (ℝ ↑pm ∪ 𝑆)) | 
| 79 | 20 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → 𝐷 = dom 𝐹) | 
| 80 | 79 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → (𝑆 ↾t 𝐷) = (𝑆 ↾t dom 𝐹)) | 
| 81 | 49, 80 | eleq12d 2834 | . . . . . . . . . . 11
⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑎 ∈ ℝ) → ({𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷) ↔ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))) | 
| 82 | 81 | ralbidva 3175 | . . . . . . . . . 10
⊢ (𝐹:𝐷⟶ℝ → (∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷) ↔ ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))) | 
| 83 | 82 | biimpd 229 | . . . . . . . . 9
⊢ (𝐹:𝐷⟶ℝ → (∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))) | 
| 84 | 83 | imp 406 | . . . . . . . 8
⊢ ((𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷)) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)) | 
| 85 | 84 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ (𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)) | 
| 86 | 85 | 3adantr1 1169 | . . . . . 6
⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → ∀𝑎 ∈ ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹)) | 
| 87 | 78, 86 | jca 511 | . . . . 5
⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → (𝐹 ∈ (ℝ ↑pm ∪ 𝑆)
∧ ∀𝑎 ∈
ℝ (◡𝐹 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝐹))) | 
| 88 | 87, 37 | sylibr 234 | . . . 4
⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → 𝐹 ∈ {𝑓 ∈ (ℝ ↑pm ∪ 𝑆)
∣ ∀𝑎 ∈
ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)}) | 
| 89 | 15 | eqcomd 2742 | . . . . 5
⊢ (𝜑 → {𝑓 ∈ (ℝ ↑pm ∪ 𝑆)
∣ ∀𝑎 ∈
ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} = (SMblFn‘𝑆)) | 
| 90 | 89 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → {𝑓 ∈ (ℝ ↑pm ∪ 𝑆)
∣ ∀𝑎 ∈
ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑆 ↾t dom 𝑓)} = (SMblFn‘𝑆)) | 
| 91 | 88, 90 | eleqtrd 2842 | . . 3
⊢ ((𝜑 ∧ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))) → 𝐹 ∈ (SMblFn‘𝑆)) | 
| 92 | 91 | ex 412 | . 2
⊢ (𝜑 → ((𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷)) → 𝐹 ∈ (SMblFn‘𝑆))) | 
| 93 | 57, 92 | impbid 212 | 1
⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) ↔ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷)))) |