Theorem usgr2wspthons3

Description: A simple path of length 2 between two vertices represented as length 3 string corresponds to two adjacent edges in a simple graph. (Contributed by Alexander van der Vekens, 8-Mar-2018) (Revised by AV, 17-May-2021) (Proof shortened by AV, 16-Mar-2022) (Revised by Ender Ting, 29-Jan-2026)

	Ref	Expression
Hypotheses	usgr2wspthon0.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	usgr2wspthon0.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	usgr2wspthons3	⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ↔ ( 𝐴 ≠ 𝐶 ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) )

Proof

Step	Hyp	Ref	Expression
1		usgr2wspthon0.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		usgr2wspthon0.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		2nn	⊢ 2 ∈ ℕ
4		ne0i	⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ≠ ∅ )
5		wspthsnonn0vne	⊢ ( ( 2 ∈ ℕ ∧ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ≠ ∅ ) → 𝐴 ≠ 𝐶 )
6	3 4 5	sylancr	⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → 𝐴 ≠ 𝐶 )
7		simplr	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐶 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) → 𝐴 ≠ 𝐶 )
8		wpthswwlks2on	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐶 ) → ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) = ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) )
9	8	eleq2d	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐶 ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) )
10	9	biimpa	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐶 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) )
11	7 10	jca	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐶 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) → ( 𝐴 ≠ 𝐶 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) )
12	11	exp31	⊢ ( 𝐺 ∈ USGraph → ( 𝐴 ≠ 𝐶 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ( 𝐴 ≠ 𝐶 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) ) ) )
13	12	com13	⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ( 𝐴 ≠ 𝐶 → ( 𝐺 ∈ USGraph → ( 𝐴 ≠ 𝐶 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) ) ) )
14	6 13	mpd	⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ( 𝐺 ∈ USGraph → ( 𝐴 ≠ 𝐶 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) ) )
15	14	com12	⊢ ( 𝐺 ∈ USGraph → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ( 𝐴 ≠ 𝐶 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) ) )
16	9	biimprd	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐶 ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) )
17	16	expimpd	⊢ ( 𝐺 ∈ USGraph → ( ( 𝐴 ≠ 𝐶 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) )
18	15 17	impbid	⊢ ( 𝐺 ∈ USGraph → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ↔ ( 𝐴 ≠ 𝐶 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) ) )
19	18	adantr	⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ↔ ( 𝐴 ≠ 𝐶 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) ) )
20	1 2	usgrwwlks2on	⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) )
21	20	anbi2d	⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 ≠ 𝐶 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) ↔ ( 𝐴 ≠ 𝐶 ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) ) )
22		3anass	⊢ ( ( 𝐴 ≠ 𝐶 ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ↔ ( 𝐴 ≠ 𝐶 ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) )
23	21 22	bitr4di	⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 ≠ 𝐶 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) ↔ ( 𝐴 ≠ 𝐶 ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) )
24	19 23	bitrd	⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ↔ ( 𝐴 ≠ 𝐶 ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) )