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 ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝐽 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 𝐼𝐽 ) ) → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) )

Proof

Step Hyp Ref Expression
1 ispth ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) )
2 trliswlk ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
3 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
4 3 wlkp ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
5 elfz0lmr ( 𝐽 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) → ( 𝐽 = 0 ∨ 𝐽 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∨ 𝐽 = ( ♯ ‘ 𝐹 ) ) )
6 elfzo1 ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ↔ ( 𝐼 ∈ ℕ ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ∧ 𝐼 < ( ♯ ‘ 𝐹 ) ) )
7 nnnn0 ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
8 7 3ad2ant2 ( ( 𝐼 ∈ ℕ ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ∧ 𝐼 < ( ♯ ‘ 𝐹 ) ) → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
9 6 8 sylbi ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
10 9 adantl ( ( 𝐽 = 0 ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
11 fvinim0ffz ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) → ( ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ↔ ( ( 𝑃 ‘ 0 ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ) )
12 10 11 sylan2 ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( 𝐽 = 0 ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ↔ ( ( 𝑃 ‘ 0 ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ) )
13 fveq2 ( 𝐽 = 0 → ( 𝑃𝐽 ) = ( 𝑃 ‘ 0 ) )
14 13 eqeq2d ( 𝐽 = 0 → ( ( 𝑃𝐼 ) = ( 𝑃𝐽 ) ↔ ( 𝑃𝐼 ) = ( 𝑃 ‘ 0 ) ) )
15 14 ad2antrl ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( 𝐽 = 0 ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( 𝑃𝐼 ) = ( 𝑃𝐽 ) ↔ ( 𝑃𝐼 ) = ( 𝑃 ‘ 0 ) ) )
16 ffun ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → Fun 𝑃 )
17 16 adantr ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → Fun 𝑃 )
18 fdm ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → dom 𝑃 = ( 0 ... ( ♯ ‘ 𝐹 ) ) )
19 fzo0ss1 ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) )
20 fzossfz ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝐹 ) )
21 19 20 sstri ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝐹 ) )
22 21 sseli ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → 𝐼 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
23 eleq2 ( dom 𝑃 = ( 0 ... ( ♯ ‘ 𝐹 ) ) → ( 𝐼 ∈ dom 𝑃𝐼 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) )
24 22 23 syl5ibr ( dom 𝑃 = ( 0 ... ( ♯ ‘ 𝐹 ) ) → ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → 𝐼 ∈ dom 𝑃 ) )
25 18 24 syl ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → 𝐼 ∈ dom 𝑃 ) )
26 25 imp ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝐼 ∈ dom 𝑃 )
27 17 26 jca ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( Fun 𝑃𝐼 ∈ dom 𝑃 ) )
28 27 adantrl ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( 𝐽 = 0 ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( Fun 𝑃𝐼 ∈ dom 𝑃 ) )
29 simprr ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( 𝐽 = 0 ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) )
30 funfvima ( ( Fun 𝑃𝐼 ∈ dom 𝑃 ) → ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝑃𝐼 ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
31 28 29 30 sylc ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( 𝐽 = 0 ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝑃𝐼 ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
32 eleq1 ( ( 𝑃𝐼 ) = ( 𝑃 ‘ 0 ) → ( ( 𝑃𝐼 ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ↔ ( 𝑃 ‘ 0 ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
33 31 32 syl5ibcom ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( 𝐽 = 0 ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( 𝑃𝐼 ) = ( 𝑃 ‘ 0 ) → ( 𝑃 ‘ 0 ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
34 15 33 sylbid ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( 𝐽 = 0 ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( 𝑃𝐼 ) = ( 𝑃𝐽 ) → ( 𝑃 ‘ 0 ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
35 nnel ( ¬ ( 𝑃 ‘ 0 ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ↔ ( 𝑃 ‘ 0 ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
36 34 35 syl6ibr ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( 𝐽 = 0 ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( 𝑃𝐼 ) = ( 𝑃𝐽 ) → ¬ ( 𝑃 ‘ 0 ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
37 36 necon2ad ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( 𝐽 = 0 ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( 𝑃 ‘ 0 ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) ) )
38 37 adantrd ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( 𝐽 = 0 ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( ( 𝑃 ‘ 0 ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) ) )
39 12 38 sylbid ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( 𝐽 = 0 ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) ) )
40 39 ex ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( ( 𝐽 = 0 ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) ) ) )
41 40 com23 ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ → ( ( 𝐽 = 0 ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) ) ) )
42 41 a1d ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ → ( ( 𝐽 = 0 ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) ) ) ) )
43 42 3imp ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) → ( ( 𝐽 = 0 ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) ) )
44 43 com12 ( ( 𝐽 = 0 ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) ) )
45 44 a1d ( ( 𝐽 = 0 ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐼𝐽 → ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) ) ) )
46 45 ex ( 𝐽 = 0 → ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐼𝐽 → ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) ) ) ) )
47 fvres ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝐼 ) = ( 𝑃𝐼 ) )
48 47 adantl ( ( 𝐽 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝐼 ) = ( 𝑃𝐼 ) )
49 48 adantl ( ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) ∧ ( 𝐽 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝐼 ) = ( 𝑃𝐼 ) )
50 49 eqcomd ( ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) ∧ ( 𝐽 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝑃𝐼 ) = ( ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝐼 ) )
51 fvres ( 𝐽 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝐽 ) = ( 𝑃𝐽 ) )
52 51 ad2antrl ( ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) ∧ ( 𝐽 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝐽 ) = ( 𝑃𝐽 ) )
53 52 eqcomd ( ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) ∧ ( 𝐽 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝑃𝐽 ) = ( ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝐽 ) )
54 50 53 eqeq12d ( ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) ∧ ( 𝐽 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( 𝑃𝐼 ) = ( 𝑃𝐽 ) ↔ ( ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝐼 ) = ( ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝐽 ) ) )
55 fssres ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) : ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
56 21 55 mpan2 ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) : ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
57 df-f1 ( ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) : ( 1 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ ( Vtx ‘ 𝐺 ) ↔ ( ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) : ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
58 57 biimpri ( ( ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) : ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) : ( 1 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ ( Vtx ‘ 𝐺 ) )
59 56 58 sylan ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) : ( 1 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ ( Vtx ‘ 𝐺 ) )
60 59 3adant3 ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) → ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) : ( 1 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ ( Vtx ‘ 𝐺 ) )
61 simpr ( ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) ∧ ( 𝐽 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝐽 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
62 61 ancomd ( ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) ∧ ( 𝐽 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝐽 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
63 f1veqaeq ( ( ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) : ( 1 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ ( Vtx ‘ 𝐺 ) ∧ ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝐽 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝐼 ) = ( ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝐽 ) → 𝐼 = 𝐽 ) )
64 60 62 63 syl2an2r ( ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) ∧ ( 𝐽 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝐼 ) = ( ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ‘ 𝐽 ) → 𝐼 = 𝐽 ) )
65 54 64 sylbid ( ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) ∧ ( 𝐽 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( 𝑃𝐼 ) = ( 𝑃𝐽 ) → 𝐼 = 𝐽 ) )
66 65 ancoms ( ( ( 𝐽 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) ) → ( ( 𝑃𝐼 ) = ( 𝑃𝐽 ) → 𝐼 = 𝐽 ) )
67 66 necon3d ( ( ( 𝐽 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) ) → ( 𝐼𝐽 → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) ) )
68 67 ex ( ( 𝐽 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) → ( 𝐼𝐽 → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) ) ) )
69 68 com23 ( ( 𝐽 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐼𝐽 → ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) ) ) )
70 69 ex ( 𝐽 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐼𝐽 → ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) ) ) ) )
71 9 adantl ( ( 𝐽 = ( ♯ ‘ 𝐹 ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
72 71 11 sylan2 ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( 𝐽 = ( ♯ ‘ 𝐹 ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ↔ ( ( 𝑃 ‘ 0 ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ) )
73 fveq2 ( 𝐽 = ( ♯ ‘ 𝐹 ) → ( 𝑃𝐽 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) )
74 73 eqeq2d ( 𝐽 = ( ♯ ‘ 𝐹 ) → ( ( 𝑃𝐼 ) = ( 𝑃𝐽 ) ↔ ( 𝑃𝐼 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
75 74 ad2antrl ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( 𝐽 = ( ♯ ‘ 𝐹 ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( 𝑃𝐼 ) = ( 𝑃𝐽 ) ↔ ( 𝑃𝐼 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
76 27 adantrl ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( 𝐽 = ( ♯ ‘ 𝐹 ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( Fun 𝑃𝐼 ∈ dom 𝑃 ) )
77 simprr ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( 𝐽 = ( ♯ ‘ 𝐹 ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) )
78 76 77 30 sylc ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( 𝐽 = ( ♯ ‘ 𝐹 ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝑃𝐼 ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
79 eleq1 ( ( 𝑃𝐼 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → ( ( 𝑃𝐼 ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ↔ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
80 78 79 syl5ibcom ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( 𝐽 = ( ♯ ‘ 𝐹 ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( 𝑃𝐼 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
81 75 80 sylbid ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( 𝐽 = ( ♯ ‘ 𝐹 ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( 𝑃𝐼 ) = ( 𝑃𝐽 ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
82 nnel ( ¬ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ↔ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
83 81 82 syl6ibr ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( 𝐽 = ( ♯ ‘ 𝐹 ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( 𝑃𝐼 ) = ( 𝑃𝐽 ) → ¬ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
84 83 necon2ad ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( 𝐽 = ( ♯ ‘ 𝐹 ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) ) )
85 84 adantld ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( 𝐽 = ( ♯ ‘ 𝐹 ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( ( 𝑃 ‘ 0 ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∉ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) ) )
86 72 85 sylbid ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( 𝐽 = ( ♯ ‘ 𝐹 ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) ) )
87 86 ex ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( ( 𝐽 = ( ♯ ‘ 𝐹 ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) ) ) )
88 87 com23 ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ → ( ( 𝐽 = ( ♯ ‘ 𝐹 ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) ) ) )
89 88 a1d ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ → ( ( 𝐽 = ( ♯ ‘ 𝐹 ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) ) ) ) )
90 89 3imp ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) → ( ( 𝐽 = ( ♯ ‘ 𝐹 ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) ) )
91 90 com12 ( ( 𝐽 = ( ♯ ‘ 𝐹 ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) ) )
92 91 a1d ( ( 𝐽 = ( ♯ ‘ 𝐹 ) ∧ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐼𝐽 → ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) ) ) )
93 92 ex ( 𝐽 = ( ♯ ‘ 𝐹 ) → ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐼𝐽 → ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) ) ) ) )
94 46 70 93 3jaoi ( ( 𝐽 = 0 ∨ 𝐽 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∨ 𝐽 = ( ♯ ‘ 𝐹 ) ) → ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐼𝐽 → ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) ) ) ) )
95 5 94 syl ( 𝐽 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) → ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐼𝐽 → ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) ) ) ) )
96 95 3imp21 ( ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝐽 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 𝐼𝐽 ) → ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) ) )
97 96 com12 ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) → ( ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝐽 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 𝐼𝐽 ) → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) ) )
98 97 3exp ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ → ( ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝐽 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 𝐼𝐽 ) → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) ) ) ) )
99 2 4 98 3syl ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ( Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ → ( ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝐽 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 𝐼𝐽 ) → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) ) ) ) )
100 99 3imp ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) → ( ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝐽 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 𝐼𝐽 ) → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) ) )
101 1 100 sylbi ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝐽 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 𝐼𝐽 ) → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) ) )
102 101 imp ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝐽 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 𝐼𝐽 ) ) → ( 𝑃𝐼 ) ≠ ( 𝑃𝐽 ) )