Detailed syntax breakdown of Definition df-upgr
Step | Hyp | Ref
| Expression |
1 | | cupgr 27448 |
. 2
class
UPGraph |
2 | | ve |
. . . . . . . 8
setvar 𝑒 |
3 | 2 | cv 1541 |
. . . . . . 7
class 𝑒 |
4 | 3 | cdm 5590 |
. . . . . 6
class dom 𝑒 |
5 | | vx |
. . . . . . . . . 10
setvar 𝑥 |
6 | 5 | cv 1541 |
. . . . . . . . 9
class 𝑥 |
7 | | chash 14042 |
. . . . . . . . 9
class
♯ |
8 | 6, 7 | cfv 6432 |
. . . . . . . 8
class
(♯‘𝑥) |
9 | | c2 12028 |
. . . . . . . 8
class
2 |
10 | | cle 11011 |
. . . . . . . 8
class
≤ |
11 | 8, 9, 10 | wbr 5079 |
. . . . . . 7
wff
(♯‘𝑥)
≤ 2 |
12 | | vv |
. . . . . . . . . 10
setvar 𝑣 |
13 | 12 | cv 1541 |
. . . . . . . . 9
class 𝑣 |
14 | 13 | cpw 4539 |
. . . . . . . 8
class 𝒫
𝑣 |
15 | | c0 4262 |
. . . . . . . . 9
class
∅ |
16 | 15 | csn 4567 |
. . . . . . . 8
class
{∅} |
17 | 14, 16 | cdif 3889 |
. . . . . . 7
class
(𝒫 𝑣 ∖
{∅}) |
18 | 11, 5, 17 | crab 3070 |
. . . . . 6
class {𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣
(♯‘𝑥) ≤
2} |
19 | 4, 18, 3 | wf 6428 |
. . . . 5
wff 𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣
(♯‘𝑥) ≤
2} |
20 | | vg |
. . . . . . 7
setvar 𝑔 |
21 | 20 | cv 1541 |
. . . . . 6
class 𝑔 |
22 | | ciedg 27365 |
. . . . . 6
class
iEdg |
23 | 21, 22 | cfv 6432 |
. . . . 5
class
(iEdg‘𝑔) |
24 | 19, 2, 23 | wsbc 3720 |
. . . 4
wff
[(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣
(♯‘𝑥) ≤
2} |
25 | | cvtx 27364 |
. . . . 5
class
Vtx |
26 | 21, 25 | cfv 6432 |
. . . 4
class
(Vtx‘𝑔) |
27 | 24, 12, 26 | wsbc 3720 |
. . 3
wff
[(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣
(♯‘𝑥) ≤
2} |
28 | 27, 20 | cab 2717 |
. 2
class {𝑔 ∣
[(Vtx‘𝑔) /
𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣
(♯‘𝑥) ≤
2}} |
29 | 1, 28 | wceq 1542 |
1
wff UPGraph =
{𝑔 ∣
[(Vtx‘𝑔) /
𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣
(♯‘𝑥) ≤
2}} |