Detailed syntax breakdown of Definition df-struct
Step | Hyp | Ref
| Expression |
1 | | cstr 15691 |
. 2
class
Struct |
2 | | vx |
. . . . . 6
setvar 𝑥 |
3 | 2 | cv 1474 |
. . . . 5
class 𝑥 |
4 | | cle 9954 |
. . . . . 6
class
≤ |
5 | | cn 10897 |
. . . . . . 7
class
ℕ |
6 | 5, 5 | cxp 5036 |
. . . . . 6
class (ℕ
× ℕ) |
7 | 4, 6 | cin 3539 |
. . . . 5
class ( ≤
∩ (ℕ × ℕ)) |
8 | 3, 7 | wcel 1977 |
. . . 4
wff 𝑥 ∈ ( ≤ ∩ (ℕ
× ℕ)) |
9 | | vf |
. . . . . . 7
setvar 𝑓 |
10 | 9 | cv 1474 |
. . . . . 6
class 𝑓 |
11 | | c0 3874 |
. . . . . . 7
class
∅ |
12 | 11 | csn 4125 |
. . . . . 6
class
{∅} |
13 | 10, 12 | cdif 3537 |
. . . . 5
class (𝑓 ∖
{∅}) |
14 | 13 | wfun 5798 |
. . . 4
wff Fun (𝑓 ∖
{∅}) |
15 | 10 | cdm 5038 |
. . . . 5
class dom 𝑓 |
16 | | cfz 12197 |
. . . . . 6
class
... |
17 | 3, 16 | cfv 5804 |
. . . . 5
class
(...‘𝑥) |
18 | 15, 17 | wss 3540 |
. . . 4
wff dom 𝑓 ⊆ (...‘𝑥) |
19 | 8, 14, 18 | w3a 1031 |
. . 3
wff (𝑥 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥)) |
20 | 19, 9, 2 | copab 4642 |
. 2
class
{〈𝑓, 𝑥〉 ∣ (𝑥 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))} |
21 | 1, 20 | wceq 1475 |
1
wff Struct =
{〈𝑓, 𝑥〉 ∣ (𝑥 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))} |