# 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}=\mathrm{Vtx}\left({G}\right)$
usgr2wspthon0.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
Assertion usgr2wspthon ${⊢}\left({G}\in \mathrm{USGraph}\wedge \left({A}\in {V}\wedge {C}\in {V}\right)\right)\to \left({T}\in \left({A}\left(2\mathrm{WSPathsNOn}{G}\right){C}\right)↔\exists {b}\in {V}\phantom{\rule{.4em}{0ex}}\left(\left({T}=⟨“{A}{b}{C}”⟩\wedge {A}\ne {C}\right)\wedge \left(\left\{{A},{b}\right\}\in {E}\wedge \left\{{b},{C}\right\}\in {E}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 usgr2wspthon0.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 usgr2wspthon0.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
3 usgrupgr ${⊢}{G}\in \mathrm{USGraph}\to {G}\in \mathrm{UPGraph}$
4 3 adantr ${⊢}\left({G}\in \mathrm{USGraph}\wedge \left({A}\in {V}\wedge {C}\in {V}\right)\right)\to {G}\in \mathrm{UPGraph}$
5 simpl ${⊢}\left({A}\in {V}\wedge {C}\in {V}\right)\to {A}\in {V}$
6 5 adantl ${⊢}\left({G}\in \mathrm{USGraph}\wedge \left({A}\in {V}\wedge {C}\in {V}\right)\right)\to {A}\in {V}$
7 simpr ${⊢}\left({A}\in {V}\wedge {C}\in {V}\right)\to {C}\in {V}$
8 7 adantl ${⊢}\left({G}\in \mathrm{USGraph}\wedge \left({A}\in {V}\wedge {C}\in {V}\right)\right)\to {C}\in {V}$
9 1 elwspths2on ${⊢}\left({G}\in \mathrm{UPGraph}\wedge {A}\in {V}\wedge {C}\in {V}\right)\to \left({T}\in \left({A}\left(2\mathrm{WSPathsNOn}{G}\right){C}\right)↔\exists {b}\in {V}\phantom{\rule{.4em}{0ex}}\left({T}=⟨“{A}{b}{C}”⟩\wedge ⟨“{A}{b}{C}”⟩\in \left({A}\left(2\mathrm{WSPathsNOn}{G}\right){C}\right)\right)\right)$
10 4 6 8 9 syl3anc ${⊢}\left({G}\in \mathrm{USGraph}\wedge \left({A}\in {V}\wedge {C}\in {V}\right)\right)\to \left({T}\in \left({A}\left(2\mathrm{WSPathsNOn}{G}\right){C}\right)↔\exists {b}\in {V}\phantom{\rule{.4em}{0ex}}\left({T}=⟨“{A}{b}{C}”⟩\wedge ⟨“{A}{b}{C}”⟩\in \left({A}\left(2\mathrm{WSPathsNOn}{G}\right){C}\right)\right)\right)$
11 simpl ${⊢}\left({G}\in \mathrm{USGraph}\wedge \left({A}\in {V}\wedge {C}\in {V}\right)\right)\to {G}\in \mathrm{USGraph}$
12 11 adantr ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge \left({A}\in {V}\wedge {C}\in {V}\right)\right)\wedge {b}\in {V}\right)\to {G}\in \mathrm{USGraph}$
13 simplrl ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge \left({A}\in {V}\wedge {C}\in {V}\right)\right)\wedge {b}\in {V}\right)\to {A}\in {V}$
14 simpr ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge \left({A}\in {V}\wedge {C}\in {V}\right)\right)\wedge {b}\in {V}\right)\to {b}\in {V}$
15 simplrr ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge \left({A}\in {V}\wedge {C}\in {V}\right)\right)\wedge {b}\in {V}\right)\to {C}\in {V}$
16 1 2 usgr2wspthons3 ${⊢}\left({G}\in \mathrm{USGraph}\wedge \left({A}\in {V}\wedge {b}\in {V}\wedge {C}\in {V}\right)\right)\to \left(⟨“{A}{b}{C}”⟩\in \left({A}\left(2\mathrm{WSPathsNOn}{G}\right){C}\right)↔\left({A}\ne {C}\wedge \left\{{A},{b}\right\}\in {E}\wedge \left\{{b},{C}\right\}\in {E}\right)\right)$
17 12 13 14 15 16 syl13anc ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge \left({A}\in {V}\wedge {C}\in {V}\right)\right)\wedge {b}\in {V}\right)\to \left(⟨“{A}{b}{C}”⟩\in \left({A}\left(2\mathrm{WSPathsNOn}{G}\right){C}\right)↔\left({A}\ne {C}\wedge \left\{{A},{b}\right\}\in {E}\wedge \left\{{b},{C}\right\}\in {E}\right)\right)$
18 17 anbi2d ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge \left({A}\in {V}\wedge {C}\in {V}\right)\right)\wedge {b}\in {V}\right)\to \left(\left({T}=⟨“{A}{b}{C}”⟩\wedge ⟨“{A}{b}{C}”⟩\in \left({A}\left(2\mathrm{WSPathsNOn}{G}\right){C}\right)\right)↔\left({T}=⟨“{A}{b}{C}”⟩\wedge \left({A}\ne {C}\wedge \left\{{A},{b}\right\}\in {E}\wedge \left\{{b},{C}\right\}\in {E}\right)\right)\right)$
19 anass ${⊢}\left(\left({T}=⟨“{A}{b}{C}”⟩\wedge {A}\ne {C}\right)\wedge \left(\left\{{A},{b}\right\}\in {E}\wedge \left\{{b},{C}\right\}\in {E}\right)\right)↔\left({T}=⟨“{A}{b}{C}”⟩\wedge \left({A}\ne {C}\wedge \left(\left\{{A},{b}\right\}\in {E}\wedge \left\{{b},{C}\right\}\in {E}\right)\right)\right)$
20 3anass ${⊢}\left({A}\ne {C}\wedge \left\{{A},{b}\right\}\in {E}\wedge \left\{{b},{C}\right\}\in {E}\right)↔\left({A}\ne {C}\wedge \left(\left\{{A},{b}\right\}\in {E}\wedge \left\{{b},{C}\right\}\in {E}\right)\right)$
21 20 bicomi ${⊢}\left({A}\ne {C}\wedge \left(\left\{{A},{b}\right\}\in {E}\wedge \left\{{b},{C}\right\}\in {E}\right)\right)↔\left({A}\ne {C}\wedge \left\{{A},{b}\right\}\in {E}\wedge \left\{{b},{C}\right\}\in {E}\right)$
22 21 anbi2i ${⊢}\left({T}=⟨“{A}{b}{C}”⟩\wedge \left({A}\ne {C}\wedge \left(\left\{{A},{b}\right\}\in {E}\wedge \left\{{b},{C}\right\}\in {E}\right)\right)\right)↔\left({T}=⟨“{A}{b}{C}”⟩\wedge \left({A}\ne {C}\wedge \left\{{A},{b}\right\}\in {E}\wedge \left\{{b},{C}\right\}\in {E}\right)\right)$
23 19 22 bitri ${⊢}\left(\left({T}=⟨“{A}{b}{C}”⟩\wedge {A}\ne {C}\right)\wedge \left(\left\{{A},{b}\right\}\in {E}\wedge \left\{{b},{C}\right\}\in {E}\right)\right)↔\left({T}=⟨“{A}{b}{C}”⟩\wedge \left({A}\ne {C}\wedge \left\{{A},{b}\right\}\in {E}\wedge \left\{{b},{C}\right\}\in {E}\right)\right)$
24 18 23 syl6bbr ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge \left({A}\in {V}\wedge {C}\in {V}\right)\right)\wedge {b}\in {V}\right)\to \left(\left({T}=⟨“{A}{b}{C}”⟩\wedge ⟨“{A}{b}{C}”⟩\in \left({A}\left(2\mathrm{WSPathsNOn}{G}\right){C}\right)\right)↔\left(\left({T}=⟨“{A}{b}{C}”⟩\wedge {A}\ne {C}\right)\wedge \left(\left\{{A},{b}\right\}\in {E}\wedge \left\{{b},{C}\right\}\in {E}\right)\right)\right)$
25 24 rexbidva ${⊢}\left({G}\in \mathrm{USGraph}\wedge \left({A}\in {V}\wedge {C}\in {V}\right)\right)\to \left(\exists {b}\in {V}\phantom{\rule{.4em}{0ex}}\left({T}=⟨“{A}{b}{C}”⟩\wedge ⟨“{A}{b}{C}”⟩\in \left({A}\left(2\mathrm{WSPathsNOn}{G}\right){C}\right)\right)↔\exists {b}\in {V}\phantom{\rule{.4em}{0ex}}\left(\left({T}=⟨“{A}{b}{C}”⟩\wedge {A}\ne {C}\right)\wedge \left(\left\{{A},{b}\right\}\in {E}\wedge \left\{{b},{C}\right\}\in {E}\right)\right)\right)$
26 10 25 bitrd ${⊢}\left({G}\in \mathrm{USGraph}\wedge \left({A}\in {V}\wedge {C}\in {V}\right)\right)\to \left({T}\in \left({A}\left(2\mathrm{WSPathsNOn}{G}\right){C}\right)↔\exists {b}\in {V}\phantom{\rule{.4em}{0ex}}\left(\left({T}=⟨“{A}{b}{C}”⟩\wedge {A}\ne {C}\right)\wedge \left(\left\{{A},{b}\right\}\in {E}\wedge \left\{{b},{C}\right\}\in {E}\right)\right)\right)$