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 ) )