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 )