Detailed syntax breakdown of Definition df-conngr
Step | Hyp | Ref
| Expression |
1 | | cconngr 28300 |
. 2
class
ConnGraph |
2 | | vf |
. . . . . . . . . 10
setvar 𝑓 |
3 | 2 | cv 1542 |
. . . . . . . . 9
class 𝑓 |
4 | | vp |
. . . . . . . . . 10
setvar 𝑝 |
5 | 4 | cv 1542 |
. . . . . . . . 9
class 𝑝 |
6 | | vk |
. . . . . . . . . . 11
setvar 𝑘 |
7 | 6 | cv 1542 |
. . . . . . . . . 10
class 𝑘 |
8 | | vn |
. . . . . . . . . . 11
setvar 𝑛 |
9 | 8 | cv 1542 |
. . . . . . . . . 10
class 𝑛 |
10 | | vg |
. . . . . . . . . . . 12
setvar 𝑔 |
11 | 10 | cv 1542 |
. . . . . . . . . . 11
class 𝑔 |
12 | | cpthson 27832 |
. . . . . . . . . . 11
class
PathsOn |
13 | 11, 12 | cfv 6400 |
. . . . . . . . . 10
class
(PathsOn‘𝑔) |
14 | 7, 9, 13 | co 7234 |
. . . . . . . . 9
class (𝑘(PathsOn‘𝑔)𝑛) |
15 | 3, 5, 14 | wbr 5069 |
. . . . . . . 8
wff 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝 |
16 | 15, 4 | wex 1787 |
. . . . . . 7
wff
∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝 |
17 | 16, 2 | wex 1787 |
. . . . . 6
wff
∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝 |
18 | | vv |
. . . . . . 7
setvar 𝑣 |
19 | 18 | cv 1542 |
. . . . . 6
class 𝑣 |
20 | 17, 8, 19 | wral 3064 |
. . . . 5
wff
∀𝑛 ∈
𝑣 ∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝 |
21 | 20, 6, 19 | wral 3064 |
. . . 4
wff
∀𝑘 ∈
𝑣 ∀𝑛 ∈ 𝑣 ∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝 |
22 | | cvtx 27118 |
. . . . 5
class
Vtx |
23 | 11, 22 | cfv 6400 |
. . . 4
class
(Vtx‘𝑔) |
24 | 21, 18, 23 | wsbc 3711 |
. . 3
wff
[(Vtx‘𝑔) / 𝑣]∀𝑘 ∈ 𝑣 ∀𝑛 ∈ 𝑣 ∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝 |
25 | 24, 10 | cab 2716 |
. 2
class {𝑔 ∣
[(Vtx‘𝑔) /
𝑣]∀𝑘 ∈ 𝑣 ∀𝑛 ∈ 𝑣 ∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝} |
26 | 1, 25 | wceq 1543 |
1
wff ConnGraph =
{𝑔 ∣
[(Vtx‘𝑔) /
𝑣]∀𝑘 ∈ 𝑣 ∀𝑛 ∈ 𝑣 ∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝} |