Metamath Proof Explorer

Theorem clwwlknondisj

Description: The sets of closed walks on different vertices are disjunct. (Contributed by Alexander van der Vekens, 7-Oct-2018) (Revised by AV, 28-May-2021) (Revised by AV, 3-Mar-2022) (Proof shortened by AV, 28-Mar-2022)

Ref Expression
Assertion clwwlknondisj 
|- Disj_ x e. V ( x ( ClWWalksNOn ` G ) N )

Proof

Step Hyp Ref Expression
1 clwwlknon 
 |-  ( x ( ClWWalksNOn ` G ) N ) = { w e. ( N ClWWalksN G ) | ( w ` 0 ) = x }
2 clwwlknon 
 |-  ( y ( ClWWalksNOn ` G ) N ) = { w e. ( N ClWWalksN G ) | ( w ` 0 ) = y }
3 1 2 ineq12i 
 |-  ( ( x ( ClWWalksNOn ` G ) N ) i^i ( y ( ClWWalksNOn ` G ) N ) ) = ( { w e. ( N ClWWalksN G ) | ( w ` 0 ) = x } i^i { w e. ( N ClWWalksN G ) | ( w ` 0 ) = y } )
4 inrab 
 |-  ( { w e. ( N ClWWalksN G ) | ( w ` 0 ) = x } i^i { w e. ( N ClWWalksN G ) | ( w ` 0 ) = y } ) = { w e. ( N ClWWalksN G ) | ( ( w ` 0 ) = x /\ ( w ` 0 ) = y ) }
5 eqtr2 
 |-  ( ( ( w ` 0 ) = x /\ ( w ` 0 ) = y ) -> x = y )
6 5 con3i 
 |-  ( -. x = y -> -. ( ( w ` 0 ) = x /\ ( w ` 0 ) = y ) )
7 6 ralrimivw 
 |-  ( -. x = y -> A. w e. ( N ClWWalksN G ) -. ( ( w ` 0 ) = x /\ ( w ` 0 ) = y ) )
8 rabeq0 
 |-  ( { w e. ( N ClWWalksN G ) | ( ( w ` 0 ) = x /\ ( w ` 0 ) = y ) } = (/) <-> A. w e. ( N ClWWalksN G ) -. ( ( w ` 0 ) = x /\ ( w ` 0 ) = y ) )
9 7 8 sylibr 
 |-  ( -. x = y -> { w e. ( N ClWWalksN G ) | ( ( w ` 0 ) = x /\ ( w ` 0 ) = y ) } = (/) )
10 4 9 eqtrid 
 |-  ( -. x = y -> ( { w e. ( N ClWWalksN G ) | ( w ` 0 ) = x } i^i { w e. ( N ClWWalksN G ) | ( w ` 0 ) = y } ) = (/) )
11 3 10 eqtrid 
 |-  ( -. x = y -> ( ( x ( ClWWalksNOn ` G ) N ) i^i ( y ( ClWWalksNOn ` G ) N ) ) = (/) )
12 11 orri 
 |-  ( x = y \/ ( ( x ( ClWWalksNOn ` G ) N ) i^i ( y ( ClWWalksNOn ` G ) N ) ) = (/) )
13 12 rgen2w 
 |-  A. x e. V A. y e. V ( x = y \/ ( ( x ( ClWWalksNOn ` G ) N ) i^i ( y ( ClWWalksNOn ` G ) N ) ) = (/) )
14 oveq1 
 |-  ( x = y -> ( x ( ClWWalksNOn ` G ) N ) = ( y ( ClWWalksNOn ` G ) N ) )
15 14 disjor 
 |-  ( Disj_ x e. V ( x ( ClWWalksNOn ` G ) N ) <-> A. x e. V A. y e. V ( x = y \/ ( ( x ( ClWWalksNOn ` G ) N ) i^i ( y ( ClWWalksNOn ` G ) N ) ) = (/) ) )
16 13 15 mpbir 
 |-  Disj_ x e. V ( x ( ClWWalksNOn ` G ) N )