Step |
Hyp |
Ref |
Expression |
1 |
|
0pthon.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
0ex |
⊢ ∅ ∈ V |
3 |
|
snex |
⊢ { 〈 0 , 𝑁 〉 } ∈ V |
4 |
2 3
|
pm3.2i |
⊢ ( ∅ ∈ V ∧ { 〈 0 , 𝑁 〉 } ∈ V ) |
5 |
1
|
0pthon1 |
⊢ ( 𝑁 ∈ 𝑉 → ∅ ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑁 ) { 〈 0 , 𝑁 〉 } ) |
6 |
|
breq12 |
⊢ ( ( 𝑓 = ∅ ∧ 𝑝 = { 〈 0 , 𝑁 〉 } ) → ( 𝑓 ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑁 ) 𝑝 ↔ ∅ ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑁 ) { 〈 0 , 𝑁 〉 } ) ) |
7 |
6
|
spc2egv |
⊢ ( ( ∅ ∈ V ∧ { 〈 0 , 𝑁 〉 } ∈ V ) → ( ∅ ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑁 ) { 〈 0 , 𝑁 〉 } → ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑁 ) 𝑝 ) ) |
8 |
4 5 7
|
mpsyl |
⊢ ( 𝑁 ∈ 𝑉 → ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑁 ) 𝑝 ) |