Metamath Proof Explorer

Theorem usgr2wspthon

Description: A simple path of length 2 between two vertices corresponds to two adjacent edges in a simple graph. (Contributed by Alexander van der Vekens, 9-Mar-2018) (Revised by AV, 17-May-2021) (Revised by Ender Ting, 29-Jan-2026)

Ref Expression
Hypotheses usgr2wspthon0.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
usgr2wspthon0.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion usgr2wspthon ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝑇 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ↔ ∃ 𝑏 ∈ 𝑉 ( ( 𝑇 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ 𝐴 ≠ 𝐶 ) ∧ ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) ) )

Proof

Step Hyp Ref Expression
1 usgr2wspthon0.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 usgr2wspthon0.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 usgruspgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ USPGraph )
4 3 adantr ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐺 ∈ USPGraph )
5 simprl ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐴 ∈ 𝑉 )
6 simprr ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐶 ∈ 𝑉 )
7 1 elwspths2onw ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝑇 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ↔ ∃ 𝑏 ∈ 𝑉 ( 𝑇 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) )
8 4 5 6 7 syl3anc ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝑇 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ↔ ∃ 𝑏 ∈ 𝑉 ( 𝑇 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) )
9 simpl ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐺 ∈ USGraph )
10 9 adantr ⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ 𝑏 ∈ 𝑉 ) → 𝐺 ∈ USGraph )
11 simplrl ⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ 𝑏 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 )
12 simpr ⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ 𝑏 ∈ 𝑉 ) → 𝑏 ∈ 𝑉 )
13 simplrr ⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ 𝑏 ∈ 𝑉 ) → 𝐶 ∈ 𝑉 )
14 1 2 usgr2wspthons3 ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ↔ ( 𝐴 ≠ 𝐶 ∧ { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) )
15 10 11 12 13 14 syl13anc ⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ 𝑏 ∈ 𝑉 ) → ( ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ↔ ( 𝐴 ≠ 𝐶 ∧ { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) )
16 15 anbi2d ⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ 𝑏 ∈ 𝑉 ) → ( ( 𝑇 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ↔ ( 𝑇 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ( 𝐴 ≠ 𝐶 ∧ { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) ) )
17 anass ⊢ ( ( ( 𝑇 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ 𝐴 ≠ 𝐶 ) ∧ ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) ↔ ( 𝑇 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ( 𝐴 ≠ 𝐶 ∧ ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) ) )
18 3anass ⊢ ( ( 𝐴 ≠ 𝐶 ∧ { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ↔ ( 𝐴 ≠ 𝐶 ∧ ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) )
19 18 bicomi ⊢ ( ( 𝐴 ≠ 𝐶 ∧ ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) ↔ ( 𝐴 ≠ 𝐶 ∧ { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) )
20 19 anbi2i ⊢ ( ( 𝑇 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ( 𝐴 ≠ 𝐶 ∧ ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) ) ↔ ( 𝑇 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ( 𝐴 ≠ 𝐶 ∧ { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) )
21 17 20 bitri ⊢ ( ( ( 𝑇 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ 𝐴 ≠ 𝐶 ) ∧ ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) ↔ ( 𝑇 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ( 𝐴 ≠ 𝐶 ∧ { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) )
22 16 21 bitr4di ⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ 𝑏 ∈ 𝑉 ) → ( ( 𝑇 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ↔ ( ( 𝑇 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ 𝐴 ≠ 𝐶 ) ∧ ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) ) )
23 22 rexbidva ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ∃ 𝑏 ∈ 𝑉 ( 𝑇 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ↔ ∃ 𝑏 ∈ 𝑉 ( ( 𝑇 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ 𝐴 ≠ 𝐶 ) ∧ ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) ) )
24 8 23 bitrd ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝑇 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ↔ ∃ 𝑏 ∈ 𝑉 ( ( 𝑇 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ 𝐴 ≠ 𝐶 ) ∧ ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) ) )