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

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 imbitrrid ⊢ ( 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 imbitrrdi ⊢ ( ( 𝑃 : ( 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 imbitrrdi ⊢ ( ( 𝑃 : ( 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 ... ( ♯ ‘ 𝐹 ) ) ∧ 𝐼 ≠ 𝐽 ) ) → ( 𝑃 ‘ 𝐼 ) ≠ ( 𝑃 ‘ 𝐽 ) )