Metamath Proof Explorer

Theorem dfpth2

Description: Alternate definition for a pair of classes/functions to be a path (in an undirected graph). (Contributed by AV, 4-Oct-2025)

Ref Expression
Assertion dfpth2 ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ... ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝑃 ‘ 0 ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ispth ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) )
2 istrl ⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝐹 ) )
3 wlkcl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
4 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
5 4 wlkp ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
6 ffn ⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → 𝑃 Fn ( 0 ... ( ♯ ‘ 𝐹 ) ) )
7 6 adantl ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → 𝑃 Fn ( 0 ... ( ♯ ‘ 𝐹 ) ) )
8 0elfz ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
9 8 adantr ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
10 nn0fz0 ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝐹 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
11 10 biimpi ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ 𝐹 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
12 11 adantr ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( ♯ ‘ 𝐹 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
13 7 9 12 3jca ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( 𝑃 Fn ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) )
14 3 5 13 syl2anc ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝑃 Fn ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) )
15 14 adantr ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝐹 ) → ( 𝑃 Fn ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) )
16 2 15 sylbi ⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ( 𝑃 Fn ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) )
17 fnimapr ⊢ ( ( 𝑃 Fn ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } )
18 16 17 syl ⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } )
19 18 ineq1d ⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
20 19 eqeq1d ⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ( ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ↔ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) )
21 disj ⊢ ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ↔ ∀ 𝑥 ∈ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ¬ 𝑥 ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
22 fvex ⊢ ( 𝑃 ‘ 0 ) ∈ V
23 fvex ⊢ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ V
24 eleq1 ⊢ ( 𝑥 = ( 𝑃 ‘ 0 ) → ( 𝑥 ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ↔ ( 𝑃 ‘ 0 ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
25 24 notbid ⊢ ( 𝑥 = ( 𝑃 ‘ 0 ) → ( ¬ 𝑥 ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ↔ ¬ ( 𝑃 ‘ 0 ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
26 eleq1 ⊢ ( 𝑥 = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → ( 𝑥 ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ↔ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
27 26 notbid ⊢ ( 𝑥 = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → ( ¬ 𝑥 ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ↔ ¬ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
28 22 23 25 27 ralpr ⊢ ( ∀ 𝑥 ∈ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ¬ 𝑥 ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ↔ ( ¬ ( 𝑃 ‘ 0 ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ¬ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
29 df-nel ⊢ ( ( 𝑃 ‘ 0 ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ↔ ¬ ( 𝑃 ‘ 0 ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
30 29 bicomi ⊢ ( ¬ ( 𝑃 ‘ 0 ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ↔ ( 𝑃 ‘ 0 ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
31 28 30 bianbi ⊢ ( ∀ 𝑥 ∈ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ¬ 𝑥 ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ↔ ( ( 𝑃 ‘ 0 ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ¬ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
32 21 31 bitri ⊢ ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ↔ ( ( 𝑃 ‘ 0 ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ¬ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
33 20 32 bitrdi ⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ( ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ↔ ( ( 𝑃 ‘ 0 ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ¬ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ) )
34 33 anbi2d ⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ( ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) ↔ ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 ‘ 0 ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ¬ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ) ) )
35 ancom ⊢ ( ( ( 𝑃 ‘ 0 ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ¬ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ↔ ( ¬ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝑃 ‘ 0 ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
36 35 bianass ⊢ ( ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 ‘ 0 ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ¬ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ) ↔ ( ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ¬ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ∧ ( 𝑃 ‘ 0 ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
37 36 a1i ⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ( ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 ‘ 0 ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ¬ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ) ↔ ( ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ¬ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ∧ ( 𝑃 ‘ 0 ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ) )
38 noel ⊢ ¬ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ∅
39 38 biantru ⊢ ( Fun ◡ ( 𝑃 ↾ ∅ ) ↔ ( Fun ◡ ( 𝑃 ↾ ∅ ) ∧ ¬ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ∅ ) )
40 39 bicomi ⊢ ( ( Fun ◡ ( 𝑃 ↾ ∅ ) ∧ ¬ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ∅ ) ↔ Fun ◡ ( 𝑃 ↾ ∅ ) )
41 40 a1i ⊢ ( ( ♯ ‘ 𝐹 ) = 0 → ( ( Fun ◡ ( 𝑃 ↾ ∅ ) ∧ ¬ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ∅ ) ↔ Fun ◡ ( 𝑃 ↾ ∅ ) ) )
42 oveq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 0 → ( 1 ..^ ( ♯ ‘ 𝐹 ) ) = ( 1 ..^ 0 ) )
43 0le1 ⊢ 0 ≤ 1
44 1z ⊢ 1 ∈ ℤ
45 0z ⊢ 0 ∈ ℤ
46 fzon ⊢ ( ( 1 ∈ ℤ ∧ 0 ∈ ℤ ) → ( 0 ≤ 1 ↔ ( 1 ..^ 0 ) = ∅ ) )
47 44 45 46 mp2an ⊢ ( 0 ≤ 1 ↔ ( 1 ..^ 0 ) = ∅ )
48 43 47 mpbi ⊢ ( 1 ..^ 0 ) = ∅
49 42 48 eqtrdi ⊢ ( ( ♯ ‘ 𝐹 ) = 0 → ( 1 ..^ ( ♯ ‘ 𝐹 ) ) = ∅ )
50 49 reseq2d ⊢ ( ( ♯ ‘ 𝐹 ) = 0 → ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) = ( 𝑃 ↾ ∅ ) )
51 50 cnveqd ⊢ ( ( ♯ ‘ 𝐹 ) = 0 → ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) = ◡ ( 𝑃 ↾ ∅ ) )
52 51 funeqd ⊢ ( ( ♯ ‘ 𝐹 ) = 0 → ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ↔ Fun ◡ ( 𝑃 ↾ ∅ ) ) )
53 49 imaeq2d ⊢ ( ( ♯ ‘ 𝐹 ) = 0 → ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) = ( 𝑃 “ ∅ ) )
54 ima0 ⊢ ( 𝑃 “ ∅ ) = ∅
55 53 54 eqtrdi ⊢ ( ( ♯ ‘ 𝐹 ) = 0 → ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) = ∅ )
56 55 eleq2d ⊢ ( ( ♯ ‘ 𝐹 ) = 0 → ( ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ↔ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ∅ ) )
57 56 notbid ⊢ ( ( ♯ ‘ 𝐹 ) = 0 → ( ¬ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ↔ ¬ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ∅ ) )
58 52 57 anbi12d ⊢ ( ( ♯ ‘ 𝐹 ) = 0 → ( ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ¬ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ↔ ( Fun ◡ ( 𝑃 ↾ ∅ ) ∧ ¬ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ∅ ) ) )
59 oveq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 0 → ( 1 ... ( ♯ ‘ 𝐹 ) ) = ( 1 ... 0 ) )
60 fz10 ⊢ ( 1 ... 0 ) = ∅
61 59 60 eqtrdi ⊢ ( ( ♯ ‘ 𝐹 ) = 0 → ( 1 ... ( ♯ ‘ 𝐹 ) ) = ∅ )
62 61 reseq2d ⊢ ( ( ♯ ‘ 𝐹 ) = 0 → ( 𝑃 ↾ ( 1 ... ( ♯ ‘ 𝐹 ) ) ) = ( 𝑃 ↾ ∅ ) )
63 62 cnveqd ⊢ ( ( ♯ ‘ 𝐹 ) = 0 → ◡ ( 𝑃 ↾ ( 1 ... ( ♯ ‘ 𝐹 ) ) ) = ◡ ( 𝑃 ↾ ∅ ) )
64 63 funeqd ⊢ ( ( ♯ ‘ 𝐹 ) = 0 → ( Fun ◡ ( 𝑃 ↾ ( 1 ... ( ♯ ‘ 𝐹 ) ) ) ↔ Fun ◡ ( 𝑃 ↾ ∅ ) ) )
65 41 58 64 3bitr4d ⊢ ( ( ♯ ‘ 𝐹 ) = 0 → ( ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ¬ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ↔ Fun ◡ ( 𝑃 ↾ ( 1 ... ( ♯ ‘ 𝐹 ) ) ) ) )
66 65 a1d ⊢ ( ( ♯ ‘ 𝐹 ) = 0 → ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ( ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ¬ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ↔ Fun ◡ ( 𝑃 ↾ ( 1 ... ( ♯ ‘ 𝐹 ) ) ) ) ) )
67 df-nel ⊢ ( ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ↔ ¬ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
68 67 bicomi ⊢ ( ¬ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ↔ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
69 68 anbi2i ⊢ ( ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ¬ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ↔ ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
70 trliswlk ⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
71 3 10 sylib ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
72 fzonel ⊢ ¬ ( ♯ ‘ 𝐹 ) ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) )
73 72 a1i ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ¬ ( ♯ ‘ 𝐹 ) ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) )
74 71 73 eldifd ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ( ( 0 ... ( ♯ ‘ 𝐹 ) ) ∖ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
75 1eluzge0 ⊢ 1 ∈ ( ℤ≥ ‘ 0 )
76 fzoss1 ⊢ ( 1 ∈ ( ℤ≥ ‘ 0 ) → ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
77 75 76 mp1i ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
78 fzossfz ⊢ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝐹 ) )
79 77 78 sstrdi ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
80 5 74 79 3jca ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ( ( 0 ... ( ♯ ‘ 𝐹 ) ) ∖ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) )
81 resf1ext2b ⊢ ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ( ( 0 ... ( ♯ ‘ 𝐹 ) ) ∖ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ↔ Fun ◡ ( 𝑃 ↾ ( ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∪ { ( ♯ ‘ 𝐹 ) } ) ) ) )
82 70 80 81 3syl ⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ( ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ↔ Fun ◡ ( 𝑃 ↾ ( ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∪ { ( ♯ ‘ 𝐹 ) } ) ) ) )
83 69 82 bitrid ⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ( ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ¬ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ↔ Fun ◡ ( 𝑃 ↾ ( ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∪ { ( ♯ ‘ 𝐹 ) } ) ) ) )
84 83 adantl ⊢ ( ( ( ♯ ‘ 𝐹 ) ≠ 0 ∧ 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) → ( ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ¬ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ↔ Fun ◡ ( 𝑃 ↾ ( ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∪ { ( ♯ ‘ 𝐹 ) } ) ) ) )
85 elnnne0 ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ≠ 0 ) )
86 elnnuz ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ ↔ ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ 1 ) )
87 85 86 sylbb1 ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ≠ 0 ) → ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ 1 ) )
88 87 ex ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ( ♯ ‘ 𝐹 ) ≠ 0 → ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ 1 ) ) )
89 70 3 88 3syl ⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ( ( ♯ ‘ 𝐹 ) ≠ 0 → ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ 1 ) ) )
90 89 impcom ⊢ ( ( ( ♯ ‘ 𝐹 ) ≠ 0 ∧ 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) → ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ 1 ) )
91 fzisfzounsn ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ 1 ) → ( 1 ... ( ♯ ‘ 𝐹 ) ) = ( ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∪ { ( ♯ ‘ 𝐹 ) } ) )
92 90 91 syl ⊢ ( ( ( ♯ ‘ 𝐹 ) ≠ 0 ∧ 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) → ( 1 ... ( ♯ ‘ 𝐹 ) ) = ( ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∪ { ( ♯ ‘ 𝐹 ) } ) )
93 92 eqcomd ⊢ ( ( ( ♯ ‘ 𝐹 ) ≠ 0 ∧ 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) → ( ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∪ { ( ♯ ‘ 𝐹 ) } ) = ( 1 ... ( ♯ ‘ 𝐹 ) ) )
94 93 reseq2d ⊢ ( ( ( ♯ ‘ 𝐹 ) ≠ 0 ∧ 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) → ( 𝑃 ↾ ( ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∪ { ( ♯ ‘ 𝐹 ) } ) ) = ( 𝑃 ↾ ( 1 ... ( ♯ ‘ 𝐹 ) ) ) )
95 94 cnveqd ⊢ ( ( ( ♯ ‘ 𝐹 ) ≠ 0 ∧ 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) → ◡ ( 𝑃 ↾ ( ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∪ { ( ♯ ‘ 𝐹 ) } ) ) = ◡ ( 𝑃 ↾ ( 1 ... ( ♯ ‘ 𝐹 ) ) ) )
96 95 funeqd ⊢ ( ( ( ♯ ‘ 𝐹 ) ≠ 0 ∧ 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) → ( Fun ◡ ( 𝑃 ↾ ( ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∪ { ( ♯ ‘ 𝐹 ) } ) ) ↔ Fun ◡ ( 𝑃 ↾ ( 1 ... ( ♯ ‘ 𝐹 ) ) ) ) )
97 84 96 bitrd ⊢ ( ( ( ♯ ‘ 𝐹 ) ≠ 0 ∧ 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) → ( ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ¬ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ↔ Fun ◡ ( 𝑃 ↾ ( 1 ... ( ♯ ‘ 𝐹 ) ) ) ) )
98 97 ex ⊢ ( ( ♯ ‘ 𝐹 ) ≠ 0 → ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ( ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ¬ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ↔ Fun ◡ ( 𝑃 ↾ ( 1 ... ( ♯ ‘ 𝐹 ) ) ) ) ) )
99 66 98 pm2.61ine ⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ( ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ¬ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ↔ Fun ◡ ( 𝑃 ↾ ( 1 ... ( ♯ ‘ 𝐹 ) ) ) ) )
100 99 anbi1d ⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ( ( ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ¬ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ∧ ( 𝑃 ‘ 0 ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ↔ ( Fun ◡ ( 𝑃 ↾ ( 1 ... ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝑃 ‘ 0 ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ) )
101 34 37 100 3bitrd ⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ( ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) ↔ ( Fun ◡ ( 𝑃 ↾ ( 1 ... ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝑃 ‘ 0 ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ) )
102 101 pm5.32i ⊢ ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) ) ↔ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ ( Fun ◡ ( 𝑃 ↾ ( 1 ... ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝑃 ‘ 0 ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ) )
103 3anass ⊢ ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) ↔ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) ) )
104 3anass ⊢ ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ... ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝑃 ‘ 0 ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ↔ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ ( Fun ◡ ( 𝑃 ↾ ( 1 ... ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝑃 ‘ 0 ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ) )
105 102 103 104 3bitr4i ⊢ ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) ↔ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ... ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝑃 ‘ 0 ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
106 1 105 bitri ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ... ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝑃 ‘ 0 ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )