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