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 ⊢ V = Vtx ⁡ G
Assertion s3wwlks2on ⊢ G ∈ UPGraph ∧ A ∈ V ∧ C ∈ V → ⟨“ ABC ”⟩ ∈ A 2 WWalksNOn G C ↔ ∃ f f Walks ⁡ G ⟨“ ABC ”⟩ ∧ f = 2

Proof

Step Hyp Ref Expression
1 s3wwlks2on.v ⊢ V = Vtx ⁡ G
2 wwlknon ⊢ ⟨“ ABC ”⟩ ∈ A 2 WWalksNOn G C ↔ ⟨“ ABC ”⟩ ∈ 2 WWalksN G ∧ ⟨“ ABC ”⟩ ⁡ 0 = A ∧ ⟨“ ABC ”⟩ ⁡ 2 = C
3 2 a1i ⊢ G ∈ UPGraph ∧ A ∈ V ∧ C ∈ V → ⟨“ ABC ”⟩ ∈ A 2 WWalksNOn G C ↔ ⟨“ ABC ”⟩ ∈ 2 WWalksN G ∧ ⟨“ ABC ”⟩ ⁡ 0 = A ∧ ⟨“ ABC ”⟩ ⁡ 2 = C
4 3anass ⊢ ⟨“ ABC ”⟩ ∈ 2 WWalksN G ∧ ⟨“ ABC ”⟩ ⁡ 0 = A ∧ ⟨“ ABC ”⟩ ⁡ 2 = C ↔ ⟨“ ABC ”⟩ ∈ 2 WWalksN G ∧ ⟨“ ABC ”⟩ ⁡ 0 = A ∧ ⟨“ ABC ”⟩ ⁡ 2 = C
5 s3fv0 ⊢ A ∈ V → ⟨“ ABC ”⟩ ⁡ 0 = A
6 s3fv2 ⊢ C ∈ V → ⟨“ ABC ”⟩ ⁡ 2 = C
7 5 6 anim12i ⊢ A ∈ V ∧ C ∈ V → ⟨“ ABC ”⟩ ⁡ 0 = A ∧ ⟨“ ABC ”⟩ ⁡ 2 = C
8 7 3adant1 ⊢ G ∈ UPGraph ∧ A ∈ V ∧ C ∈ V → ⟨“ ABC ”⟩ ⁡ 0 = A ∧ ⟨“ ABC ”⟩ ⁡ 2 = C
9 8 biantrud ⊢ G ∈ UPGraph ∧ A ∈ V ∧ C ∈ V → ⟨“ ABC ”⟩ ∈ 2 WWalksN G ↔ ⟨“ ABC ”⟩ ∈ 2 WWalksN G ∧ ⟨“ ABC ”⟩ ⁡ 0 = A ∧ ⟨“ ABC ”⟩ ⁡ 2 = C
10 4 9 bitr4id ⊢ G ∈ UPGraph ∧ A ∈ V ∧ C ∈ V → ⟨“ ABC ”⟩ ∈ 2 WWalksN G ∧ ⟨“ ABC ”⟩ ⁡ 0 = A ∧ ⟨“ ABC ”⟩ ⁡ 2 = C ↔ ⟨“ ABC ”⟩ ∈ 2 WWalksN G
11 wlklnwwlknupgr ⊢ G ∈ UPGraph → ∃ f f Walks ⁡ G ⟨“ ABC ”⟩ ∧ f = 2 ↔ ⟨“ ABC ”⟩ ∈ 2 WWalksN G
12 11 bicomd ⊢ G ∈ UPGraph → ⟨“ ABC ”⟩ ∈ 2 WWalksN G ↔ ∃ f f Walks ⁡ G ⟨“ ABC ”⟩ ∧ f = 2
13 12 3ad2ant1 ⊢ G ∈ UPGraph ∧ A ∈ V ∧ C ∈ V → ⟨“ ABC ”⟩ ∈ 2 WWalksN G ↔ ∃ f f Walks ⁡ G ⟨“ ABC ”⟩ ∧ f = 2
14 3 10 13 3bitrd ⊢ G ∈ UPGraph ∧ A ∈ V ∧ C ∈ V → ⟨“ ABC ”⟩ ∈ A 2 WWalksNOn G C ↔ ∃ f f Walks ⁡ G ⟨“ ABC ”⟩ ∧ f = 2