# Metamath Proof Explorer

Description: Lemma for umgr2adedgwlk , umgr2adedgspth , etc. (Contributed by Alexander van der Vekens, 1-Feb-2018) (Revised by AV, 29-Jan-2021)

Ref Expression
Hypothesis umgr2adedgwlk.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
Assertion umgr2adedgwlklem ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\to \left(\left({A}\ne {B}\wedge {B}\ne {C}\right)\wedge \left({A}\in \mathrm{Vtx}\left({G}\right)\wedge {B}\in \mathrm{Vtx}\left({G}\right)\wedge {C}\in \mathrm{Vtx}\left({G}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 umgr2adedgwlk.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
2 1 umgredgne ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\right)\to {A}\ne {B}$
3 2 ex ${⊢}{G}\in \mathrm{UMGraph}\to \left(\left\{{A},{B}\right\}\in {E}\to {A}\ne {B}\right)$
4 1 umgredgne ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left\{{B},{C}\right\}\in {E}\right)\to {B}\ne {C}$
5 4 ex ${⊢}{G}\in \mathrm{UMGraph}\to \left(\left\{{B},{C}\right\}\in {E}\to {B}\ne {C}\right)$
6 3 5 anim12d ${⊢}{G}\in \mathrm{UMGraph}\to \left(\left(\left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\to \left({A}\ne {B}\wedge {B}\ne {C}\right)\right)$
7 6 3impib ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\to \left({A}\ne {B}\wedge {B}\ne {C}\right)$
8 eqid ${⊢}\mathrm{Vtx}\left({G}\right)=\mathrm{Vtx}\left({G}\right)$
9 8 1 umgrpredgv ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\right)\to \left({A}\in \mathrm{Vtx}\left({G}\right)\wedge {B}\in \mathrm{Vtx}\left({G}\right)\right)$
10 9 simpld ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\right)\to {A}\in \mathrm{Vtx}\left({G}\right)$
11 10 3adant3 ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\to {A}\in \mathrm{Vtx}\left({G}\right)$
12 8 1 umgrpredgv ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left\{{B},{C}\right\}\in {E}\right)\to \left({B}\in \mathrm{Vtx}\left({G}\right)\wedge {C}\in \mathrm{Vtx}\left({G}\right)\right)$
13 12 simpld ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left\{{B},{C}\right\}\in {E}\right)\to {B}\in \mathrm{Vtx}\left({G}\right)$
14 13 3adant2 ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\to {B}\in \mathrm{Vtx}\left({G}\right)$
15 12 simprd ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left\{{B},{C}\right\}\in {E}\right)\to {C}\in \mathrm{Vtx}\left({G}\right)$
16 15 3adant2 ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\to {C}\in \mathrm{Vtx}\left({G}\right)$
17 11 14 16 3jca ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\to \left({A}\in \mathrm{Vtx}\left({G}\right)\wedge {B}\in \mathrm{Vtx}\left({G}\right)\wedge {C}\in \mathrm{Vtx}\left({G}\right)\right)$
18 7 17 jca ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left\{{A},{B}\right\}\in {E}\wedge \left\{{B},{C}\right\}\in {E}\right)\to \left(\left({A}\ne {B}\wedge {B}\ne {C}\right)\wedge \left({A}\in \mathrm{Vtx}\left({G}\right)\wedge {B}\in \mathrm{Vtx}\left({G}\right)\wedge {C}\in \mathrm{Vtx}\left({G}\right)\right)\right)$