Detailed syntax breakdown of Definition df-scut
Step | Hyp | Ref
| Expression |
1 | | cscut 33618 |
. 2
class
|s |
2 | | va |
. . 3
setvar 𝑎 |
3 | | vb |
. . 3
setvar 𝑏 |
4 | | csur 33484 |
. . . 4
class No |
5 | 4 | cpw 4488 |
. . 3
class 𝒫
No |
6 | | csslt 33616 |
. . . 4
class
<<s |
7 | 2 | cv 1541 |
. . . . 5
class 𝑎 |
8 | 7 | csn 4516 |
. . . 4
class {𝑎} |
9 | 6, 8 | cima 5528 |
. . 3
class (
<<s “ {𝑎}) |
10 | | vx |
. . . . . . 7
setvar 𝑥 |
11 | 10 | cv 1541 |
. . . . . 6
class 𝑥 |
12 | | cbday 33486 |
. . . . . 6
class bday |
13 | 11, 12 | cfv 6339 |
. . . . 5
class ( bday ‘𝑥) |
14 | | vy |
. . . . . . . . . . . 12
setvar 𝑦 |
15 | 14 | cv 1541 |
. . . . . . . . . . 11
class 𝑦 |
16 | 15 | csn 4516 |
. . . . . . . . . 10
class {𝑦} |
17 | 7, 16, 6 | wbr 5030 |
. . . . . . . . 9
wff 𝑎 <<s {𝑦} |
18 | 3 | cv 1541 |
. . . . . . . . . 10
class 𝑏 |
19 | 16, 18, 6 | wbr 5030 |
. . . . . . . . 9
wff {𝑦} <<s 𝑏 |
20 | 17, 19 | wa 399 |
. . . . . . . 8
wff (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏) |
21 | 20, 14, 4 | crab 3057 |
. . . . . . 7
class {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)} |
22 | 12, 21 | cima 5528 |
. . . . . 6
class ( bday “ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}) |
23 | 22 | cint 4836 |
. . . . 5
class ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)}) |
24 | 13, 23 | wceq 1542 |
. . . 4
wff ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}) |
25 | 24, 10, 21 | crio 7126 |
. . 3
class
(℩𝑥
∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)})) |
26 | 2, 3, 5, 9, 25 | cmpo 7172 |
. 2
class (𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)}))) |
27 | 1, 26 | wceq 1542 |
1
wff |s =
(𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (℩𝑥 ∈ {𝑦 ∈ No
∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday
‘𝑥) = ∩ ( bday “ {𝑦 ∈
No ∣ (𝑎
<<s {𝑦} ∧ {𝑦} <<s 𝑏)}))) |