Detailed syntax breakdown of Definition df-smblfn
Step | Hyp | Ref
| Expression |
1 | | csmblfn 44192 |
. 2
class
SMblFn |
2 | | vs |
. . 3
setvar 𝑠 |
3 | | csalg 43808 |
. . 3
class
SAlg |
4 | | vf |
. . . . . . . . 9
setvar 𝑓 |
5 | 4 | cv 1538 |
. . . . . . . 8
class 𝑓 |
6 | 5 | ccnv 5584 |
. . . . . . 7
class ◡𝑓 |
7 | | cmnf 10995 |
. . . . . . . 8
class
-∞ |
8 | | va |
. . . . . . . . 9
setvar 𝑎 |
9 | 8 | cv 1538 |
. . . . . . . 8
class 𝑎 |
10 | | cioo 13067 |
. . . . . . . 8
class
(,) |
11 | 7, 9, 10 | co 7268 |
. . . . . . 7
class
(-∞(,)𝑎) |
12 | 6, 11 | cima 5588 |
. . . . . 6
class (◡𝑓 “ (-∞(,)𝑎)) |
13 | 2 | cv 1538 |
. . . . . . 7
class 𝑠 |
14 | 5 | cdm 5585 |
. . . . . . 7
class dom 𝑓 |
15 | | crest 17119 |
. . . . . . 7
class
↾t |
16 | 13, 14, 15 | co 7268 |
. . . . . 6
class (𝑠 ↾t dom 𝑓) |
17 | 12, 16 | wcel 2106 |
. . . . 5
wff (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓) |
18 | | cr 10858 |
. . . . 5
class
ℝ |
19 | 17, 8, 18 | wral 3064 |
. . . 4
wff
∀𝑎 ∈
ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓) |
20 | 13 | cuni 4840 |
. . . . 5
class ∪ 𝑠 |
21 | | cpm 8604 |
. . . . 5
class
↑pm |
22 | 18, 20, 21 | co 7268 |
. . . 4
class (ℝ
↑pm ∪ 𝑠) |
23 | 19, 4, 22 | crab 3068 |
. . 3
class {𝑓 ∈ (ℝ
↑pm ∪ 𝑠) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)} |
24 | 2, 3, 23 | cmpt 5157 |
. 2
class (𝑠 ∈ SAlg ↦ {𝑓 ∈ (ℝ
↑pm ∪ 𝑠) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)}) |
25 | 1, 24 | wceq 1539 |
1
wff SMblFn =
(𝑠 ∈ SAlg ↦
{𝑓 ∈ (ℝ
↑pm ∪ 𝑠) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)}) |