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 ⊢ V = Vtx ⁡ G
Assertion elwspths2onw ⊢ G ∈ USHGraph ∧ A ∈ V ∧ C ∈ V → W ∈ A 2 WSPathsNOn G C ↔ ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C

Proof

Step Hyp Ref Expression
1 elwwlks2on.v ⊢ V = Vtx ⁡ G
2 wspthnon ⊢ W ∈ A 2 WSPathsNOn G C ↔ W ∈ A 2 WWalksNOn G C ∧ ∃ b b A SPathsOn ⁡ G C W
3 2 biimpi ⊢ W ∈ A 2 WSPathsNOn G C → W ∈ A 2 WWalksNOn G C ∧ ∃ b b A SPathsOn ⁡ G C W
4 1 elwwlks2ons3 ⊢ W ∈ A 2 WWalksNOn G C ↔ ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WWalksNOn G C
5 4 a1i ⊢ G ∈ USHGraph ∧ A ∈ V ∧ C ∈ V → W ∈ A 2 WWalksNOn G C ↔ ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WWalksNOn G C
6 simpl ⊢ W = ⟨“ AbC ”⟩ ∧ W ∈ A 2 WSPathsNOn G C → W = ⟨“ AbC ”⟩
7 eleq1 ⊢ W = ⟨“ AbC ”⟩ → W ∈ A 2 WSPathsNOn G C ↔ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C
8 7 biimpa ⊢ W = ⟨“ AbC ”⟩ ∧ W ∈ A 2 WSPathsNOn G C → ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C
9 6 8 jca ⊢ W = ⟨“ AbC ”⟩ ∧ W ∈ A 2 WSPathsNOn G C → W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C
10 9 ex ⊢ W = ⟨“ AbC ”⟩ → W ∈ A 2 WSPathsNOn G C → W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C
11 10 adantr ⊢ W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WWalksNOn G C → W ∈ A 2 WSPathsNOn G C → W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C
12 11 com12 ⊢ W ∈ A 2 WSPathsNOn G C → W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WWalksNOn G C → W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C
13 12 reximdv ⊢ W ∈ A 2 WSPathsNOn G C → ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WWalksNOn G C → ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C
14 13 a1i13 ⊢ G ∈ USHGraph ∧ A ∈ V ∧ C ∈ V → W ∈ A 2 WSPathsNOn G C → ∃ b b A SPathsOn ⁡ G C W → ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WWalksNOn G C → ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C
15 14 com24 ⊢ G ∈ USHGraph ∧ A ∈ V ∧ C ∈ V → ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WWalksNOn G C → ∃ b b A SPathsOn ⁡ G C W → W ∈ A 2 WSPathsNOn G C → ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C
16 5 15 sylbid ⊢ G ∈ USHGraph ∧ A ∈ V ∧ C ∈ V → W ∈ A 2 WWalksNOn G C → ∃ b b A SPathsOn ⁡ G C W → W ∈ A 2 WSPathsNOn G C → ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C
17 16 impd ⊢ G ∈ USHGraph ∧ A ∈ V ∧ C ∈ V → W ∈ A 2 WWalksNOn G C ∧ ∃ b b A SPathsOn ⁡ G C W → W ∈ A 2 WSPathsNOn G C → ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C
18 17 com23 ⊢ G ∈ USHGraph ∧ A ∈ V ∧ C ∈ V → W ∈ A 2 WSPathsNOn G C → W ∈ A 2 WWalksNOn G C ∧ ∃ b b A SPathsOn ⁡ G C W → ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C
19 3 18 mpdi ⊢ G ∈ USHGraph ∧ A ∈ V ∧ C ∈ V → W ∈ A 2 WSPathsNOn G C → ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C
20 7 biimpar ⊢ W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C → W ∈ A 2 WSPathsNOn G C
21 20 a1i ⊢ G ∈ USHGraph ∧ A ∈ V ∧ C ∈ V ∧ b ∈ V → W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C → W ∈ A 2 WSPathsNOn G C
22 21 rexlimdva ⊢ G ∈ USHGraph ∧ A ∈ V ∧ C ∈ V → ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C → W ∈ A 2 WSPathsNOn G C
23 19 22 impbid ⊢ G ∈ USHGraph ∧ A ∈ V ∧ C ∈ V → W ∈ A 2 WSPathsNOn G C ↔ ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C