Detailed syntax breakdown of Definition df-stgr
Step | Hyp | Ref
| Expression |
1 | | cstgr 47853 |
. 2
class
StarGr |
2 | | vn |
. . 3
setvar 𝑛 |
3 | | cn0 12523 |
. . 3
class
ℕ0 |
4 | | cnx 17226 |
. . . . . 6
class
ndx |
5 | | cbs 17244 |
. . . . . 6
class
Base |
6 | 4, 5 | cfv 6562 |
. . . . 5
class
(Base‘ndx) |
7 | | cc0 11152 |
. . . . . 6
class
0 |
8 | 2 | cv 1535 |
. . . . . 6
class 𝑛 |
9 | | cfz 13543 |
. . . . . 6
class
... |
10 | 7, 8, 9 | co 7430 |
. . . . 5
class
(0...𝑛) |
11 | 6, 10 | cop 4636 |
. . . 4
class
〈(Base‘ndx), (0...𝑛)〉 |
12 | | cedgf 29017 |
. . . . . 6
class
.ef |
13 | 4, 12 | cfv 6562 |
. . . . 5
class
(.ef‘ndx) |
14 | | cid 5581 |
. . . . . 6
class
I |
15 | | ve |
. . . . . . . . . 10
setvar 𝑒 |
16 | 15 | cv 1535 |
. . . . . . . . 9
class 𝑒 |
17 | | vx |
. . . . . . . . . . 11
setvar 𝑥 |
18 | 17 | cv 1535 |
. . . . . . . . . 10
class 𝑥 |
19 | 7, 18 | cpr 4632 |
. . . . . . . . 9
class {0, 𝑥} |
20 | 16, 19 | wceq 1536 |
. . . . . . . 8
wff 𝑒 = {0, 𝑥} |
21 | | c1 11153 |
. . . . . . . . 9
class
1 |
22 | 21, 8, 9 | co 7430 |
. . . . . . . 8
class
(1...𝑛) |
23 | 20, 17, 22 | wrex 3067 |
. . . . . . 7
wff
∃𝑥 ∈
(1...𝑛)𝑒 = {0, 𝑥} |
24 | 10 | cpw 4604 |
. . . . . . 7
class 𝒫
(0...𝑛) |
25 | 23, 15, 24 | crab 3432 |
. . . . . 6
class {𝑒 ∈ 𝒫 (0...𝑛) ∣ ∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}} |
26 | 14, 25 | cres 5690 |
. . . . 5
class ( I
↾ {𝑒 ∈ 𝒫
(0...𝑛) ∣
∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}}) |
27 | 13, 26 | cop 4636 |
. . . 4
class
〈(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 (0...𝑛) ∣ ∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}})〉 |
28 | 11, 27 | cpr 4632 |
. . 3
class
{〈(Base‘ndx), (0...𝑛)〉, 〈(.ef‘ndx), ( I ↾
{𝑒 ∈ 𝒫
(0...𝑛) ∣
∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}})〉} |
29 | 2, 3, 28 | cmpt 5230 |
. 2
class (𝑛 ∈ ℕ0
↦ {〈(Base‘ndx), (0...𝑛)〉, 〈(.ef‘ndx), ( I ↾
{𝑒 ∈ 𝒫
(0...𝑛) ∣
∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}})〉}) |
30 | 1, 29 | wceq 1536 |
1
wff StarGr =
(𝑛 ∈
ℕ0 ↦ {〈(Base‘ndx), (0...𝑛)〉, 〈(.ef‘ndx), ( I ↾
{𝑒 ∈ 𝒫
(0...𝑛) ∣
∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}})〉}) |