Metamath Proof Explorer

Theorem spthonepeq

Description: The endpoints of a simple path between two vertices are equal iff the path is of length 0. (Contributed by Alexander van der Vekens, 1-Mar-2018) (Revised by AV, 18-Jan-2021) (Proof shortened by AV, 31-Oct-2021)

Ref Expression
Assertion spthonepeq ( 𝐹 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 → ( 𝐴 = 𝐵 ↔ ( ♯ ‘ 𝐹 ) = 0 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 1 spthonprop ⊢ ( 𝐹 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 → ( ( 𝐺 ∈ V ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) ) )
3 1 istrlson ⊢ ( ( ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) → ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ↔ ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) ) )
4 3 3adantl1 ⊢ ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) → ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ↔ ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) ) )
5 isspth ⊢ ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) )
6 5 a1i ⊢ ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) → ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) ) )
7 4 6 anbi12d ⊢ ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) → ( ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) ↔ ( ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) ∧ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) ) ) )
8 1 wlkonprop ⊢ ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 → ( ( 𝐺 ∈ V ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) )
9 wlkcl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
10 1 wlkp ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
11 df-f1 ⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ ( Vtx ‘ 𝐺 ) ↔ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ◡ 𝑃 ) )
12 eqeq2 ⊢ ( 𝐴 = 𝐵 → ( ( 𝑃 ‘ 0 ) = 𝐴 ↔ ( 𝑃 ‘ 0 ) = 𝐵 ) )
13 eqtr3 ⊢ ( ( ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ∧ ( 𝑃 ‘ 0 ) = 𝐵 ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ 0 ) )
14 elnn0uz ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ 0 ) )
15 eluzfz2 ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ 0 ) → ( ♯ ‘ 𝐹 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
16 14 15 sylbi ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ 𝐹 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
17 0elfz ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
18 16 17 jca ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ( ♯ ‘ 𝐹 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) )
19 f1veqaeq ⊢ ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝐹 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ) → ( ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ 0 ) → ( ♯ ‘ 𝐹 ) = 0 ) )
20 18 19 sylan2 ⊢ ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) → ( ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ 0 ) → ( ♯ ‘ 𝐹 ) = 0 ) )
21 20 ex ⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ 0 ) → ( ♯ ‘ 𝐹 ) = 0 ) ) )
22 21 com13 ⊢ ( ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ 0 ) → ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ ( Vtx ‘ 𝐺 ) → ( ♯ ‘ 𝐹 ) = 0 ) ) )
23 13 22 syl ⊢ ( ( ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ∧ ( 𝑃 ‘ 0 ) = 𝐵 ) → ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ ( Vtx ‘ 𝐺 ) → ( ♯ ‘ 𝐹 ) = 0 ) ) )
24 23 expcom ⊢ ( ( 𝑃 ‘ 0 ) = 𝐵 → ( ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 → ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ ( Vtx ‘ 𝐺 ) → ( ♯ ‘ 𝐹 ) = 0 ) ) ) )
25 12 24 syl6bi ⊢ ( 𝐴 = 𝐵 → ( ( 𝑃 ‘ 0 ) = 𝐴 → ( ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 → ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ ( Vtx ‘ 𝐺 ) → ( ♯ ‘ 𝐹 ) = 0 ) ) ) ) )
26 25 com15 ⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ ( Vtx ‘ 𝐺 ) → ( ( 𝑃 ‘ 0 ) = 𝐴 → ( ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 → ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 𝐴 = 𝐵 → ( ♯ ‘ 𝐹 ) = 0 ) ) ) ) )
27 11 26 sylbir ⊢ ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ◡ 𝑃 ) → ( ( 𝑃 ‘ 0 ) = 𝐴 → ( ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 → ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 𝐴 = 𝐵 → ( ♯ ‘ 𝐹 ) = 0 ) ) ) ) )
28 27 expcom ⊢ ( Fun ◡ 𝑃 → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( ( 𝑃 ‘ 0 ) = 𝐴 → ( ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 → ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 𝐴 = 𝐵 → ( ♯ ‘ 𝐹 ) = 0 ) ) ) ) ) )
29 28 com15 ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( ( 𝑃 ‘ 0 ) = 𝐴 → ( ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 → ( Fun ◡ 𝑃 → ( 𝐴 = 𝐵 → ( ♯ ‘ 𝐹 ) = 0 ) ) ) ) ) )
30 9 10 29 sylc ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ( 𝑃 ‘ 0 ) = 𝐴 → ( ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 → ( Fun ◡ 𝑃 → ( 𝐴 = 𝐵 → ( ♯ ‘ 𝐹 ) = 0 ) ) ) ) )
31 30 3imp1 ⊢ ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ∧ Fun ◡ 𝑃 ) → ( 𝐴 = 𝐵 → ( ♯ ‘ 𝐹 ) = 0 ) )
32 fveqeq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 0 → ( ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ↔ ( 𝑃 ‘ 0 ) = 𝐵 ) )
33 32 anbi2d ⊢ ( ( ♯ ‘ 𝐹 ) = 0 → ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ↔ ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 0 ) = 𝐵 ) ) )
34 eqtr2 ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 0 ) = 𝐵 ) → 𝐴 = 𝐵 )
35 33 34 syl6bi ⊢ ( ( ♯ ‘ 𝐹 ) = 0 → ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → 𝐴 = 𝐵 ) )
36 35 com12 ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → ( ( ♯ ‘ 𝐹 ) = 0 → 𝐴 = 𝐵 ) )
37 36 3adant1 ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → ( ( ♯ ‘ 𝐹 ) = 0 → 𝐴 = 𝐵 ) )
38 37 adantr ⊢ ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ∧ Fun ◡ 𝑃 ) → ( ( ♯ ‘ 𝐹 ) = 0 → 𝐴 = 𝐵 ) )
39 31 38 impbid ⊢ ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ∧ Fun ◡ 𝑃 ) → ( 𝐴 = 𝐵 ↔ ( ♯ ‘ 𝐹 ) = 0 ) )
40 39 ex ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → ( Fun ◡ 𝑃 → ( 𝐴 = 𝐵 ↔ ( ♯ ‘ 𝐹 ) = 0 ) ) )
41 40 3ad2ant3 ⊢ ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) → ( Fun ◡ 𝑃 → ( 𝐴 = 𝐵 ↔ ( ♯ ‘ 𝐹 ) = 0 ) ) )
42 8 41 syl ⊢ ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 → ( Fun ◡ 𝑃 → ( 𝐴 = 𝐵 ↔ ( ♯ ‘ 𝐹 ) = 0 ) ) )
43 42 adantld ⊢ ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 → ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) → ( 𝐴 = 𝐵 ↔ ( ♯ ‘ 𝐹 ) = 0 ) ) )
44 43 adantr ⊢ ( ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) → ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) → ( 𝐴 = 𝐵 ↔ ( ♯ ‘ 𝐹 ) = 0 ) ) )
45 44 imp ⊢ ( ( ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) ∧ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) ) → ( 𝐴 = 𝐵 ↔ ( ♯ ‘ 𝐹 ) = 0 ) )
46 7 45 syl6bi ⊢ ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) → ( ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) → ( 𝐴 = 𝐵 ↔ ( ♯ ‘ 𝐹 ) = 0 ) ) )
47 46 3impia ⊢ ( ( ( 𝐺 ∈ V ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) ) → ( 𝐴 = 𝐵 ↔ ( ♯ ‘ 𝐹 ) = 0 ) )
48 2 47 syl ⊢ ( 𝐹 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 → ( 𝐴 = 𝐵 ↔ ( ♯ ‘ 𝐹 ) = 0 ) )