Metamath Proof Explorer

Theorem sps3wwlks2on

Description: A length 3 string which represents a walk of length 2 between two vertices. Concerns simple pseudographs, in contrast to s3wwlks2on and does not require the Axiom of Choice for its proof. (Contributed by Ender Ting, 28-Jan-2026)

Ref Expression
Hypothesis s3wwlks2on.v ⊢ V = Vtx ⁡ G
Assertion sps3wwlks2on ⊢ G ∈ USHGraph ∧ 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 ∈ USHGraph ∧ 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 biantrud ⊢ A ∈ V ∧ C ∈ V → ⟨“ ABC ”⟩ ∈ 2 WWalksN G ↔ ⟨“ ABC ”⟩ ∈ 2 WWalksN G ∧ ⟨“ ABC ”⟩ ⁡ 0 = A ∧ ⟨“ ABC ”⟩ ⁡ 2 = C
9 4 8 bitr4id ⊢ A ∈ V ∧ C ∈ V → ⟨“ ABC ”⟩ ∈ 2 WWalksN G ∧ ⟨“ ABC ”⟩ ⁡ 0 = A ∧ ⟨“ ABC ”⟩ ⁡ 2 = C ↔ ⟨“ ABC ”⟩ ∈ 2 WWalksN G
10 9 3adant1 ⊢ G ∈ USHGraph ∧ A ∈ V ∧ C ∈ V → ⟨“ ABC ”⟩ ∈ 2 WWalksN G ∧ ⟨“ ABC ”⟩ ⁡ 0 = A ∧ ⟨“ ABC ”⟩ ⁡ 2 = C ↔ ⟨“ ABC ”⟩ ∈ 2 WWalksN G
11 wlklnwwlkn ⊢ G ∈ USHGraph → ∃ f f Walks ⁡ G ⟨“ ABC ”⟩ ∧ f = 2 ↔ ⟨“ ABC ”⟩ ∈ 2 WWalksN G
12 11 bicomd ⊢ G ∈ USHGraph → ⟨“ ABC ”⟩ ∈ 2 WWalksN G ↔ ∃ f f Walks ⁡ G ⟨“ ABC ”⟩ ∧ f = 2
13 12 3ad2ant1 ⊢ G ∈ USHGraph ∧ A ∈ V ∧ C ∈ V → ⟨“ ABC ”⟩ ∈ 2 WWalksN G ↔ ∃ f f Walks ⁡ G ⟨“ ABC ”⟩ ∧ f = 2
14 3 10 13 3bitrd ⊢ G ∈ USHGraph ∧ A ∈ V ∧ C ∈ V → ⟨“ ABC ”⟩ ∈ A 2 WWalksNOn G C ↔ ∃ f f Walks ⁡ G ⟨“ ABC ”⟩ ∧ f = 2