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 ) |