Theorem 2wspdisj

Description: All simple paths of length 2 from a fixed vertex to another vertex are disjunct. (Contributed by Alexander van der Vekens, 4-Mar-2018) (Revised by AV, 9-Jan-2022)

	Ref	Expression
Assertion	2wspdisj	|- Disj_ b e. ( V \ { A } ) ( A ( 2 WSPathsNOn G ) b )

Proof

Step	Hyp	Ref	Expression
1		oveq2	|- ( b = c -> ( A ( 2 WSPathsNOn G ) b ) = ( A ( 2 WSPathsNOn G ) c ) )
2		wspthneq1eq2	|- ( ( t e. ( A ( 2 WSPathsNOn G ) b ) /\ t e. ( A ( 2 WSPathsNOn G ) c ) ) -> ( A = A /\ b = c ) )
3	2	simprd	|- ( ( t e. ( A ( 2 WSPathsNOn G ) b ) /\ t e. ( A ( 2 WSPathsNOn G ) c ) ) -> b = c )
4	3	3adant1	|- ( ( T. /\ t e. ( A ( 2 WSPathsNOn G ) b ) /\ t e. ( A ( 2 WSPathsNOn G ) c ) ) -> b = c )
5	1 4	disjord	|- ( T. -> Disj_ b e. ( V \ { A } ) ( A ( 2 WSPathsNOn G ) b ) )
6	5	mptru	|- Disj_ b e. ( V \ { A } ) ( A ( 2 WSPathsNOn G ) b )