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)

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 usgrupgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UPGraph )
4 3 adantr ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐺 ∈ UPGraph )
5 simpl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 )
6 5 adantl ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐴 ∈ 𝑉 )
7 simpr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → 𝐶 ∈ 𝑉 )
8 7 adantl ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐶 ∈ 𝑉 )
9 1 elwspths2on ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝑇 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ↔ ∃ 𝑏 ∈ 𝑉 ( 𝑇 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) )
10 4 6 8 9 syl3anc ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝑇 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ↔ ∃ 𝑏 ∈ 𝑉 ( 𝑇 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ) )
11 simpl ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐺 ∈ USGraph )
12 11 adantr ⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ 𝑏 ∈ 𝑉 ) → 𝐺 ∈ USGraph )
13 simplrl ⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ 𝑏 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 )
14 simpr ⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ 𝑏 ∈ 𝑉 ) → 𝑏 ∈ 𝑉 )
15 simplrr ⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ 𝑏 ∈ 𝑉 ) → 𝐶 ∈ 𝑉 )
16 1 2 usgr2wspthons3 ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ↔ ( 𝐴 ≠ 𝐶 ∧ { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) )
17 12 13 14 15 16 syl13anc ⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ 𝑏 ∈ 𝑉 ) → ( ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ↔ ( 𝐴 ≠ 𝐶 ∧ { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) )
18 17 anbi2d ⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ 𝑏 ∈ 𝑉 ) → ( ( 𝑇 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ↔ ( 𝑇 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ( 𝐴 ≠ 𝐶 ∧ { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) ) )
19 anass ⊢ ( ( ( 𝑇 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ 𝐴 ≠ 𝐶 ) ∧ ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) ↔ ( 𝑇 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ( 𝐴 ≠ 𝐶 ∧ ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) ) )
20 3anass ⊢ ( ( 𝐴 ≠ 𝐶 ∧ { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ↔ ( 𝐴 ≠ 𝐶 ∧ ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) )
21 20 bicomi ⊢ ( ( 𝐴 ≠ 𝐶 ∧ ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) ↔ ( 𝐴 ≠ 𝐶 ∧ { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) )
22 21 anbi2i ⊢ ( ( 𝑇 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ( 𝐴 ≠ 𝐶 ∧ ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) ) ↔ ( 𝑇 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ( 𝐴 ≠ 𝐶 ∧ { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) )
23 19 22 bitri ⊢ ( ( ( 𝑇 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ 𝐴 ≠ 𝐶 ) ∧ ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) ↔ ( 𝑇 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ( 𝐴 ≠ 𝐶 ∧ { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) )
24 18 23 bitr4di ⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ 𝑏 ∈ 𝑉 ) → ( ( 𝑇 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ↔ ( ( 𝑇 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ 𝐴 ≠ 𝐶 ) ∧ ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) ) )
25 24 rexbidva ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ∃ 𝑏 ∈ 𝑉 ( 𝑇 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ) ↔ ∃ 𝑏 ∈ 𝑉 ( ( 𝑇 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ 𝐴 ≠ 𝐶 ) ∧ ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) ) )
26 10 25 bitrd ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝑇 ∈ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐶 ) ↔ ∃ 𝑏 ∈ 𝑉 ( ( 𝑇 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ 𝐴 ≠ 𝐶 ) ∧ ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) ) )