Detailed syntax breakdown of Definition df-stgr
| Step | Hyp | Ref
| Expression |
| 1 | | cstgr 47918 |
. 2
class
StarGr |
| 2 | | vn |
. . 3
setvar 𝑛 |
| 3 | | cn0 12526 |
. . 3
class
ℕ0 |
| 4 | | cnx 17230 |
. . . . . 6
class
ndx |
| 5 | | cbs 17247 |
. . . . . 6
class
Base |
| 6 | 4, 5 | cfv 6561 |
. . . . 5
class
(Base‘ndx) |
| 7 | | cc0 11155 |
. . . . . 6
class
0 |
| 8 | 2 | cv 1539 |
. . . . . 6
class 𝑛 |
| 9 | | cfz 13547 |
. . . . . 6
class
... |
| 10 | 7, 8, 9 | co 7431 |
. . . . 5
class
(0...𝑛) |
| 11 | 6, 10 | cop 4632 |
. . . 4
class
〈(Base‘ndx), (0...𝑛)〉 |
| 12 | | cedgf 29003 |
. . . . . 6
class
.ef |
| 13 | 4, 12 | cfv 6561 |
. . . . 5
class
(.ef‘ndx) |
| 14 | | cid 5577 |
. . . . . 6
class
I |
| 15 | | ve |
. . . . . . . . . 10
setvar 𝑒 |
| 16 | 15 | cv 1539 |
. . . . . . . . 9
class 𝑒 |
| 17 | | vx |
. . . . . . . . . . 11
setvar 𝑥 |
| 18 | 17 | cv 1539 |
. . . . . . . . . 10
class 𝑥 |
| 19 | 7, 18 | cpr 4628 |
. . . . . . . . 9
class {0, 𝑥} |
| 20 | 16, 19 | wceq 1540 |
. . . . . . . 8
wff 𝑒 = {0, 𝑥} |
| 21 | | c1 11156 |
. . . . . . . . 9
class
1 |
| 22 | 21, 8, 9 | co 7431 |
. . . . . . . 8
class
(1...𝑛) |
| 23 | 20, 17, 22 | wrex 3070 |
. . . . . . 7
wff
∃𝑥 ∈
(1...𝑛)𝑒 = {0, 𝑥} |
| 24 | 10 | cpw 4600 |
. . . . . . 7
class 𝒫
(0...𝑛) |
| 25 | 23, 15, 24 | crab 3436 |
. . . . . 6
class {𝑒 ∈ 𝒫 (0...𝑛) ∣ ∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}} |
| 26 | 14, 25 | cres 5687 |
. . . . 5
class ( I
↾ {𝑒 ∈ 𝒫
(0...𝑛) ∣
∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}}) |
| 27 | 13, 26 | cop 4632 |
. . . 4
class
〈(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 (0...𝑛) ∣ ∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}})〉 |
| 28 | 11, 27 | cpr 4628 |
. . 3
class
{〈(Base‘ndx), (0...𝑛)〉, 〈(.ef‘ndx), ( I ↾
{𝑒 ∈ 𝒫
(0...𝑛) ∣
∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}})〉} |
| 29 | 2, 3, 28 | cmpt 5225 |
. 2
class (𝑛 ∈ ℕ0
↦ {〈(Base‘ndx), (0...𝑛)〉, 〈(.ef‘ndx), ( I ↾
{𝑒 ∈ 𝒫
(0...𝑛) ∣
∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}})〉}) |
| 30 | 1, 29 | wceq 1540 |
1
wff StarGr =
(𝑛 ∈
ℕ0 ↦ {〈(Base‘ndx), (0...𝑛)〉, 〈(.ef‘ndx), ( I ↾
{𝑒 ∈ 𝒫
(0...𝑛) ∣
∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}})〉}) |