Step | Hyp | Ref
| Expression |
1 | | csmblfn 45022 |
. 2
class
SMblFn |
2 | | vs |
. . 3
setvar 𝑠 |
3 | | csalg 44635 |
. . 3
class
SAlg |
4 | | vf |
. . . . . . . . 9
setvar 𝑓 |
5 | 4 | cv 1541 |
. . . . . . . 8
class 𝑓 |
6 | 5 | ccnv 5633 |
. . . . . . 7
class ◡𝑓 |
7 | | cmnf 11192 |
. . . . . . . 8
class
-∞ |
8 | | va |
. . . . . . . . 9
setvar 𝑎 |
9 | 8 | cv 1541 |
. . . . . . . 8
class 𝑎 |
10 | | cioo 13270 |
. . . . . . . 8
class
(,) |
11 | 7, 9, 10 | co 7358 |
. . . . . . 7
class
(-∞(,)𝑎) |
12 | 6, 11 | cima 5637 |
. . . . . 6
class (◡𝑓 “ (-∞(,)𝑎)) |
13 | 2 | cv 1541 |
. . . . . . 7
class 𝑠 |
14 | 5 | cdm 5634 |
. . . . . . 7
class dom 𝑓 |
15 | | crest 17307 |
. . . . . . 7
class
↾t |
16 | 13, 14, 15 | co 7358 |
. . . . . 6
class (𝑠 ↾t dom 𝑓) |
17 | 12, 16 | wcel 2107 |
. . . . 5
wff (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓) |
18 | | cr 11055 |
. . . . 5
class
ℝ |
19 | 17, 8, 18 | wral 3061 |
. . . 4
wff
∀𝑎 ∈
ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓) |
20 | 13 | cuni 4866 |
. . . . 5
class ∪ 𝑠 |
21 | | cpm 8769 |
. . . . 5
class
↑pm |
22 | 18, 20, 21 | co 7358 |
. . . 4
class (ℝ
↑pm ∪ 𝑠) |
23 | 19, 4, 22 | crab 3406 |
. . 3
class {𝑓 ∈ (ℝ
↑pm ∪ 𝑠) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)} |
24 | 2, 3, 23 | cmpt 5189 |
. 2
class (𝑠 ∈ SAlg ↦ {𝑓 ∈ (ℝ
↑pm ∪ 𝑠) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)}) |
25 | 1, 24 | wceq 1542 |
1
wff SMblFn =
(𝑠 ∈ SAlg ↦
{𝑓 ∈ (ℝ
↑pm ∪ 𝑠) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)}) |