Step |
Hyp |
Ref |
Expression |
0 |
|
cconngr |
⊢ ConnGraph |
1 |
|
vg |
⊢ 𝑔 |
2 |
|
cvtx |
⊢ Vtx |
3 |
1
|
cv |
⊢ 𝑔 |
4 |
3 2
|
cfv |
⊢ ( Vtx ‘ 𝑔 ) |
5 |
|
vv |
⊢ 𝑣 |
6 |
|
vk |
⊢ 𝑘 |
7 |
5
|
cv |
⊢ 𝑣 |
8 |
|
vn |
⊢ 𝑛 |
9 |
|
vf |
⊢ 𝑓 |
10 |
|
vp |
⊢ 𝑝 |
11 |
9
|
cv |
⊢ 𝑓 |
12 |
6
|
cv |
⊢ 𝑘 |
13 |
|
cpthson |
⊢ PathsOn |
14 |
3 13
|
cfv |
⊢ ( PathsOn ‘ 𝑔 ) |
15 |
8
|
cv |
⊢ 𝑛 |
16 |
12 15 14
|
co |
⊢ ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) |
17 |
10
|
cv |
⊢ 𝑝 |
18 |
11 17 16
|
wbr |
⊢ 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 |
19 |
18 10
|
wex |
⊢ ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 |
20 |
19 9
|
wex |
⊢ ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 |
21 |
20 8 7
|
wral |
⊢ ∀ 𝑛 ∈ 𝑣 ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 |
22 |
21 6 7
|
wral |
⊢ ∀ 𝑘 ∈ 𝑣 ∀ 𝑛 ∈ 𝑣 ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 |
23 |
22 5 4
|
wsbc |
⊢ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] ∀ 𝑘 ∈ 𝑣 ∀ 𝑛 ∈ 𝑣 ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 |
24 |
23 1
|
cab |
⊢ { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] ∀ 𝑘 ∈ 𝑣 ∀ 𝑛 ∈ 𝑣 ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 } |
25 |
0 24
|
wceq |
⊢ ConnGraph = { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] ∀ 𝑘 ∈ 𝑣 ∀ 𝑛 ∈ 𝑣 ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 } |