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 𝑉 = ( Vtx ‘ 𝐺 )
Assertion elwspths2on ( ( 𝐺 ∈ UPGraph ∧ 𝐴𝑉𝐶𝑉 ) → ( 𝑊 ∈ ( 𝐴 ( 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 elwwlks2on ( ( 𝐺 ∈ UPGraph ∧ 𝐴𝑉𝐶𝑉 ) → ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ↔ ∃ 𝑏𝑉 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) ) )
5 simpl ( ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) → 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ )
6 eleq1 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ → ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ↔ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) )
7 6 biimpa ( ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) → ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) )
8 5 7 jca ( ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) → ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) )
9 8 ex ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ → ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) )
10 9 adantr ( ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) )
11 10 com12 ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ( ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) )
12 11 reximdv ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ( ∃ 𝑏𝑉 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ∃ 𝑏𝑉 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) )
13 12 a1i13 ( ( 𝐺 ∈ UPGraph ∧ 𝐴𝑉𝐶𝑉 ) → ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ( ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐶 ) 𝑊 → ( ∃ 𝑏𝑉 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ∃ 𝑏𝑉 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) ) ) )
14 13 com24 ( ( 𝐺 ∈ UPGraph ∧ 𝐴𝑉𝐶𝑉 ) → ( ∃ 𝑏𝑉 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐶 ) 𝑊 → ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ∃ 𝑏𝑉 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) ) ) )
15 4 14 sylbid ( ( 𝐺 ∈ UPGraph ∧ 𝐴𝑉𝐶𝑉 ) → ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) → ( ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐶 ) 𝑊 → ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ∃ 𝑏𝑉 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) ) ) )
16 15 impd ( ( 𝐺 ∈ UPGraph ∧ 𝐴𝑉𝐶𝑉 ) → ( ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐶 ) 𝑊 ) → ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ∃ 𝑏𝑉 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) ) )
17 16 com23 ( ( 𝐺 ∈ UPGraph ∧ 𝐴𝑉𝐶𝑉 ) → ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ( ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐶 ) 𝑊 ) → ∃ 𝑏𝑉 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) ) )
18 3 17 mpdi ( ( 𝐺 ∈ UPGraph ∧ 𝐴𝑉𝐶𝑉 ) → ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) → ∃ 𝑏𝑉 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) )
19 6 biimpar ( ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) → 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) )
20 19 a1i ( ( ( 𝐺 ∈ UPGraph ∧ 𝐴𝑉𝐶𝑉 ) ∧ 𝑏𝑉 ) → ( ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) → 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) )
21 20 rexlimdva ( ( 𝐺 ∈ UPGraph ∧ 𝐴𝑉𝐶𝑉 ) → ( ∃ 𝑏𝑉 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) → 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) )
22 18 21 impbid ( ( 𝐺 ∈ UPGraph ∧ 𝐴𝑉𝐶𝑉 ) → ( 𝑊 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ↔ ∃ 𝑏𝑉 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) )