Detailed syntax breakdown of Definition df-sh
Step | Hyp | Ref
| Expression |
1 | | csh 28865 |
. 2
class
Sℋ |
2 | | c0v 28861 |
. . . . 5
class
0ℎ |
3 | | vh |
. . . . . 6
setvar ℎ |
4 | 3 | cv 1541 |
. . . . 5
class ℎ |
5 | 2, 4 | wcel 2114 |
. . . 4
wff
0ℎ ∈ ℎ |
6 | | cva 28857 |
. . . . . 6
class
+ℎ |
7 | 4, 4 | cxp 5523 |
. . . . . 6
class (ℎ × ℎ) |
8 | 6, 7 | cima 5528 |
. . . . 5
class (
+ℎ “ (ℎ × ℎ)) |
9 | 8, 4 | wss 3843 |
. . . 4
wff (
+ℎ “ (ℎ × ℎ)) ⊆ ℎ |
10 | | csm 28858 |
. . . . . 6
class
·ℎ |
11 | | cc 10615 |
. . . . . . 7
class
ℂ |
12 | 11, 4 | cxp 5523 |
. . . . . 6
class (ℂ
× ℎ) |
13 | 10, 12 | cima 5528 |
. . . . 5
class (
·ℎ “ (ℂ × ℎ)) |
14 | 13, 4 | wss 3843 |
. . . 4
wff (
·ℎ “ (ℂ × ℎ)) ⊆ ℎ |
15 | 5, 9, 14 | w3a 1088 |
. . 3
wff
(0ℎ ∈ ℎ ∧ ( +ℎ “ (ℎ × ℎ)) ⊆ ℎ ∧ ( ·ℎ
“ (ℂ × ℎ))
⊆ ℎ) |
16 | | chba 28856 |
. . . 4
class
ℋ |
17 | 16 | cpw 4488 |
. . 3
class 𝒫
ℋ |
18 | 15, 3, 17 | crab 3057 |
. 2
class {ℎ ∈ 𝒫 ℋ ∣
(0ℎ ∈ ℎ ∧ ( +ℎ “ (ℎ × ℎ)) ⊆ ℎ ∧ ( ·ℎ
“ (ℂ × ℎ))
⊆ ℎ)} |
19 | 1, 18 | wceq 1542 |
1
wff
Sℋ = {ℎ ∈ 𝒫 ℋ ∣
(0ℎ ∈ ℎ ∧ ( +ℎ “ (ℎ × ℎ)) ⊆ ℎ ∧ ( ·ℎ
“ (ℂ × ℎ))
⊆ ℎ)} |