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

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