Metamath Proof Explorer

Theorem elwspths2on

Description: A simple path of length 2 between two vertices (in a graph) as length 3 string. (Contributed by Alexander van der Vekens, 9-Mar-2018) (Revised by AV, 12-May-2021) (Proof shortened by AV, 16-Mar-2022)

Ref Expression
Hypothesis elwwlks2on.v ⊢ V = Vtx ⁡ G
Assertion elwspths2on ⊢ G ∈ UPGraph ∧ 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 ∧ ∃ f f A SPathsOn ⁡ G C W
3 2 biimpi ⊢ W ∈ A 2 WSPathsNOn G C → W ∈ A 2 WWalksNOn G C ∧ ∃ f f A SPathsOn ⁡ G C W
4 1 elwwlks2on ⊢ G ∈ UPGraph ∧ A ∈ V ∧ C ∈ V → W ∈ A 2 WWalksNOn G C ↔ ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ∃ f f Walks ⁡ G W ∧ f = 2
5 simpl ⊢ W = ⟨“ AbC ”⟩ ∧ W ∈ A 2 WSPathsNOn G C → W = ⟨“ AbC ”⟩
6 eleq1 ⊢ W = ⟨“ AbC ”⟩ → W ∈ A 2 WSPathsNOn G C ↔ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C
7 6 biimpa ⊢ W = ⟨“ AbC ”⟩ ∧ W ∈ A 2 WSPathsNOn G C → ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C
8 5 7 jca ⊢ W = ⟨“ AbC ”⟩ ∧ W ∈ A 2 WSPathsNOn G C → W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C
9 8 ex ⊢ W = ⟨“ AbC ”⟩ → W ∈ A 2 WSPathsNOn G C → W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C
10 9 adantr ⊢ W = ⟨“ AbC ”⟩ ∧ ∃ f f Walks ⁡ G W ∧ f = 2 → W ∈ A 2 WSPathsNOn G C → W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C
11 10 com12 ⊢ W ∈ A 2 WSPathsNOn G C → W = ⟨“ AbC ”⟩ ∧ ∃ f f Walks ⁡ G W ∧ f = 2 → W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C
12 11 reximdv ⊢ W ∈ A 2 WSPathsNOn G C → ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ∃ f f Walks ⁡ G W ∧ f = 2 → ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C
13 12 a1i13 ⊢ G ∈ UPGraph ∧ A ∈ V ∧ C ∈ V → W ∈ A 2 WSPathsNOn G C → ∃ f f A SPathsOn ⁡ G C W → ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ∃ f f Walks ⁡ G W ∧ f = 2 → ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C
14 13 com24 ⊢ G ∈ UPGraph ∧ A ∈ V ∧ C ∈ V → ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ∃ f f Walks ⁡ G W ∧ f = 2 → ∃ f f A SPathsOn ⁡ G C W → W ∈ A 2 WSPathsNOn G C → ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C
15 4 14 sylbid ⊢ G ∈ UPGraph ∧ A ∈ V ∧ C ∈ V → W ∈ A 2 WWalksNOn G C → ∃ f f A SPathsOn ⁡ G C W → W ∈ A 2 WSPathsNOn G C → ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C
16 15 impd ⊢ G ∈ UPGraph ∧ A ∈ V ∧ C ∈ V → W ∈ A 2 WWalksNOn G C ∧ ∃ f f A SPathsOn ⁡ G C W → W ∈ A 2 WSPathsNOn G C → ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C
17 16 com23 ⊢ G ∈ UPGraph ∧ A ∈ V ∧ C ∈ V → W ∈ A 2 WSPathsNOn G C → W ∈ A 2 WWalksNOn G C ∧ ∃ f f A SPathsOn ⁡ G C W → ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C
18 3 17 mpdi ⊢ G ∈ UPGraph ∧ A ∈ V ∧ C ∈ V → W ∈ A 2 WSPathsNOn G C → ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C
19 6 biimpar ⊢ W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C → W ∈ A 2 WSPathsNOn G C
20 19 a1i ⊢ G ∈ UPGraph ∧ A ∈ V ∧ C ∈ V ∧ b ∈ V → W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C → W ∈ A 2 WSPathsNOn G C
21 20 rexlimdva ⊢ G ∈ UPGraph ∧ A ∈ V ∧ C ∈ V → ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C → W ∈ A 2 WSPathsNOn G C
22 18 21 impbid ⊢ G ∈ UPGraph ∧ A ∈ V ∧ C ∈ V → W ∈ A 2 WSPathsNOn G C ↔ ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WSPathsNOn G C