Step |
Hyp |
Ref |
Expression |
1 |
|
0pth.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
ispth |
⊢ ( ∅ ( Paths ‘ 𝐺 ) 𝑃 ↔ ( ∅ ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ ∅ ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ) = ∅ ) ) |
3 |
2
|
a1i |
⊢ ( 𝐺 ∈ 𝑊 → ( ∅ ( Paths ‘ 𝐺 ) 𝑃 ↔ ( ∅ ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ ∅ ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ) = ∅ ) ) ) |
4 |
|
3anass |
⊢ ( ( ∅ ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ ∅ ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ) = ∅ ) ↔ ( ∅ ( Trails ‘ 𝐺 ) 𝑃 ∧ ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ ∅ ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ) = ∅ ) ) ) |
5 |
4
|
a1i |
⊢ ( 𝐺 ∈ 𝑊 → ( ( ∅ ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ ∅ ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ) = ∅ ) ↔ ( ∅ ( Trails ‘ 𝐺 ) 𝑃 ∧ ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ ∅ ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ) = ∅ ) ) ) ) |
6 |
|
funcnv0 |
⊢ Fun ◡ ∅ |
7 |
|
hash0 |
⊢ ( ♯ ‘ ∅ ) = 0 |
8 |
|
0le1 |
⊢ 0 ≤ 1 |
9 |
7 8
|
eqbrtri |
⊢ ( ♯ ‘ ∅ ) ≤ 1 |
10 |
|
1z |
⊢ 1 ∈ ℤ |
11 |
|
0z |
⊢ 0 ∈ ℤ |
12 |
7 11
|
eqeltri |
⊢ ( ♯ ‘ ∅ ) ∈ ℤ |
13 |
|
fzon |
⊢ ( ( 1 ∈ ℤ ∧ ( ♯ ‘ ∅ ) ∈ ℤ ) → ( ( ♯ ‘ ∅ ) ≤ 1 ↔ ( 1 ..^ ( ♯ ‘ ∅ ) ) = ∅ ) ) |
14 |
10 12 13
|
mp2an |
⊢ ( ( ♯ ‘ ∅ ) ≤ 1 ↔ ( 1 ..^ ( ♯ ‘ ∅ ) ) = ∅ ) |
15 |
9 14
|
mpbi |
⊢ ( 1 ..^ ( ♯ ‘ ∅ ) ) = ∅ |
16 |
15
|
reseq2i |
⊢ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) = ( 𝑃 ↾ ∅ ) |
17 |
|
res0 |
⊢ ( 𝑃 ↾ ∅ ) = ∅ |
18 |
16 17
|
eqtri |
⊢ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) = ∅ |
19 |
18
|
cnveqi |
⊢ ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) = ◡ ∅ |
20 |
19
|
funeqi |
⊢ ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ↔ Fun ◡ ∅ ) |
21 |
6 20
|
mpbir |
⊢ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) |
22 |
15
|
imaeq2i |
⊢ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) = ( 𝑃 “ ∅ ) |
23 |
|
ima0 |
⊢ ( 𝑃 “ ∅ ) = ∅ |
24 |
22 23
|
eqtri |
⊢ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) = ∅ |
25 |
24
|
ineq2i |
⊢ ( ( 𝑃 “ { 0 , ( ♯ ‘ ∅ ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ) = ( ( 𝑃 “ { 0 , ( ♯ ‘ ∅ ) } ) ∩ ∅ ) |
26 |
|
in0 |
⊢ ( ( 𝑃 “ { 0 , ( ♯ ‘ ∅ ) } ) ∩ ∅ ) = ∅ |
27 |
25 26
|
eqtri |
⊢ ( ( 𝑃 “ { 0 , ( ♯ ‘ ∅ ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ) = ∅ |
28 |
21 27
|
pm3.2i |
⊢ ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ ∅ ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ) = ∅ ) |
29 |
28
|
biantru |
⊢ ( ∅ ( Trails ‘ 𝐺 ) 𝑃 ↔ ( ∅ ( Trails ‘ 𝐺 ) 𝑃 ∧ ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ ∅ ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ) = ∅ ) ) ) |
30 |
5 29
|
bitr4di |
⊢ ( 𝐺 ∈ 𝑊 → ( ( ∅ ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ ∅ ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ) = ∅ ) ↔ ∅ ( Trails ‘ 𝐺 ) 𝑃 ) ) |
31 |
1
|
0trl |
⊢ ( 𝐺 ∈ 𝑊 → ( ∅ ( Trails ‘ 𝐺 ) 𝑃 ↔ 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ) ) |
32 |
3 30 31
|
3bitrd |
⊢ ( 𝐺 ∈ 𝑊 → ( ∅ ( Paths ‘ 𝐺 ) 𝑃 ↔ 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ) ) |