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

Metamath Proof Explorer

Theorem s3wwlks2on

Description: A length 3 string which represents a walk of length 2 between two vertices. (Contributed by Alexander van der Vekens, 15-Feb-2018) (Revised by AV, 12-May-2021)

Ref Expression
Hypothesis s3wwlks2on.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion s3wwlks2on ( ( 𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ↔ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )

Proof

Step Hyp Ref Expression
1 s3wwlks2on.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 wwlknon ⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 2 WWalksN 𝐺 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 ) )
3 2 a1i ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 2 WWalksN 𝐺 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 ) ) )
4 3anass ⊢ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 2 WWalksN 𝐺 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 ) ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 2 WWalksN 𝐺 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 ) ) )
5 s3fv0 ⊢ ( 𝐴 ∈ 𝑉 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 )
6 s3fv2 ⊢ ( 𝐶 ∈ 𝑉 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 )
7 5 6 anim12i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 ) )
8 7 3adant1 ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 ) )
9 8 biantrud ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 2 WWalksN 𝐺 ) ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 2 WWalksN 𝐺 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 ) ) ) )
10 4 9 bitr4id ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 2 WWalksN 𝐺 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 ) ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 2 WWalksN 𝐺 ) ) )
11 wlklnwwlknupgr ⊢ ( 𝐺 ∈ UPGraph → ( ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ ( ♯ ‘ 𝑓 ) = 2 ) ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 2 WWalksN 𝐺 ) ) )
12 11 bicomd ⊢ ( 𝐺 ∈ UPGraph → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 2 WWalksN 𝐺 ) ↔ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )
13 12 3ad2ant1 ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 2 WWalksN 𝐺 ) ↔ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )
14 3 10 13 3bitrd ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ↔ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )