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