Metamath Proof Explorer


Theorem umgr2adedgwlklem

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 = ( Edg ` G )
Assertion umgr2adedgwlklem
|- ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) -> ( ( A =/= B /\ B =/= C ) /\ ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) ) )

Proof

Step Hyp Ref Expression
1 umgr2adedgwlk.e
 |-  E = ( Edg ` G )
2 1 umgredgne
 |-  ( ( G e. UMGraph /\ { A , B } e. E ) -> A =/= B )
3 2 ex
 |-  ( G e. UMGraph -> ( { A , B } e. E -> A =/= B ) )
4 1 umgredgne
 |-  ( ( G e. UMGraph /\ { B , C } e. E ) -> B =/= C )
5 4 ex
 |-  ( G e. UMGraph -> ( { B , C } e. E -> B =/= C ) )
6 3 5 anim12d
 |-  ( G e. UMGraph -> ( ( { A , B } e. E /\ { B , C } e. E ) -> ( A =/= B /\ B =/= C ) ) )
7 6 3impib
 |-  ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) -> ( A =/= B /\ B =/= C ) )
8 eqid
 |-  ( Vtx ` G ) = ( Vtx ` G )
9 8 1 umgrpredgv
 |-  ( ( G e. UMGraph /\ { A , B } e. E ) -> ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) )
10 9 simpld
 |-  ( ( G e. UMGraph /\ { A , B } e. E ) -> A e. ( Vtx ` G ) )
11 10 3adant3
 |-  ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) -> A e. ( Vtx ` G ) )
12 8 1 umgrpredgv
 |-  ( ( G e. UMGraph /\ { B , C } e. E ) -> ( B e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) )
13 12 simpld
 |-  ( ( G e. UMGraph /\ { B , C } e. E ) -> B e. ( Vtx ` G ) )
14 13 3adant2
 |-  ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) -> B e. ( Vtx ` G ) )
15 12 simprd
 |-  ( ( G e. UMGraph /\ { B , C } e. E ) -> C e. ( Vtx ` G ) )
16 15 3adant2
 |-  ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) -> C e. ( Vtx ` G ) )
17 11 14 16 3jca
 |-  ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) -> ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) )
18 7 17 jca
 |-  ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) -> ( ( A =/= B /\ B =/= C ) /\ ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) ) )