Detailed syntax breakdown of Definition df-conngra
Step | Hyp | Ref
| Expression |
1 | | cconngra 26197 |
. 2
class
ConnGrph |
2 | | vf |
. . . . . . . . 9
setvar 𝑓 |
3 | 2 | cv 1474 |
. . . . . . . 8
class 𝑓 |
4 | | vp |
. . . . . . . . 9
setvar 𝑝 |
5 | 4 | cv 1474 |
. . . . . . . 8
class 𝑝 |
6 | | vk |
. . . . . . . . . 10
setvar 𝑘 |
7 | 6 | cv 1474 |
. . . . . . . . 9
class 𝑘 |
8 | | vn |
. . . . . . . . . 10
setvar 𝑛 |
9 | 8 | cv 1474 |
. . . . . . . . 9
class 𝑛 |
10 | | vv |
. . . . . . . . . . 11
setvar 𝑣 |
11 | 10 | cv 1474 |
. . . . . . . . . 10
class 𝑣 |
12 | | ve |
. . . . . . . . . . 11
setvar 𝑒 |
13 | 12 | cv 1474 |
. . . . . . . . . 10
class 𝑒 |
14 | | cpthon 26032 |
. . . . . . . . . 10
class
PathOn |
15 | 11, 13, 14 | co 6549 |
. . . . . . . . 9
class (𝑣 PathOn 𝑒) |
16 | 7, 9, 15 | co 6549 |
. . . . . . . 8
class (𝑘(𝑣 PathOn 𝑒)𝑛) |
17 | 3, 5, 16 | wbr 4583 |
. . . . . . 7
wff 𝑓(𝑘(𝑣 PathOn 𝑒)𝑛)𝑝 |
18 | 17, 4 | wex 1695 |
. . . . . 6
wff
∃𝑝 𝑓(𝑘(𝑣 PathOn 𝑒)𝑛)𝑝 |
19 | 18, 2 | wex 1695 |
. . . . 5
wff
∃𝑓∃𝑝 𝑓(𝑘(𝑣 PathOn 𝑒)𝑛)𝑝 |
20 | 19, 8, 11 | wral 2896 |
. . . 4
wff
∀𝑛 ∈
𝑣 ∃𝑓∃𝑝 𝑓(𝑘(𝑣 PathOn 𝑒)𝑛)𝑝 |
21 | 20, 6, 11 | wral 2896 |
. . 3
wff
∀𝑘 ∈
𝑣 ∀𝑛 ∈ 𝑣 ∃𝑓∃𝑝 𝑓(𝑘(𝑣 PathOn 𝑒)𝑛)𝑝 |
22 | 21, 10, 12 | copab 4642 |
. 2
class
{〈𝑣, 𝑒〉 ∣ ∀𝑘 ∈ 𝑣 ∀𝑛 ∈ 𝑣 ∃𝑓∃𝑝 𝑓(𝑘(𝑣 PathOn 𝑒)𝑛)𝑝} |
23 | 1, 22 | wceq 1475 |
1
wff ConnGrph =
{〈𝑣, 𝑒〉 ∣ ∀𝑘 ∈ 𝑣 ∀𝑛 ∈ 𝑣 ∃𝑓∃𝑝 𝑓(𝑘(𝑣 PathOn 𝑒)𝑛)𝑝} |