Metamath Proof Explorer

Theorem 2wspmdisj

Description: The sets of paths of length 2 with a given vertex in the middle are distinct for different vertices in the middle. (Contributed by Alexander van der Vekens, 11-Mar-2018) (Revised by AV, 18-May-2021) (Proof shortened by AV, 10-Jan-2022)

Ref Expression
Hypotheses frgrhash2wsp.v 
|- V = ( Vtx ` G )
fusgreg2wsp.m 
|- M = ( a e. V |-> { w e. ( 2 WSPathsN G ) | ( w ` 1 ) = a } )
Assertion 2wspmdisj 
|- Disj_ x e. V ( M ` x )

Proof

Step Hyp Ref Expression
1 frgrhash2wsp.v 
 |-  V = ( Vtx ` G )
2 fusgreg2wsp.m 
 |-  M = ( a e. V |-> { w e. ( 2 WSPathsN G ) | ( w ` 1 ) = a } )
3 orc 
 |-  ( x = y -> ( x = y \/ ( ( M ` x ) i^i ( M ` y ) ) = (/) ) )
4 3 a1d 
 |-  ( x = y -> ( ( x e. V /\ y e. V ) -> ( x = y \/ ( ( M ` x ) i^i ( M ` y ) ) = (/) ) ) )
5 1 2 fusgreg2wsplem 
 |-  ( y e. V -> ( t e. ( M ` y ) <-> ( t e. ( 2 WSPathsN G ) /\ ( t ` 1 ) = y ) ) )
6 5 adantl 
 |-  ( ( x e. V /\ y e. V ) -> ( t e. ( M ` y ) <-> ( t e. ( 2 WSPathsN G ) /\ ( t ` 1 ) = y ) ) )
7 6 adantr 
 |-  ( ( ( x e. V /\ y e. V ) /\ t e. ( M ` x ) ) -> ( t e. ( M ` y ) <-> ( t e. ( 2 WSPathsN G ) /\ ( t ` 1 ) = y ) ) )
8 1 2 fusgreg2wsplem 
 |-  ( x e. V -> ( t e. ( M ` x ) <-> ( t e. ( 2 WSPathsN G ) /\ ( t ` 1 ) = x ) ) )
9 eqtr2 
 |-  ( ( ( t ` 1 ) = x /\ ( t ` 1 ) = y ) -> x = y )
10 9 expcom 
 |-  ( ( t ` 1 ) = y -> ( ( t ` 1 ) = x -> x = y ) )
11 10 adantl 
 |-  ( ( t e. ( 2 WSPathsN G ) /\ ( t ` 1 ) = y ) -> ( ( t ` 1 ) = x -> x = y ) )
12 11 com12 
 |-  ( ( t ` 1 ) = x -> ( ( t e. ( 2 WSPathsN G ) /\ ( t ` 1 ) = y ) -> x = y ) )
13 12 adantl 
 |-  ( ( t e. ( 2 WSPathsN G ) /\ ( t ` 1 ) = x ) -> ( ( t e. ( 2 WSPathsN G ) /\ ( t ` 1 ) = y ) -> x = y ) )
14 8 13 biimtrdi 
 |-  ( x e. V -> ( t e. ( M ` x ) -> ( ( t e. ( 2 WSPathsN G ) /\ ( t ` 1 ) = y ) -> x = y ) ) )
15 14 adantr 
 |-  ( ( x e. V /\ y e. V ) -> ( t e. ( M ` x ) -> ( ( t e. ( 2 WSPathsN G ) /\ ( t ` 1 ) = y ) -> x = y ) ) )
16 15 imp 
 |-  ( ( ( x e. V /\ y e. V ) /\ t e. ( M ` x ) ) -> ( ( t e. ( 2 WSPathsN G ) /\ ( t ` 1 ) = y ) -> x = y ) )
17 7 16 sylbid 
 |-  ( ( ( x e. V /\ y e. V ) /\ t e. ( M ` x ) ) -> ( t e. ( M ` y ) -> x = y ) )
18 17 con3d 
 |-  ( ( ( x e. V /\ y e. V ) /\ t e. ( M ` x ) ) -> ( -. x = y -> -. t e. ( M ` y ) ) )
19 18 impancom 
 |-  ( ( ( x e. V /\ y e. V ) /\ -. x = y ) -> ( t e. ( M ` x ) -> -. t e. ( M ` y ) ) )
20 19 ralrimiv 
 |-  ( ( ( x e. V /\ y e. V ) /\ -. x = y ) -> A. t e. ( M ` x ) -. t e. ( M ` y ) )
21 disj 
 |-  ( ( ( M ` x ) i^i ( M ` y ) ) = (/) <-> A. t e. ( M ` x ) -. t e. ( M ` y ) )
22 20 21 sylibr 
 |-  ( ( ( x e. V /\ y e. V ) /\ -. x = y ) -> ( ( M ` x ) i^i ( M ` y ) ) = (/) )
23 22 olcd 
 |-  ( ( ( x e. V /\ y e. V ) /\ -. x = y ) -> ( x = y \/ ( ( M ` x ) i^i ( M ` y ) ) = (/) ) )
24 23 expcom 
 |-  ( -. x = y -> ( ( x e. V /\ y e. V ) -> ( x = y \/ ( ( M ` x ) i^i ( M ` y ) ) = (/) ) ) )
25 4 24 pm2.61i 
 |-  ( ( x e. V /\ y e. V ) -> ( x = y \/ ( ( M ` x ) i^i ( M ` y ) ) = (/) ) )
26 25 rgen2 
 |-  A. x e. V A. y e. V ( x = y \/ ( ( M ` x ) i^i ( M ` y ) ) = (/) )
27 fveq2 
 |-  ( x = y -> ( M ` x ) = ( M ` y ) )
28 27 disjor 
 |-  ( Disj_ x e. V ( M ` x ) <-> A. x e. V A. y e. V ( x = y \/ ( ( M ` x ) i^i ( M ` y ) ) = (/) ) )
29 26 28 mpbir 
 |-  Disj_ x e. V ( M ` x )