Metamath Proof Explorer


Theorem usgr2wlkspthlem2

Description: Lemma 2 for usgr2wlkspth . (Contributed by Alexander van der Vekens, 2-Mar-2018) (Revised by AV, 27-Jan-2021)

Ref Expression
Assertion usgr2wlkspthlem2 ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → Fun 𝑃 )

Proof

Step Hyp Ref Expression
1 simp1 ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → 𝐺 ∈ USGraph )
2 1 anim2i ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃𝐺 ∈ USGraph ) )
3 2 ancomd ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝐺 ∈ USGraph ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) )
4 3simpc ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
5 4 adantl ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
6 usgr2wlkneq ( ( ( 𝐺 ∈ USGraph ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) ∧ ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 1 ) ) )
7 3 5 6 syl2anc ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 1 ) ) )
8 simpl ( ( ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 1 ) ) → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ) )
9 fvex ( 𝑃 ‘ 0 ) ∈ V
10 fvex ( 𝑃 ‘ 1 ) ∈ V
11 fvex ( 𝑃 ‘ 2 ) ∈ V
12 9 10 11 3pm3.2i ( ( 𝑃 ‘ 0 ) ∈ V ∧ ( 𝑃 ‘ 1 ) ∈ V ∧ ( 𝑃 ‘ 2 ) ∈ V )
13 8 12 jctil ( ( ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 1 ) ) → ( ( ( 𝑃 ‘ 0 ) ∈ V ∧ ( 𝑃 ‘ 1 ) ∈ V ∧ ( 𝑃 ‘ 2 ) ∈ V ) ∧ ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ) ) )
14 funcnvs3 ( ( ( ( 𝑃 ‘ 0 ) ∈ V ∧ ( 𝑃 ‘ 1 ) ∈ V ∧ ( 𝑃 ‘ 2 ) ∈ V ) ∧ ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ∧ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ) ) → Fun ⟨“ ( 𝑃 ‘ 0 ) ( 𝑃 ‘ 1 ) ( 𝑃 ‘ 2 ) ”⟩ )
15 7 13 14 3syl ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → Fun ⟨“ ( 𝑃 ‘ 0 ) ( 𝑃 ‘ 1 ) ( 𝑃 ‘ 2 ) ”⟩ )
16 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
17 16 wlkpwrd ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃𝑃 ∈ Word ( Vtx ‘ 𝐺 ) )
18 wlklenvp1 ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) )
19 oveq1 ( ( ♯ ‘ 𝐹 ) = 2 → ( ( ♯ ‘ 𝐹 ) + 1 ) = ( 2 + 1 ) )
20 2p1e3 ( 2 + 1 ) = 3
21 19 20 eqtrdi ( ( ♯ ‘ 𝐹 ) = 2 → ( ( ♯ ‘ 𝐹 ) + 1 ) = 3 )
22 21 3ad2ant2 ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( ( ♯ ‘ 𝐹 ) + 1 ) = 3 )
23 18 22 sylan9eq ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → ( ♯ ‘ 𝑃 ) = 3 )
24 wrdlen3s3 ( ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 3 ) → 𝑃 = ⟨“ ( 𝑃 ‘ 0 ) ( 𝑃 ‘ 1 ) ( 𝑃 ‘ 2 ) ”⟩ )
25 17 23 24 syl2an2r ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → 𝑃 = ⟨“ ( 𝑃 ‘ 0 ) ( 𝑃 ‘ 1 ) ( 𝑃 ‘ 2 ) ”⟩ )
26 25 cnveqd ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → 𝑃 = ⟨“ ( 𝑃 ‘ 0 ) ( 𝑃 ‘ 1 ) ( 𝑃 ‘ 2 ) ”⟩ )
27 26 funeqd ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → ( Fun 𝑃 ↔ Fun ⟨“ ( 𝑃 ‘ 0 ) ( 𝑃 ‘ 1 ) ( 𝑃 ‘ 2 ) ”⟩ ) )
28 15 27 mpbird ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → Fun 𝑃 )