Metamath Proof Explorer

Theorem elwspths2onw

Description: A simple path of length 2 between two vertices (in a simple pseudograph) as length 3 string. This theorem avoids the Axiom of Choice for its proof, at the cost of requiring a simple graph; the more general version is elwspths2on . (Contributed by Ender Ting, 29-Jan-2026)

Ref Expression
Hypothesis elwwlks2on.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion elwspths2onw ( ( 𝐺 ∈ USPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ↔ ∃ 𝑏 ∈ 𝑉 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) )

Proof

Step Hyp Ref Expression
1 elwwlks2on.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 wspthnon ⊢ ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ↔ ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ∧ ∃ 𝑏 𝑏 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐶 ) 𝑊 ) )
3 2 biimpi ⊢ ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ∧ ∃ 𝑏 𝑏 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐶 ) 𝑊 ) )
4 1 elwwlks2ons3 ⊢ ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ↔ ∃ 𝑏 ∈ 𝑉 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) )
5 4 a1i ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ↔ ∃ 𝑏 ∈ 𝑉 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) ) )
6 simpl ⊢ ( ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) → 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ )
7 eleq1 ⊢ ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ → ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ↔ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) )
8 7 biimpa ⊢ ( ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) → ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) )
9 6 8 jca ⊢ ( ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) → ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) )
10 9 ex ⊢ ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ → ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) )
11 10 adantr ⊢ ( ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) → ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) )
12 11 com12 ⊢ ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ( ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) → ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) )
13 12 reximdv ⊢ ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ( ∃ 𝑏 ∈ 𝑉 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) → ∃ 𝑏 ∈ 𝑉 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) )
14 13 a1i13 ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ( ∃ 𝑏 𝑏 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐶 ) 𝑊 → ( ∃ 𝑏 ∈ 𝑉 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) → ∃ 𝑏 ∈ 𝑉 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) ) ) )
15 14 com24 ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ∃ 𝑏 ∈ 𝑉 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) → ( ∃ 𝑏 𝑏 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐶 ) 𝑊 → ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ∃ 𝑏 ∈ 𝑉 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) ) ) )
16 5 15 sylbid ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) → ( ∃ 𝑏 𝑏 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐶 ) 𝑊 → ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ∃ 𝑏 ∈ 𝑉 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) ) ) )
17 16 impd ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ∧ ∃ 𝑏 𝑏 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐶 ) 𝑊 ) → ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ∃ 𝑏 ∈ 𝑉 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) ) )
18 17 com23 ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ( ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ∧ ∃ 𝑏 𝑏 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐶 ) 𝑊 ) → ∃ 𝑏 ∈ 𝑉 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) ) )
19 3 18 mpdi ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ∃ 𝑏 ∈ 𝑉 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) )
20 7 biimpar ⊢ ( ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) → 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) )
21 20 a1i ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝑏 ∈ 𝑉 ) → ( ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) → 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) )
22 21 rexlimdva ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ∃ 𝑏 ∈ 𝑉 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) → 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) )
23 19 22 impbid ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ↔ ∃ 𝑏 ∈ 𝑉 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) )