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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	sps3wwlks2on	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ↔ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		s3wwlks2on.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		wwlknon	⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 2 WWalksN 𝐺 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 ) )
3	2	a1i	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 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	biantrud	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 2 WWalksN 𝐺 ) ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 2 WWalksN 𝐺 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 ) ) ) )
9	4 8	bitr4id	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 2 WWalksN 𝐺 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 ) ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 2 WWalksN 𝐺 ) ) )
10	9	3adant1	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 2 WWalksN 𝐺 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 ) ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 2 WWalksN 𝐺 ) ) )
11		wlklnwwlkn	⊢ ( 𝐺 ∈ USPGraph → ( ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ ( ♯ ‘ 𝑓 ) = 2 ) ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 2 WWalksN 𝐺 ) ) )
12	11	bicomd	⊢ ( 𝐺 ∈ USPGraph → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 2 WWalksN 𝐺 ) ↔ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )
13	12	3ad2ant1	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 2 WWalksN 𝐺 ) ↔ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )
14	3 10 13	3bitrd	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ↔ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )