umgr2adedgwlkon

Description: In a multigraph, two adjacent edges form a walk between two vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018) (Revised by AV, 30-Jan-2021)

	Ref	Expression
Hypotheses	umgr2adedgwlk.e	\|- E = ( Edg ` G )
	umgr2adedgwlk.i	\|- I = ( iEdg ` G )
	umgr2adedgwlk.f	\|- F = <" J K ">
	umgr2adedgwlk.p	\|- P = <" A B C ">
	umgr2adedgwlk.g	\|- ( ph -> G e. UMGraph )
	umgr2adedgwlk.a	\|- ( ph -> ( { A , B } e. E /\ { B , C } e. E ) )
	umgr2adedgwlk.j	\|- ( ph -> ( I ` J ) = { A , B } )
	umgr2adedgwlk.k	\|- ( ph -> ( I ` K ) = { B , C } )
Assertion	umgr2adedgwlkon	\|- ( ph -> F ( A ( WalksOn ` G ) C ) P )

Proof

Step	Hyp	Ref	Expression
1		umgr2adedgwlk.e	\|- E = ( Edg ` G )
2		umgr2adedgwlk.i	\|- I = ( iEdg ` G )
3		umgr2adedgwlk.f	\|- F = <" J K ">
4		umgr2adedgwlk.p	\|- P = <" A B C ">
5		umgr2adedgwlk.g	\|- ( ph -> G e. UMGraph )
6		umgr2adedgwlk.a	\|- ( ph -> ( { A , B } e. E /\ { B , C } e. E ) )
7		umgr2adedgwlk.j	\|- ( ph -> ( I ` J ) = { A , B } )
8		umgr2adedgwlk.k	\|- ( ph -> ( I ` K ) = { B , C } )
9		3anass	\|- ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) <-> ( G e. UMGraph /\ ( { A , B } e. E /\ { B , C } e. E ) ) )
10	5 6 9	sylanbrc	\|- ( ph -> ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) )
11	1	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 ) ) ) )
12	10 11	syl	\|- ( ph -> ( ( A =/= B /\ B =/= C ) /\ ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) ) )
13	12	simprd	\|- ( ph -> ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) /\ C e. ( Vtx ` G ) ) )
14	12	simpld	\|- ( ph -> ( A =/= B /\ B =/= C ) )
15		ssid	\|- { A , B } C_ { A , B }
16	15 7	sseqtrrid	\|- ( ph -> { A , B } C_ ( I ` J ) )
17		ssid	\|- { B , C } C_ { B , C }
18	17 8	sseqtrrid	\|- ( ph -> { B , C } C_ ( I ` K ) )
19	16 18	jca	\|- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) ) )
20		eqid	\|- ( Vtx ` G ) = ( Vtx ` G )
21	4 3 13 14 19 20 2	2wlkond	\|- ( ph -> F ( A ( WalksOn ` G ) C ) P )

Metamath Proof Explorer

Theorem umgr2adedgwlkon

Proof