Step | Hyp | Ref
| Expression |
1 | | cconngr 28839 |
. 2
class
ConnGraph |
2 | | vf |
. . . . . . . . . 10
setvar π |
3 | 2 | cv 1539 |
. . . . . . . . 9
class π |
4 | | vp |
. . . . . . . . . 10
setvar π |
5 | 4 | cv 1539 |
. . . . . . . . 9
class π |
6 | | vk |
. . . . . . . . . . 11
setvar π |
7 | 6 | cv 1539 |
. . . . . . . . . 10
class π |
8 | | vn |
. . . . . . . . . . 11
setvar π |
9 | 8 | cv 1539 |
. . . . . . . . . 10
class π |
10 | | vg |
. . . . . . . . . . . 12
setvar π |
11 | 10 | cv 1539 |
. . . . . . . . . . 11
class π |
12 | | cpthson 28371 |
. . . . . . . . . . 11
class
PathsOn |
13 | 11, 12 | cfv 6480 |
. . . . . . . . . 10
class
(PathsOnβπ) |
14 | 7, 9, 13 | co 7338 |
. . . . . . . . 9
class (π(PathsOnβπ)π) |
15 | 3, 5, 14 | wbr 5093 |
. . . . . . . 8
wff π(π(PathsOnβπ)π)π |
16 | 15, 4 | wex 1780 |
. . . . . . 7
wff
βπ π(π(PathsOnβπ)π)π |
17 | 16, 2 | wex 1780 |
. . . . . 6
wff
βπβπ π(π(PathsOnβπ)π)π |
18 | | vv |
. . . . . . 7
setvar π£ |
19 | 18 | cv 1539 |
. . . . . 6
class π£ |
20 | 17, 8, 19 | wral 3061 |
. . . . 5
wff
βπ β
π£ βπβπ π(π(PathsOnβπ)π)π |
21 | 20, 6, 19 | wral 3061 |
. . . 4
wff
βπ β
π£ βπ β π£ βπβπ π(π(PathsOnβπ)π)π |
22 | | cvtx 27656 |
. . . . 5
class
Vtx |
23 | 11, 22 | cfv 6480 |
. . . 4
class
(Vtxβπ) |
24 | 21, 18, 23 | wsbc 3727 |
. . 3
wff
[(Vtxβπ) / π£]βπ β π£ βπ β π£ βπβπ π(π(PathsOnβπ)π)π |
25 | 24, 10 | cab 2713 |
. 2
class {π β£
[(Vtxβπ) /
π£]βπ β π£ βπ β π£ βπβπ π(π(PathsOnβπ)π)π} |
26 | 1, 25 | wceq 1540 |
1
wff ConnGraph =
{π β£
[(Vtxβπ) /
π£]βπ β π£ βπ β π£ βπβπ π(π(PathsOnβπ)π)π} |