Metamath Proof Explorer

Theorem 2wspiundisj

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

Ref Expression
Assertion 2wspiundisj 
|- Disj_ a e. V U_ b e. ( V \ { a } ) ( a ( 2 WSPathsNOn G ) b )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( a = c -> ( a ( 2 WSPathsNOn G ) b ) = ( c ( 2 WSPathsNOn G ) b ) )
2 oveq2 
 |-  ( b = d -> ( c ( 2 WSPathsNOn G ) b ) = ( c ( 2 WSPathsNOn G ) d ) )
3 sneq 
 |-  ( a = c -> { a } = { c } )
4 3 difeq2d 
 |-  ( a = c -> ( V \ { a } ) = ( V \ { c } ) )
5 wspthneq1eq2 
 |-  ( ( t e. ( a ( 2 WSPathsNOn G ) b ) /\ t e. ( c ( 2 WSPathsNOn G ) d ) ) -> ( a = c /\ b = d ) )
6 5 simpld 
 |-  ( ( t e. ( a ( 2 WSPathsNOn G ) b ) /\ t e. ( c ( 2 WSPathsNOn G ) d ) ) -> a = c )
7 6 3adant1 
 |-  ( ( T. /\ t e. ( a ( 2 WSPathsNOn G ) b ) /\ t e. ( c ( 2 WSPathsNOn G ) d ) ) -> a = c )
8 1 2 4 7 disjiund 
 |-  ( T. -> Disj_ a e. V U_ b e. ( V \ { a } ) ( a ( 2 WSPathsNOn G ) b ) )
9 8 mptru 
 |-  Disj_ a e. V U_ b e. ( V \ { a } ) ( a ( 2 WSPathsNOn G ) b )