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