Metamath Proof Explorer

Theorem pthdivtx

Description: The inner vertices of a path are distinct from all other vertices. (Contributed by AV, 5-Feb-2021) (Proof shortened by AV, 31-Oct-2021)

Ref Expression
Assertion pthdivtx 
|- ( ( F ( Paths ` G ) P /\ ( I e. ( 1 ..^ ( # ` F ) ) /\ J e. ( 0 ... ( # ` F ) ) /\ I =/= J ) ) -> ( P ` I ) =/= ( P ` J ) )

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 trliswlk 
 |-  ( F ( Trails ` G ) P -> F ( Walks ` G ) P )
3 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
4 3 wlkp 
 |-  ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
5 elfz0lmr 
 |-  ( J e. ( 0 ... ( # ` F ) ) -> ( J = 0 \/ J e. ( 1 ..^ ( # ` F ) ) \/ J = ( # ` F ) ) )
6 elfzo1 
 |-  ( I e. ( 1 ..^ ( # ` F ) ) <-> ( I e. NN /\ ( # ` F ) e. NN /\ I < ( # ` F ) ) )
7 nnnn0 
 |-  ( ( # ` F ) e. NN -> ( # ` F ) e. NN0 )
8 7 3ad2ant2 
 |-  ( ( I e. NN /\ ( # ` F ) e. NN /\ I < ( # ` F ) ) -> ( # ` F ) e. NN0 )
9 6 8 sylbi 
 |-  ( I e. ( 1 ..^ ( # ` F ) ) -> ( # ` F ) e. NN0 )
10 9 adantl 
 |-  ( ( J = 0 /\ I e. ( 1 ..^ ( # ` F ) ) ) -> ( # ` F ) e. NN0 )
11 fvinim0ffz 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( # ` F ) e. NN0 ) -> ( ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) <-> ( ( P ` 0 ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) /\ ( P ` ( # ` F ) ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) ) ) )
12 10 11 sylan2 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( J = 0 /\ I e. ( 1 ..^ ( # ` F ) ) ) ) -> ( ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) <-> ( ( P ` 0 ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) /\ ( P ` ( # ` F ) ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) ) ) )
13 fveq2 
 |-  ( J = 0 -> ( P ` J ) = ( P ` 0 ) )
14 13 eqeq2d 
 |-  ( J = 0 -> ( ( P ` I ) = ( P ` J ) <-> ( P ` I ) = ( P ` 0 ) ) )
15 14 ad2antrl 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( J = 0 /\ I e. ( 1 ..^ ( # ` F ) ) ) ) -> ( ( P ` I ) = ( P ` J ) <-> ( P ` I ) = ( P ` 0 ) ) )
16 ffun 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> Fun P )
17 16 adantr 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ I e. ( 1 ..^ ( # ` F ) ) ) -> Fun P )
18 fdm 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> dom P = ( 0 ... ( # ` F ) ) )
19 fzo0ss1 
 |-  ( 1 ..^ ( # ` F ) ) C_ ( 0 ..^ ( # ` F ) )
20 fzossfz 
 |-  ( 0 ..^ ( # ` F ) ) C_ ( 0 ... ( # ` F ) )
21 19 20 sstri 
 |-  ( 1 ..^ ( # ` F ) ) C_ ( 0 ... ( # ` F ) )
22 21 sseli 
 |-  ( I e. ( 1 ..^ ( # ` F ) ) -> I e. ( 0 ... ( # ` F ) ) )
23 eleq2 
 |-  ( dom P = ( 0 ... ( # ` F ) ) -> ( I e. dom P <-> I e. ( 0 ... ( # ` F ) ) ) )
24 22 23 syl5ibr 
 |-  ( dom P = ( 0 ... ( # ` F ) ) -> ( I e. ( 1 ..^ ( # ` F ) ) -> I e. dom P ) )
25 18 24 syl 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( I e. ( 1 ..^ ( # ` F ) ) -> I e. dom P ) )
26 25 imp 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ I e. ( 1 ..^ ( # ` F ) ) ) -> I e. dom P )
27 17 26 jca 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ I e. ( 1 ..^ ( # ` F ) ) ) -> ( Fun P /\ I e. dom P ) )
28 27 adantrl 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( J = 0 /\ I e. ( 1 ..^ ( # ` F ) ) ) ) -> ( Fun P /\ I e. dom P ) )
29 simprr 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( J = 0 /\ I e. ( 1 ..^ ( # ` F ) ) ) ) -> I e. ( 1 ..^ ( # ` F ) ) )
30 funfvima 
 |-  ( ( Fun P /\ I e. dom P ) -> ( I e. ( 1 ..^ ( # ` F ) ) -> ( P ` I ) e. ( P " ( 1 ..^ ( # ` F ) ) ) ) )
31 28 29 30 sylc 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( J = 0 /\ I e. ( 1 ..^ ( # ` F ) ) ) ) -> ( P ` I ) e. ( P " ( 1 ..^ ( # ` F ) ) ) )
32 eleq1 
 |-  ( ( P ` I ) = ( P ` 0 ) -> ( ( P ` I ) e. ( P " ( 1 ..^ ( # ` F ) ) ) <-> ( P ` 0 ) e. ( P " ( 1 ..^ ( # ` F ) ) ) ) )
33 31 32 syl5ibcom 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( J = 0 /\ I e. ( 1 ..^ ( # ` F ) ) ) ) -> ( ( P ` I ) = ( P ` 0 ) -> ( P ` 0 ) e. ( P " ( 1 ..^ ( # ` F ) ) ) ) )
34 15 33 sylbid 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( J = 0 /\ I e. ( 1 ..^ ( # ` F ) ) ) ) -> ( ( P ` I ) = ( P ` J ) -> ( P ` 0 ) e. ( P " ( 1 ..^ ( # ` F ) ) ) ) )
35 nnel 
 |-  ( -. ( P ` 0 ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) <-> ( P ` 0 ) e. ( P " ( 1 ..^ ( # ` F ) ) ) )
36 34 35 syl6ibr 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( J = 0 /\ I e. ( 1 ..^ ( # ` F ) ) ) ) -> ( ( P ` I ) = ( P ` J ) -> -. ( P ` 0 ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) ) )
37 36 necon2ad 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( J = 0 /\ I e. ( 1 ..^ ( # ` F ) ) ) ) -> ( ( P ` 0 ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) -> ( P ` I ) =/= ( P ` J ) ) )
38 37 adantrd 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( J = 0 /\ I e. ( 1 ..^ ( # ` F ) ) ) ) -> ( ( ( P ` 0 ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) /\ ( P ` ( # ` F ) ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) ) -> ( P ` I ) =/= ( P ` J ) ) )
39 12 38 sylbid 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( J = 0 /\ I e. ( 1 ..^ ( # ` F ) ) ) ) -> ( ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) -> ( P ` I ) =/= ( P ` J ) ) )
40 39 ex 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( ( J = 0 /\ I e. ( 1 ..^ ( # ` F ) ) ) -> ( ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) -> ( P ` I ) =/= ( P ` J ) ) ) )
41 40 com23 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) -> ( ( J = 0 /\ I e. ( 1 ..^ ( # ` F ) ) ) -> ( P ` I ) =/= ( P ` J ) ) ) )
42 41 a1d 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) -> ( ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) -> ( ( J = 0 /\ I e. ( 1 ..^ ( # ` F ) ) ) -> ( P ` I ) =/= ( P ` J ) ) ) ) )
43 42 3imp 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) -> ( ( J = 0 /\ I e. ( 1 ..^ ( # ` F ) ) ) -> ( P ` I ) =/= ( P ` J ) ) )
44 43 com12 
 |-  ( ( J = 0 /\ I e. ( 1 ..^ ( # ` F ) ) ) -> ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) -> ( P ` I ) =/= ( P ` J ) ) )
45 44 a1d 
 |-  ( ( J = 0 /\ I e. ( 1 ..^ ( # ` F ) ) ) -> ( I =/= J -> ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) -> ( P ` I ) =/= ( P ` J ) ) ) )
46 45 ex 
 |-  ( J = 0 -> ( I e. ( 1 ..^ ( # ` F ) ) -> ( I =/= J -> ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) -> ( P ` I ) =/= ( P ` J ) ) ) ) )
47 fvres 
 |-  ( I e. ( 1 ..^ ( # ` F ) ) -> ( ( P |` ( 1 ..^ ( # ` F ) ) ) ` I ) = ( P ` I ) )
48 47 adantl 
 |-  ( ( J e. ( 1 ..^ ( # ` F ) ) /\ I e. ( 1 ..^ ( # ` F ) ) ) -> ( ( P |` ( 1 ..^ ( # ` F ) ) ) ` I ) = ( P ` I ) )
49 48 adantl 
 |-  ( ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) /\ ( J e. ( 1 ..^ ( # ` F ) ) /\ I e. ( 1 ..^ ( # ` F ) ) ) ) -> ( ( P |` ( 1 ..^ ( # ` F ) ) ) ` I ) = ( P ` I ) )
50 49 eqcomd 
 |-  ( ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) /\ ( J e. ( 1 ..^ ( # ` F ) ) /\ I e. ( 1 ..^ ( # ` F ) ) ) ) -> ( P ` I ) = ( ( P |` ( 1 ..^ ( # ` F ) ) ) ` I ) )
51 fvres 
 |-  ( J e. ( 1 ..^ ( # ` F ) ) -> ( ( P |` ( 1 ..^ ( # ` F ) ) ) ` J ) = ( P ` J ) )
52 51 ad2antrl 
 |-  ( ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) /\ ( J e. ( 1 ..^ ( # ` F ) ) /\ I e. ( 1 ..^ ( # ` F ) ) ) ) -> ( ( P |` ( 1 ..^ ( # ` F ) ) ) ` J ) = ( P ` J ) )
53 52 eqcomd 
 |-  ( ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) /\ ( J e. ( 1 ..^ ( # ` F ) ) /\ I e. ( 1 ..^ ( # ` F ) ) ) ) -> ( P ` J ) = ( ( P |` ( 1 ..^ ( # ` F ) ) ) ` J ) )
54 50 53 eqeq12d 
 |-  ( ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) /\ ( J e. ( 1 ..^ ( # ` F ) ) /\ I e. ( 1 ..^ ( # ` F ) ) ) ) -> ( ( P ` I ) = ( P ` J ) <-> ( ( P |` ( 1 ..^ ( # ` F ) ) ) ` I ) = ( ( P |` ( 1 ..^ ( # ` F ) ) ) ` J ) ) )
55 fssres 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( 1 ..^ ( # ` F ) ) C_ ( 0 ... ( # ` F ) ) ) -> ( P |` ( 1 ..^ ( # ` F ) ) ) : ( 1 ..^ ( # ` F ) ) --> ( Vtx ` G ) )
56 21 55 mpan2 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( P |` ( 1 ..^ ( # ` F ) ) ) : ( 1 ..^ ( # ` F ) ) --> ( Vtx ` G ) )
57 df-f1 
 |-  ( ( P |` ( 1 ..^ ( # ` F ) ) ) : ( 1 ..^ ( # ` F ) ) -1-1-> ( Vtx ` G ) <-> ( ( P |` ( 1 ..^ ( # ` F ) ) ) : ( 1 ..^ ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) ) )
58 57 biimpri 
 |-  ( ( ( P |` ( 1 ..^ ( # ` F ) ) ) : ( 1 ..^ ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) ) -> ( P |` ( 1 ..^ ( # ` F ) ) ) : ( 1 ..^ ( # ` F ) ) -1-1-> ( Vtx ` G ) )
59 56 58 sylan 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) ) -> ( P |` ( 1 ..^ ( # ` F ) ) ) : ( 1 ..^ ( # ` F ) ) -1-1-> ( Vtx ` G ) )
60 59 3adant3 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) -> ( P |` ( 1 ..^ ( # ` F ) ) ) : ( 1 ..^ ( # ` F ) ) -1-1-> ( Vtx ` G ) )
61 simpr 
 |-  ( ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) /\ ( J e. ( 1 ..^ ( # ` F ) ) /\ I e. ( 1 ..^ ( # ` F ) ) ) ) -> ( J e. ( 1 ..^ ( # ` F ) ) /\ I e. ( 1 ..^ ( # ` F ) ) ) )
62 61 ancomd 
 |-  ( ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) /\ ( J e. ( 1 ..^ ( # ` F ) ) /\ I e. ( 1 ..^ ( # ` F ) ) ) ) -> ( I e. ( 1 ..^ ( # ` F ) ) /\ J e. ( 1 ..^ ( # ` F ) ) ) )
63 f1veqaeq 
 |-  ( ( ( P |` ( 1 ..^ ( # ` F ) ) ) : ( 1 ..^ ( # ` F ) ) -1-1-> ( Vtx ` G ) /\ ( I e. ( 1 ..^ ( # ` F ) ) /\ J e. ( 1 ..^ ( # ` F ) ) ) ) -> ( ( ( P |` ( 1 ..^ ( # ` F ) ) ) ` I ) = ( ( P |` ( 1 ..^ ( # ` F ) ) ) ` J ) -> I = J ) )
64 60 62 63 syl2an2r 
 |-  ( ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) /\ ( J e. ( 1 ..^ ( # ` F ) ) /\ I e. ( 1 ..^ ( # ` F ) ) ) ) -> ( ( ( P |` ( 1 ..^ ( # ` F ) ) ) ` I ) = ( ( P |` ( 1 ..^ ( # ` F ) ) ) ` J ) -> I = J ) )
65 54 64 sylbid 
 |-  ( ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) /\ ( J e. ( 1 ..^ ( # ` F ) ) /\ I e. ( 1 ..^ ( # ` F ) ) ) ) -> ( ( P ` I ) = ( P ` J ) -> I = J ) )
66 65 ancoms 
 |-  ( ( ( J e. ( 1 ..^ ( # ` F ) ) /\ I e. ( 1 ..^ ( # ` F ) ) ) /\ ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) ) -> ( ( P ` I ) = ( P ` J ) -> I = J ) )
67 66 necon3d 
 |-  ( ( ( J e. ( 1 ..^ ( # ` F ) ) /\ I e. ( 1 ..^ ( # ` F ) ) ) /\ ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) ) -> ( I =/= J -> ( P ` I ) =/= ( P ` J ) ) )
68 67 ex 
 |-  ( ( J e. ( 1 ..^ ( # ` F ) ) /\ I e. ( 1 ..^ ( # ` F ) ) ) -> ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) -> ( I =/= J -> ( P ` I ) =/= ( P ` J ) ) ) )
69 68 com23 
 |-  ( ( J e. ( 1 ..^ ( # ` F ) ) /\ I e. ( 1 ..^ ( # ` F ) ) ) -> ( I =/= J -> ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) -> ( P ` I ) =/= ( P ` J ) ) ) )
70 69 ex 
 |-  ( J e. ( 1 ..^ ( # ` F ) ) -> ( I e. ( 1 ..^ ( # ` F ) ) -> ( I =/= J -> ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) -> ( P ` I ) =/= ( P ` J ) ) ) ) )
71 9 adantl 
 |-  ( ( J = ( # ` F ) /\ I e. ( 1 ..^ ( # ` F ) ) ) -> ( # ` F ) e. NN0 )
72 71 11 sylan2 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( J = ( # ` F ) /\ I e. ( 1 ..^ ( # ` F ) ) ) ) -> ( ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) <-> ( ( P ` 0 ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) /\ ( P ` ( # ` F ) ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) ) ) )
73 fveq2 
 |-  ( J = ( # ` F ) -> ( P ` J ) = ( P ` ( # ` F ) ) )
74 73 eqeq2d 
 |-  ( J = ( # ` F ) -> ( ( P ` I ) = ( P ` J ) <-> ( P ` I ) = ( P ` ( # ` F ) ) ) )
75 74 ad2antrl 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( J = ( # ` F ) /\ I e. ( 1 ..^ ( # ` F ) ) ) ) -> ( ( P ` I ) = ( P ` J ) <-> ( P ` I ) = ( P ` ( # ` F ) ) ) )
76 27 adantrl 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( J = ( # ` F ) /\ I e. ( 1 ..^ ( # ` F ) ) ) ) -> ( Fun P /\ I e. dom P ) )
77 simprr 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( J = ( # ` F ) /\ I e. ( 1 ..^ ( # ` F ) ) ) ) -> I e. ( 1 ..^ ( # ` F ) ) )
78 76 77 30 sylc 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( J = ( # ` F ) /\ I e. ( 1 ..^ ( # ` F ) ) ) ) -> ( P ` I ) e. ( P " ( 1 ..^ ( # ` F ) ) ) )
79 eleq1 
 |-  ( ( P ` I ) = ( P ` ( # ` F ) ) -> ( ( P ` I ) e. ( P " ( 1 ..^ ( # ` F ) ) ) <-> ( P ` ( # ` F ) ) e. ( P " ( 1 ..^ ( # ` F ) ) ) ) )
80 78 79 syl5ibcom 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( J = ( # ` F ) /\ I e. ( 1 ..^ ( # ` F ) ) ) ) -> ( ( P ` I ) = ( P ` ( # ` F ) ) -> ( P ` ( # ` F ) ) e. ( P " ( 1 ..^ ( # ` F ) ) ) ) )
81 75 80 sylbid 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( J = ( # ` F ) /\ I e. ( 1 ..^ ( # ` F ) ) ) ) -> ( ( P ` I ) = ( P ` J ) -> ( P ` ( # ` F ) ) e. ( P " ( 1 ..^ ( # ` F ) ) ) ) )
82 nnel 
 |-  ( -. ( P ` ( # ` F ) ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) <-> ( P ` ( # ` F ) ) e. ( P " ( 1 ..^ ( # ` F ) ) ) )
83 81 82 syl6ibr 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( J = ( # ` F ) /\ I e. ( 1 ..^ ( # ` F ) ) ) ) -> ( ( P ` I ) = ( P ` J ) -> -. ( P ` ( # ` F ) ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) ) )
84 83 necon2ad 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( J = ( # ` F ) /\ I e. ( 1 ..^ ( # ` F ) ) ) ) -> ( ( P ` ( # ` F ) ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) -> ( P ` I ) =/= ( P ` J ) ) )
85 84 adantld 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( J = ( # ` F ) /\ I e. ( 1 ..^ ( # ` F ) ) ) ) -> ( ( ( P ` 0 ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) /\ ( P ` ( # ` F ) ) e/ ( P " ( 1 ..^ ( # ` F ) ) ) ) -> ( P ` I ) =/= ( P ` J ) ) )
86 72 85 sylbid 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( J = ( # ` F ) /\ I e. ( 1 ..^ ( # ` F ) ) ) ) -> ( ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) -> ( P ` I ) =/= ( P ` J ) ) )
87 86 ex 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( ( J = ( # ` F ) /\ I e. ( 1 ..^ ( # ` F ) ) ) -> ( ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) -> ( P ` I ) =/= ( P ` J ) ) ) )
88 87 com23 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) -> ( ( J = ( # ` F ) /\ I e. ( 1 ..^ ( # ` F ) ) ) -> ( P ` I ) =/= ( P ` J ) ) ) )
89 88 a1d 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) -> ( ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) -> ( ( J = ( # ` F ) /\ I e. ( 1 ..^ ( # ` F ) ) ) -> ( P ` I ) =/= ( P ` J ) ) ) ) )
90 89 3imp 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) -> ( ( J = ( # ` F ) /\ I e. ( 1 ..^ ( # ` F ) ) ) -> ( P ` I ) =/= ( P ` J ) ) )
91 90 com12 
 |-  ( ( J = ( # ` F ) /\ I e. ( 1 ..^ ( # ` F ) ) ) -> ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) -> ( P ` I ) =/= ( P ` J ) ) )
92 91 a1d 
 |-  ( ( J = ( # ` F ) /\ I e. ( 1 ..^ ( # ` F ) ) ) -> ( I =/= J -> ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) -> ( P ` I ) =/= ( P ` J ) ) ) )
93 92 ex 
 |-  ( J = ( # ` F ) -> ( I e. ( 1 ..^ ( # ` F ) ) -> ( I =/= J -> ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) -> ( P ` I ) =/= ( P ` J ) ) ) ) )
94 46 70 93 3jaoi 
 |-  ( ( J = 0 \/ J e. ( 1 ..^ ( # ` F ) ) \/ J = ( # ` F ) ) -> ( I e. ( 1 ..^ ( # ` F ) ) -> ( I =/= J -> ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) -> ( P ` I ) =/= ( P ` J ) ) ) ) )
95 5 94 syl 
 |-  ( J e. ( 0 ... ( # ` F ) ) -> ( I e. ( 1 ..^ ( # ` F ) ) -> ( I =/= J -> ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) -> ( P ` I ) =/= ( P ` J ) ) ) ) )
96 95 3imp21 
 |-  ( ( I e. ( 1 ..^ ( # ` F ) ) /\ J e. ( 0 ... ( # ` F ) ) /\ I =/= J ) -> ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) -> ( P ` I ) =/= ( P ` J ) ) )
97 96 com12 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) -> ( ( I e. ( 1 ..^ ( # ` F ) ) /\ J e. ( 0 ... ( # ` F ) ) /\ I =/= J ) -> ( P ` I ) =/= ( P ` J ) ) )
98 97 3exp 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) -> ( ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) -> ( ( I e. ( 1 ..^ ( # ` F ) ) /\ J e. ( 0 ... ( # ` F ) ) /\ I =/= J ) -> ( P ` I ) =/= ( P ` J ) ) ) ) )
99 2 4 98 3syl 
 |-  ( F ( Trails ` G ) P -> ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) -> ( ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) -> ( ( I e. ( 1 ..^ ( # ` F ) ) /\ J e. ( 0 ... ( # ` F ) ) /\ I =/= J ) -> ( P ` I ) =/= ( P ` J ) ) ) ) )
100 99 3imp 
 |-  ( ( F ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) -> ( ( I e. ( 1 ..^ ( # ` F ) ) /\ J e. ( 0 ... ( # ` F ) ) /\ I =/= J ) -> ( P ` I ) =/= ( P ` J ) ) )
101 1 100 sylbi 
 |-  ( F ( Paths ` G ) P -> ( ( I e. ( 1 ..^ ( # ` F ) ) /\ J e. ( 0 ... ( # ` F ) ) /\ I =/= J ) -> ( P ` I ) =/= ( P ` J ) ) )
102 101 imp 
 |-  ( ( F ( Paths ` G ) P /\ ( I e. ( 1 ..^ ( # ` F ) ) /\ J e. ( 0 ... ( # ` F ) ) /\ I =/= J ) ) -> ( P ` I ) =/= ( P ` J ) )