| Step |
Hyp |
Ref |
Expression |
| 1 |
|
0pthon.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
| 2 |
1
|
0trlon |
⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ∅ ( 𝑁 ( TrailsOn ‘ 𝐺 ) 𝑁 ) 𝑃 ) |
| 3 |
|
simpl |
⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ) |
| 4 |
|
id |
⊢ ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 → 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ) |
| 5 |
|
0z |
⊢ 0 ∈ ℤ |
| 6 |
|
elfz3 |
⊢ ( 0 ∈ ℤ → 0 ∈ ( 0 ... 0 ) ) |
| 7 |
5 6
|
mp1i |
⊢ ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 → 0 ∈ ( 0 ... 0 ) ) |
| 8 |
4 7
|
ffvelcdmd |
⊢ ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 → ( 𝑃 ‘ 0 ) ∈ 𝑉 ) |
| 9 |
8
|
adantr |
⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ( 𝑃 ‘ 0 ) ∈ 𝑉 ) |
| 10 |
|
eleq1 |
⊢ ( ( 𝑃 ‘ 0 ) = 𝑁 → ( ( 𝑃 ‘ 0 ) ∈ 𝑉 ↔ 𝑁 ∈ 𝑉 ) ) |
| 11 |
10
|
adantl |
⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ( ( 𝑃 ‘ 0 ) ∈ 𝑉 ↔ 𝑁 ∈ 𝑉 ) ) |
| 12 |
9 11
|
mpbid |
⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → 𝑁 ∈ 𝑉 ) |
| 13 |
1
|
1vgrex |
⊢ ( 𝑁 ∈ 𝑉 → 𝐺 ∈ V ) |
| 14 |
1
|
0pth |
⊢ ( 𝐺 ∈ V → ( ∅ ( Paths ‘ 𝐺 ) 𝑃 ↔ 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ) ) |
| 15 |
12 13 14
|
3syl |
⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ( ∅ ( Paths ‘ 𝐺 ) 𝑃 ↔ 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ) ) |
| 16 |
3 15
|
mpbird |
⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ∅ ( Paths ‘ 𝐺 ) 𝑃 ) |
| 17 |
1
|
0wlkonlem1 |
⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ( 𝑁 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) |
| 18 |
1
|
0wlkonlem2 |
⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → 𝑃 ∈ ( 𝑉 ↑pm ( 0 ... 0 ) ) ) |
| 19 |
|
0ex |
⊢ ∅ ∈ V |
| 20 |
18 19
|
jctil |
⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ( ∅ ∈ V ∧ 𝑃 ∈ ( 𝑉 ↑pm ( 0 ... 0 ) ) ) ) |
| 21 |
1
|
ispthson |
⊢ ( ( ( 𝑁 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ ( ∅ ∈ V ∧ 𝑃 ∈ ( 𝑉 ↑pm ( 0 ... 0 ) ) ) ) → ( ∅ ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑁 ) 𝑃 ↔ ( ∅ ( 𝑁 ( TrailsOn ‘ 𝐺 ) 𝑁 ) 𝑃 ∧ ∅ ( Paths ‘ 𝐺 ) 𝑃 ) ) ) |
| 22 |
17 20 21
|
syl2anc |
⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ( ∅ ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑁 ) 𝑃 ↔ ( ∅ ( 𝑁 ( TrailsOn ‘ 𝐺 ) 𝑁 ) 𝑃 ∧ ∅ ( Paths ‘ 𝐺 ) 𝑃 ) ) ) |
| 23 |
2 16 22
|
mpbir2and |
⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ∅ ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑁 ) 𝑃 ) |