3pthond

Description: A path of length 3 from one vertex to another, different vertex via a third vertex. (Contributed by AV, 10-Feb-2021) (Revised by AV, 24-Mar-2021)

	Ref	Expression
Hypotheses	3wlkd.p	\|- P = <" A B C D ">
	3wlkd.f	\|- F = <" J K L ">
	3wlkd.s	\|- ( ph -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) )
	3wlkd.n	\|- ( ph -> ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) )
	3wlkd.e	\|- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) /\ { C , D } C_ ( I ` L ) ) )
	3wlkd.v	\|- V = ( Vtx ` G )
	3wlkd.i	\|- I = ( iEdg ` G )
	3trld.n	\|- ( ph -> ( J =/= K /\ J =/= L /\ K =/= L ) )
Assertion	3pthond	\|- ( ph -> F ( A ( PathsOn ` G ) D ) P )

Proof

Step	Hyp	Ref	Expression
1		3wlkd.p	\|- P = <" A B C D ">
2		3wlkd.f	\|- F = <" J K L ">
3		3wlkd.s	\|- ( ph -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) )
4		3wlkd.n	\|- ( ph -> ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) )
5		3wlkd.e	\|- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) /\ { C , D } C_ ( I ` L ) ) )
6		3wlkd.v	\|- V = ( Vtx ` G )
7		3wlkd.i	\|- I = ( iEdg ` G )
8		3trld.n	\|- ( ph -> ( J =/= K /\ J =/= L /\ K =/= L ) )
9	1 2 3 4 5 6 7 8	3trlond	\|- ( ph -> F ( A ( TrailsOn ` G ) D ) P )
10	1 2 3 4 5 6 7 8	3pthd	\|- ( ph -> F ( Paths ` G ) P )
11	3	simplld	\|- ( ph -> A e. V )
12	3	simprrd	\|- ( ph -> D e. V )
13		s3cli	\|- <" J K L "> e. Word _V
14	2 13	eqeltri	\|- F e. Word _V
15		s4cli	\|- <" A B C D "> e. Word _V
16	1 15	eqeltri	\|- P e. Word _V
17	14 16	pm3.2i	\|- ( F e. Word _V /\ P e. Word _V )
18	17	a1i	\|- ( ph -> ( F e. Word _V /\ P e. Word _V ) )
19	6	ispthson	\|- ( ( ( A e. V /\ D e. V ) /\ ( F e. Word _V /\ P e. Word _V ) ) -> ( F ( A ( PathsOn ` G ) D ) P <-> ( F ( A ( TrailsOn ` G ) D ) P /\ F ( Paths ` G ) P ) ) )
20	11 12 18 19	syl21anc	\|- ( ph -> ( F ( A ( PathsOn ` G ) D ) P <-> ( F ( A ( TrailsOn ` G ) D ) P /\ F ( Paths ` G ) P ) ) )
21	9 10 20	mpbir2and	\|- ( ph -> F ( A ( PathsOn ` G ) D ) P )

Metamath Proof Explorer

Theorem 3pthond

Proof