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

Metamath Proof Explorer

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 )