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
|
ffvelrnd |
⊢ ( 𝑃 : ( 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 ‘ 𝐺 ) 𝑁 ) 𝑃 ) |