This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( F ( Paths ` G ) P <-> ( F ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ... ( # ` F ) ) ) /\ ( P ` 0 ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ispth 
 |-  ( F ( Paths ` G ) P <-> ( F ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) )
2 istrl 
 |-  ( F ( Trails ` G ) P <-> ( F ( Walks ` G ) P /\ Fun `' F ) )
3 wlkcl 
 |-  ( F ( Walks ` G ) P -> ( # ` F ) e. NN0 )
4 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
5 4 wlkp 
 |-  ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
6 ffn 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> P Fn ( 0 ... ( # ` F ) ) )
7 6 adantl 
 |-  ( ( ( # ` F ) e. NN0 /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) -> P Fn ( 0 ... ( # ` F ) ) )
8 0elfz 
 |-  ( ( # ` F ) e. NN0 -> 0 e. ( 0 ... ( # ` F ) ) )
9 8 adantr 
 |-  ( ( ( # ` F ) e. NN0 /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) -> 0 e. ( 0 ... ( # ` F ) ) )
10 nn0fz0 
 |-  ( ( # ` F ) e. NN0 <-> ( # ` F ) e. ( 0 ... ( # ` F ) ) )
11 10 birani 
 |-  ( ( ( # ` F ) e. NN0 /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) -> ( # ` F ) e. ( 0 ... ( # ` F ) ) )
12 7 9 11 3jca 
 |-  ( ( ( # ` F ) e. NN0 /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) -> ( P Fn ( 0 ... ( # ` F ) ) /\ 0 e. ( 0 ... ( # ` F ) ) /\ ( # ` F ) e. ( 0 ... ( # ` F ) ) ) )
13 3 5 12 syl2anc 
 |-  ( F ( Walks ` G ) P -> ( P Fn ( 0 ... ( # ` F ) ) /\ 0 e. ( 0 ... ( # ` F ) ) /\ ( # ` F ) e. ( 0 ... ( # ` F ) ) ) )
14 13 adantr 
 |-  ( ( F ( Walks ` G ) P /\ Fun `' F ) -> ( P Fn ( 0 ... ( # ` F ) ) /\ 0 e. ( 0 ... ( # ` F ) ) /\ ( # ` F ) e. ( 0 ... ( # ` F ) ) ) )
15 2 14 sylbi 
 |-  ( F ( Trails ` G ) P -> ( P Fn ( 0 ... ( # ` F ) ) /\ 0 e. ( 0 ... ( # ` F ) ) /\ ( # ` F ) e. ( 0 ... ( # ` F ) ) ) )
16 fnimapr 
 |-  ( ( P Fn ( 0 ... ( # ` F ) ) /\ 0 e. ( 0 ... ( # ` F ) ) /\ ( # ` F ) e. ( 0 ... ( # ` F ) ) ) -> ( P " { 0 , ( # ` F ) } ) = { ( P ` 0 ) , ( P ` ( # ` F ) ) } )
17 15 16 syl 
 |-  ( F ( Trails ` G ) P -> ( P " { 0 , ( # ` F ) } ) = { ( P ` 0 ) , ( P ` ( # ` F ) ) } )
18 17 ineq1d 
 |-  ( F ( Trails ` G ) P -> ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = ( { ( P ` 0 ) , ( P ` ( # ` F ) ) } i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) )
19 18 eqeq1d 
 |-  ( F ( Trails ` G ) P -> ( ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) <-> ( { ( P ` 0 ) , ( P ` ( # ` F ) ) } i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) )
20 disj 
 |-  ( ( { ( P ` 0 ) , ( P ` ( # ` F ) ) } i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) <-> A. x e. { ( P ` 0 ) , ( P ` ( # ` F ) ) } -. x e. ( P " ( 1 ..^ ( # ` F ) ) ) )
21 fvex 
 |-  ( P ` 0 ) e. _V
22 fvex 
 |-  ( P ` ( # ` F ) ) e. _V
23 eleq1 
 |-  ( x = ( P ` 0 ) -> ( x e. ( P " ( 1 ..^ ( # ` F ) ) ) <-> ( P ` 0 ) e. ( P " ( 1 ..^ ( # ` F ) ) ) ) )
24 23 notbid 
 |-  ( x = ( P ` 0 ) -> ( -. x e. ( P " ( 1 ..^ ( # ` F ) ) ) <-> -. ( P ` 0 ) e. ( P " ( 1 ..^ ( # ` F ) ) ) ) )
25 eleq1 
 |-  ( x = ( P ` ( # ` F ) ) -> ( x e. ( P " ( 1 ..^ ( # ` F ) ) ) <-> ( P ` ( # ` F ) ) e. ( P " ( 1 ..^ ( # ` F ) ) ) ) )
26 25 notbid 
 |-  ( x = ( P ` ( # ` F ) ) -> ( -. x e. ( P " ( 1 ..^ ( # ` F ) ) ) <-> -. ( P ` ( # ` F ) ) e. ( P " ( 1 ..^ ( # ` F ) ) ) ) )
27 21 22 24 26 ralpr 
 |-  ( A. x e. { ( P ` 0 ) , ( P ` ( # ` F ) ) } -. x e. ( P " ( 1 ..^ ( # ` F ) ) ) <-> ( -. ( P ` 0 ) e. ( P " ( 1 ..^ ( # ` F ) ) ) /\ -. ( P ` ( # ` F ) ) e. ( P " ( 1 ..^ ( # ` F ) ) ) ) )
28 df-nel 
 |-  ( ( P ` 0 ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) <-> -. ( P ` 0 ) e. ( P " ( 1 ..^ ( # ` F ) ) ) )
29 28 bicomi 
 |-  ( -. ( P ` 0 ) e. ( P " ( 1 ..^ ( # ` F ) ) ) <-> ( P ` 0 ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) )
30 27 29 bianbi 
 |-  ( A. x e. { ( P ` 0 ) , ( P ` ( # ` F ) ) } -. x e. ( P " ( 1 ..^ ( # ` F ) ) ) <-> ( ( P ` 0 ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) /\ -. ( P ` ( # ` F ) ) e. ( P " ( 1 ..^ ( # ` F ) ) ) ) )
31 20 30 bitri 
 |-  ( ( { ( P ` 0 ) , ( P ` ( # ` F ) ) } i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) <-> ( ( P ` 0 ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) /\ -. ( P ` ( # ` F ) ) e. ( P " ( 1 ..^ ( # ` F ) ) ) ) )
32 19 31 bitrdi 
 |-  ( F ( Trails ` G ) P -> ( ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) <-> ( ( P ` 0 ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) /\ -. ( P ` ( # ` F ) ) e. ( P " ( 1 ..^ ( # ` F ) ) ) ) ) )
33 32 anbi2d 
 |-  ( F ( Trails ` G ) P -> ( ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) <-> ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P ` 0 ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) /\ -. ( P ` ( # ` F ) ) e. ( P " ( 1 ..^ ( # ` F ) ) ) ) ) ) )
34 ancom 
 |-  ( ( ( P ` 0 ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) /\ -. ( P ` ( # ` F ) ) e. ( P " ( 1 ..^ ( # ` F ) ) ) ) <-> ( -. ( P ` ( # ` F ) ) e. ( P " ( 1 ..^ ( # ` F ) ) ) /\ ( P ` 0 ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) ) )
35 34 bianass 
 |-  ( ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P ` 0 ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) /\ -. ( P ` ( # ` F ) ) e. ( P " ( 1 ..^ ( # ` F ) ) ) ) ) <-> ( ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ -. ( P ` ( # ` F ) ) e. ( P " ( 1 ..^ ( # ` F ) ) ) ) /\ ( P ` 0 ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) ) )
36 35 a1i 
 |-  ( F ( Trails ` G ) P -> ( ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P ` 0 ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) /\ -. ( P ` ( # ` F ) ) e. ( P " ( 1 ..^ ( # ` F ) ) ) ) ) <-> ( ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ -. ( P ` ( # ` F ) ) e. ( P " ( 1 ..^ ( # ` F ) ) ) ) /\ ( P ` 0 ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) ) ) )
37 noel 
 |-  -. ( P ` ( # ` F ) ) e. (/)
38 37 biantru 
 |-  ( Fun `' ( P |` (/) ) <-> ( Fun `' ( P |` (/) ) /\ -. ( P ` ( # ` F ) ) e. (/) ) )
39 38 bicomi 
 |-  ( ( Fun `' ( P |` (/) ) /\ -. ( P ` ( # ` F ) ) e. (/) ) <-> Fun `' ( P |` (/) ) )
40 39 a1i 
 |-  ( ( # ` F ) = 0 -> ( ( Fun `' ( P |` (/) ) /\ -. ( P ` ( # ` F ) ) e. (/) ) <-> Fun `' ( P |` (/) ) ) )
41 oveq2 
 |-  ( ( # ` F ) = 0 -> ( 1 ..^ ( # ` F ) ) = ( 1 ..^ 0 ) )
42 0le1 
 |-  0 <_ 1
43 1z 
 |-  1 e. ZZ
44 0z 
 |-  0 e. ZZ
45 fzon 
 |-  ( ( 1 e. ZZ /\ 0 e. ZZ ) -> ( 0 <_ 1 <-> ( 1 ..^ 0 ) = (/) ) )
46 43 44 45 mp2an 
 |-  ( 0 <_ 1 <-> ( 1 ..^ 0 ) = (/) )
47 42 46 mpbi 
 |-  ( 1 ..^ 0 ) = (/)
48 41 47 eqtrdi 
 |-  ( ( # ` F ) = 0 -> ( 1 ..^ ( # ` F ) ) = (/) )
49 48 reseq2d 
 |-  ( ( # ` F ) = 0 -> ( P |` ( 1 ..^ ( # ` F ) ) ) = ( P |` (/) ) )
50 49 cnveqd 
 |-  ( ( # ` F ) = 0 -> `' ( P |` ( 1 ..^ ( # ` F ) ) ) = `' ( P |` (/) ) )
51 50 funeqd 
 |-  ( ( # ` F ) = 0 -> ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) <-> Fun `' ( P |` (/) ) ) )
52 48 imaeq2d 
 |-  ( ( # ` F ) = 0 -> ( P " ( 1 ..^ ( # ` F ) ) ) = ( P " (/) ) )
53 ima0 
 |-  ( P " (/) ) = (/)
54 52 53 eqtrdi 
 |-  ( ( # ` F ) = 0 -> ( P " ( 1 ..^ ( # ` F ) ) ) = (/) )
55 54 eleq2d 
 |-  ( ( # ` F ) = 0 -> ( ( P ` ( # ` F ) ) e. ( P " ( 1 ..^ ( # ` F ) ) ) <-> ( P ` ( # ` F ) ) e. (/) ) )
56 55 notbid 
 |-  ( ( # ` F ) = 0 -> ( -. ( P ` ( # ` F ) ) e. ( P " ( 1 ..^ ( # ` F ) ) ) <-> -. ( P ` ( # ` F ) ) e. (/) ) )
57 51 56 anbi12d 
 |-  ( ( # ` F ) = 0 -> ( ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ -. ( P ` ( # ` F ) ) e. ( P " ( 1 ..^ ( # ` F ) ) ) ) <-> ( Fun `' ( P |` (/) ) /\ -. ( P ` ( # ` F ) ) e. (/) ) ) )
58 oveq2 
 |-  ( ( # ` F ) = 0 -> ( 1 ... ( # ` F ) ) = ( 1 ... 0 ) )
59 fz10 
 |-  ( 1 ... 0 ) = (/)
60 58 59 eqtrdi 
 |-  ( ( # ` F ) = 0 -> ( 1 ... ( # ` F ) ) = (/) )
61 60 reseq2d 
 |-  ( ( # ` F ) = 0 -> ( P |` ( 1 ... ( # ` F ) ) ) = ( P |` (/) ) )
62 61 cnveqd 
 |-  ( ( # ` F ) = 0 -> `' ( P |` ( 1 ... ( # ` F ) ) ) = `' ( P |` (/) ) )
63 62 funeqd 
 |-  ( ( # ` F ) = 0 -> ( Fun `' ( P |` ( 1 ... ( # ` F ) ) ) <-> Fun `' ( P |` (/) ) ) )
64 40 57 63 3bitr4d 
 |-  ( ( # ` F ) = 0 -> ( ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ -. ( P ` ( # ` F ) ) e. ( P " ( 1 ..^ ( # ` F ) ) ) ) <-> Fun `' ( P |` ( 1 ... ( # ` F ) ) ) ) )
65 64 a1d 
 |-  ( ( # ` F ) = 0 -> ( F ( Trails ` G ) P -> ( ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ -. ( P ` ( # ` F ) ) e. ( P " ( 1 ..^ ( # ` F ) ) ) ) <-> Fun `' ( P |` ( 1 ... ( # ` F ) ) ) ) ) )
66 df-nel 
 |-  ( ( P ` ( # ` F ) ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) <-> -. ( P ` ( # ` F ) ) e. ( P " ( 1 ..^ ( # ` F ) ) ) )
67 66 bicomi 
 |-  ( -. ( P ` ( # ` F ) ) e. ( P " ( 1 ..^ ( # ` F ) ) ) <-> ( P ` ( # ` F ) ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) )
68 67 anbi2i 
 |-  ( ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ -. ( P ` ( # ` F ) ) e. ( P " ( 1 ..^ ( # ` F ) ) ) ) <-> ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( P ` ( # ` F ) ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) ) )
69 trliswlk 
 |-  ( F ( Trails ` G ) P -> F ( Walks ` G ) P )
70 3 10 sylib 
 |-  ( F ( Walks ` G ) P -> ( # ` F ) e. ( 0 ... ( # ` F ) ) )
71 fzonel 
 |-  -. ( # ` F ) e. ( 1 ..^ ( # ` F ) )
72 71 a1i 
 |-  ( F ( Walks ` G ) P -> -. ( # ` F ) e. ( 1 ..^ ( # ` F ) ) )
73 70 72 eldifd 
 |-  ( F ( Walks ` G ) P -> ( # ` F ) e. ( ( 0 ... ( # ` F ) ) \ ( 1 ..^ ( # ` F ) ) ) )
74 1eluzge0 
 |-  1 e. ( ZZ>= ` 0 )
75 fzoss1 
 |-  ( 1 e. ( ZZ>= ` 0 ) -> ( 1 ..^ ( # ` F ) ) C_ ( 0 ..^ ( # ` F ) ) )
76 74 75 mp1i 
 |-  ( F ( Walks ` G ) P -> ( 1 ..^ ( # ` F ) ) C_ ( 0 ..^ ( # ` F ) ) )
77 fzossfz 
 |-  ( 0 ..^ ( # ` F ) ) C_ ( 0 ... ( # ` F ) )
78 76 77 sstrdi 
 |-  ( F ( Walks ` G ) P -> ( 1 ..^ ( # ` F ) ) C_ ( 0 ... ( # ` F ) ) )
79 5 73 78 3jca 
 |-  ( F ( Walks ` G ) P -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( # ` F ) e. ( ( 0 ... ( # ` F ) ) \ ( 1 ..^ ( # ` F ) ) ) /\ ( 1 ..^ ( # ` F ) ) C_ ( 0 ... ( # ` F ) ) ) )
80 resf1ext2b 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( # ` F ) e. ( ( 0 ... ( # ` F ) ) \ ( 1 ..^ ( # ` F ) ) ) /\ ( 1 ..^ ( # ` F ) ) C_ ( 0 ... ( # ` F ) ) ) -> ( ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( P ` ( # ` F ) ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) ) <-> Fun `' ( P |` ( ( 1 ..^ ( # ` F ) ) u. { ( # ` F ) } ) ) ) )
81 69 79 80 3syl 
 |-  ( F ( Trails ` G ) P -> ( ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( P ` ( # ` F ) ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) ) <-> Fun `' ( P |` ( ( 1 ..^ ( # ` F ) ) u. { ( # ` F ) } ) ) ) )
82 68 81 bitrid 
 |-  ( F ( Trails ` G ) P -> ( ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ -. ( P ` ( # ` F ) ) e. ( P " ( 1 ..^ ( # ` F ) ) ) ) <-> Fun `' ( P |` ( ( 1 ..^ ( # ` F ) ) u. { ( # ` F ) } ) ) ) )
83 82 adantl 
 |-  ( ( ( # ` F ) =/= 0 /\ F ( Trails ` G ) P ) -> ( ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ -. ( P ` ( # ` F ) ) e. ( P " ( 1 ..^ ( # ` F ) ) ) ) <-> Fun `' ( P |` ( ( 1 ..^ ( # ` F ) ) u. { ( # ` F ) } ) ) ) )
84 elnnne0 
 |-  ( ( # ` F ) e. NN <-> ( ( # ` F ) e. NN0 /\ ( # ` F ) =/= 0 ) )
85 elnnuz 
 |-  ( ( # ` F ) e. NN <-> ( # ` F ) e. ( ZZ>= ` 1 ) )
86 84 85 sylbb1 
 |-  ( ( ( # ` F ) e. NN0 /\ ( # ` F ) =/= 0 ) -> ( # ` F ) e. ( ZZ>= ` 1 ) )
87 86 ex 
 |-  ( ( # ` F ) e. NN0 -> ( ( # ` F ) =/= 0 -> ( # ` F ) e. ( ZZ>= ` 1 ) ) )
88 69 3 87 3syl 
 |-  ( F ( Trails ` G ) P -> ( ( # ` F ) =/= 0 -> ( # ` F ) e. ( ZZ>= ` 1 ) ) )
89 88 impcom 
 |-  ( ( ( # ` F ) =/= 0 /\ F ( Trails ` G ) P ) -> ( # ` F ) e. ( ZZ>= ` 1 ) )
90 fzisfzounsn 
 |-  ( ( # ` F ) e. ( ZZ>= ` 1 ) -> ( 1 ... ( # ` F ) ) = ( ( 1 ..^ ( # ` F ) ) u. { ( # ` F ) } ) )
91 89 90 syl 
 |-  ( ( ( # ` F ) =/= 0 /\ F ( Trails ` G ) P ) -> ( 1 ... ( # ` F ) ) = ( ( 1 ..^ ( # ` F ) ) u. { ( # ` F ) } ) )
92 91 eqcomd 
 |-  ( ( ( # ` F ) =/= 0 /\ F ( Trails ` G ) P ) -> ( ( 1 ..^ ( # ` F ) ) u. { ( # ` F ) } ) = ( 1 ... ( # ` F ) ) )
93 92 reseq2d 
 |-  ( ( ( # ` F ) =/= 0 /\ F ( Trails ` G ) P ) -> ( P |` ( ( 1 ..^ ( # ` F ) ) u. { ( # ` F ) } ) ) = ( P |` ( 1 ... ( # ` F ) ) ) )
94 93 cnveqd 
 |-  ( ( ( # ` F ) =/= 0 /\ F ( Trails ` G ) P ) -> `' ( P |` ( ( 1 ..^ ( # ` F ) ) u. { ( # ` F ) } ) ) = `' ( P |` ( 1 ... ( # ` F ) ) ) )
95 94 funeqd 
 |-  ( ( ( # ` F ) =/= 0 /\ F ( Trails ` G ) P ) -> ( Fun `' ( P |` ( ( 1 ..^ ( # ` F ) ) u. { ( # ` F ) } ) ) <-> Fun `' ( P |` ( 1 ... ( # ` F ) ) ) ) )
96 83 95 bitrd 
 |-  ( ( ( # ` F ) =/= 0 /\ F ( Trails ` G ) P ) -> ( ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ -. ( P ` ( # ` F ) ) e. ( P " ( 1 ..^ ( # ` F ) ) ) ) <-> Fun `' ( P |` ( 1 ... ( # ` F ) ) ) ) )
97 96 ex 
 |-  ( ( # ` F ) =/= 0 -> ( F ( Trails ` G ) P -> ( ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ -. ( P ` ( # ` F ) ) e. ( P " ( 1 ..^ ( # ` F ) ) ) ) <-> Fun `' ( P |` ( 1 ... ( # ` F ) ) ) ) ) )
98 65 97 pm2.61ine 
 |-  ( F ( Trails ` G ) P -> ( ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ -. ( P ` ( # ` F ) ) e. ( P " ( 1 ..^ ( # ` F ) ) ) ) <-> Fun `' ( P |` ( 1 ... ( # ` F ) ) ) ) )
99 98 anbi1d 
 |-  ( F ( Trails ` G ) P -> ( ( ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ -. ( P ` ( # ` F ) ) e. ( P " ( 1 ..^ ( # ` F ) ) ) ) /\ ( P ` 0 ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) ) <-> ( Fun `' ( P |` ( 1 ... ( # ` F ) ) ) /\ ( P ` 0 ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) ) ) )
100 33 36 99 3bitrd 
 |-  ( F ( Trails ` G ) P -> ( ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) <-> ( Fun `' ( P |` ( 1 ... ( # ` F ) ) ) /\ ( P ` 0 ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) ) ) )
101 100 pm5.32i 
 |-  ( ( F ( Trails ` G ) P /\ ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) ) <-> ( F ( Trails ` G ) P /\ ( Fun `' ( P |` ( 1 ... ( # ` F ) ) ) /\ ( P ` 0 ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) ) ) )
102 3anass 
 |-  ( ( F ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) <-> ( F ( Trails ` G ) P /\ ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) ) )
103 3anass 
 |-  ( ( F ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ... ( # ` F ) ) ) /\ ( P ` 0 ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) ) <-> ( F ( Trails ` G ) P /\ ( Fun `' ( P |` ( 1 ... ( # ` F ) ) ) /\ ( P ` 0 ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) ) ) )
104 101 102 103 3bitr4i 
 |-  ( ( F ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) <-> ( F ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ... ( # ` F ) ) ) /\ ( P ` 0 ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) ) )
105 1 104 bitri 
 |-  ( F ( Paths ` G ) P <-> ( F ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ... ( # ` F ) ) ) /\ ( P ` 0 ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) ) )