This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) ) )