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 ⊢V=Vtx⁡G
usgr2wspthon0.e ⊢E=Edg⁡G
Assertion usgr2wspthon ⊢G∈USGraph∧A∈V∧C∈V→T∈A2WSPathsNOnGC↔∃b∈VT=⟨“AbC”⟩∧A≠C∧Ab∈E∧bC∈E

Proof

Step Hyp Ref Expression
1 usgr2wspthon0.v ⊢V=Vtx⁡G
2 usgr2wspthon0.e ⊢E=Edg⁡G
3 usgrupgr ⊢G∈USGraph→G∈UPGraph
4 3 adantr ⊢G∈USGraph∧A∈V∧C∈V→G∈UPGraph
5 simpl ⊢A∈V∧C∈V→A∈V
6 5 adantl ⊢G∈USGraph∧A∈V∧C∈V→A∈V
7 simpr ⊢A∈V∧C∈V→C∈V
8 7 adantl ⊢G∈USGraph∧A∈V∧C∈V→C∈V
9 1 elwspths2on ⊢G∈UPGraph∧A∈V∧C∈V→T∈A2WSPathsNOnGC↔∃b∈VT=⟨“AbC”⟩∧⟨“AbC”⟩∈A2WSPathsNOnGC
10 4 6 8 9 syl3anc ⊢G∈USGraph∧A∈V∧C∈V→T∈A2WSPathsNOnGC↔∃b∈VT=⟨“AbC”⟩∧⟨“AbC”⟩∈A2WSPathsNOnGC
11 simpl ⊢G∈USGraph∧A∈V∧C∈V→G∈USGraph
12 11 adantr ⊢G∈USGraph∧A∈V∧C∈V∧b∈V→G∈USGraph
13 simplrl ⊢G∈USGraph∧A∈V∧C∈V∧b∈V→A∈V
14 simpr ⊢G∈USGraph∧A∈V∧C∈V∧b∈V→b∈V
15 simplrr ⊢G∈USGraph∧A∈V∧C∈V∧b∈V→C∈V
16 1 2 usgr2wspthons3 ⊢G∈USGraph∧A∈V∧b∈V∧C∈V→⟨“AbC”⟩∈A2WSPathsNOnGC↔A≠C∧Ab∈E∧bC∈E
17 12 13 14 15 16 syl13anc ⊢G∈USGraph∧A∈V∧C∈V∧b∈V→⟨“AbC”⟩∈A2WSPathsNOnGC↔A≠C∧Ab∈E∧bC∈E
18 17 anbi2d ⊢G∈USGraph∧A∈V∧C∈V∧b∈V→T=⟨“AbC”⟩∧⟨“AbC”⟩∈A2WSPathsNOnGC↔T=⟨“AbC”⟩∧A≠C∧Ab∈E∧bC∈E
19 anass ⊢T=⟨“AbC”⟩∧A≠C∧Ab∈E∧bC∈E↔T=⟨“AbC”⟩∧A≠C∧Ab∈E∧bC∈E
20 3anass ⊢A≠C∧Ab∈E∧bC∈E↔A≠C∧Ab∈E∧bC∈E
21 20 bicomi ⊢A≠C∧Ab∈E∧bC∈E↔A≠C∧Ab∈E∧bC∈E
22 21 anbi2i ⊢T=⟨“AbC”⟩∧A≠C∧Ab∈E∧bC∈E↔T=⟨“AbC”⟩∧A≠C∧Ab∈E∧bC∈E
23 19 22 bitri ⊢T=⟨“AbC”⟩∧A≠C∧Ab∈E∧bC∈E↔T=⟨“AbC”⟩∧A≠C∧Ab∈E∧bC∈E
24 18 23 bitr4di ⊢G∈USGraph∧A∈V∧C∈V∧b∈V→T=⟨“AbC”⟩∧⟨“AbC”⟩∈A2WSPathsNOnGC↔T=⟨“AbC”⟩∧A≠C∧Ab∈E∧bC∈E
25 24 rexbidva ⊢G∈USGraph∧A∈V∧C∈V→∃b∈VT=⟨“AbC”⟩∧⟨“AbC”⟩∈A2WSPathsNOnGC↔∃b∈VT=⟨“AbC”⟩∧A≠C∧Ab∈E∧bC∈E
26 10 25 bitrd ⊢G∈USGraph∧A∈V∧C∈V→T∈A2WSPathsNOnGC↔∃b∈VT=⟨“AbC”⟩∧A≠C∧Ab∈E∧bC∈E