This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐺 ) 𝐶 ) ) ) )