Metamath Proof Explorer

Theorem wspniunwspnon

Description: The set of nonempty simple paths of fixed length is the double union of the simple paths of the fixed length between different vertices. (Contributed by Alexander van der Vekens, 3-Mar-2018) (Revised by AV, 16-May-2021) (Proof shortened by AV, 15-Mar-2022)

Ref Expression
Hypothesis wspniunwspnon.v 
|- V = ( Vtx ` G )
Assertion wspniunwspnon 
|- ( ( N e. NN /\ G e. U ) -> ( N WSPathsN G ) = U_ x e. V U_ y e. ( V \ { x } ) ( x ( N WSPathsNOn G ) y ) )

Proof

Step Hyp Ref Expression
1 wspniunwspnon.v 
 |-  V = ( Vtx ` G )
2 wspthsnonn0vne 
 |-  ( ( N e. NN /\ ( x ( N WSPathsNOn G ) y ) =/= (/) ) -> x =/= y )
3 2 ex 
 |-  ( N e. NN -> ( ( x ( N WSPathsNOn G ) y ) =/= (/) -> x =/= y ) )
4 3 adantr 
 |-  ( ( N e. NN /\ G e. U ) -> ( ( x ( N WSPathsNOn G ) y ) =/= (/) -> x =/= y ) )
5 ne0i 
 |-  ( w e. ( x ( N WSPathsNOn G ) y ) -> ( x ( N WSPathsNOn G ) y ) =/= (/) )
6 4 5 impel 
 |-  ( ( ( N e. NN /\ G e. U ) /\ w e. ( x ( N WSPathsNOn G ) y ) ) -> x =/= y )
7 6 necomd 
 |-  ( ( ( N e. NN /\ G e. U ) /\ w e. ( x ( N WSPathsNOn G ) y ) ) -> y =/= x )
8 7 ex 
 |-  ( ( N e. NN /\ G e. U ) -> ( w e. ( x ( N WSPathsNOn G ) y ) -> y =/= x ) )
9 8 pm4.71rd 
 |-  ( ( N e. NN /\ G e. U ) -> ( w e. ( x ( N WSPathsNOn G ) y ) <-> ( y =/= x /\ w e. ( x ( N WSPathsNOn G ) y ) ) ) )
10 9 rexbidv 
 |-  ( ( N e. NN /\ G e. U ) -> ( E. y e. V w e. ( x ( N WSPathsNOn G ) y ) <-> E. y e. V ( y =/= x /\ w e. ( x ( N WSPathsNOn G ) y ) ) ) )
11 rexdifsn 
 |-  ( E. y e. ( V \ { x } ) w e. ( x ( N WSPathsNOn G ) y ) <-> E. y e. V ( y =/= x /\ w e. ( x ( N WSPathsNOn G ) y ) ) )
12 10 11 bitr4di 
 |-  ( ( N e. NN /\ G e. U ) -> ( E. y e. V w e. ( x ( N WSPathsNOn G ) y ) <-> E. y e. ( V \ { x } ) w e. ( x ( N WSPathsNOn G ) y ) ) )
13 12 rexbidv 
 |-  ( ( N e. NN /\ G e. U ) -> ( E. x e. V E. y e. V w e. ( x ( N WSPathsNOn G ) y ) <-> E. x e. V E. y e. ( V \ { x } ) w e. ( x ( N WSPathsNOn G ) y ) ) )
14 1 wspthsnwspthsnon 
 |-  ( w e. ( N WSPathsN G ) <-> E. x e. V E. y e. V w e. ( x ( N WSPathsNOn G ) y ) )
15 vex 
 |-  w e. _V
16 eleq1w 
 |-  ( p = w -> ( p e. ( x ( N WSPathsNOn G ) y ) <-> w e. ( x ( N WSPathsNOn G ) y ) ) )
17 16 rexbidv 
 |-  ( p = w -> ( E. y e. ( V \ { x } ) p e. ( x ( N WSPathsNOn G ) y ) <-> E. y e. ( V \ { x } ) w e. ( x ( N WSPathsNOn G ) y ) ) )
18 17 rexbidv 
 |-  ( p = w -> ( E. x e. V E. y e. ( V \ { x } ) p e. ( x ( N WSPathsNOn G ) y ) <-> E. x e. V E. y e. ( V \ { x } ) w e. ( x ( N WSPathsNOn G ) y ) ) )
19 15 18 elab 
 |-  ( w e. { p | E. x e. V E. y e. ( V \ { x } ) p e. ( x ( N WSPathsNOn G ) y ) } <-> E. x e. V E. y e. ( V \ { x } ) w e. ( x ( N WSPathsNOn G ) y ) )
20 13 14 19 3bitr4g 
 |-  ( ( N e. NN /\ G e. U ) -> ( w e. ( N WSPathsN G ) <-> w e. { p | E. x e. V E. y e. ( V \ { x } ) p e. ( x ( N WSPathsNOn G ) y ) } ) )
21 20 eqrdv 
 |-  ( ( N e. NN /\ G e. U ) -> ( N WSPathsN G ) = { p | E. x e. V E. y e. ( V \ { x } ) p e. ( x ( N WSPathsNOn G ) y ) } )
22 dfiunv2 
 |-  U_ x e. V U_ y e. ( V \ { x } ) ( x ( N WSPathsNOn G ) y ) = { p | E. x e. V E. y e. ( V \ { x } ) p e. ( x ( N WSPathsNOn G ) y ) }
23 21 22 eqtr4di 
 |-  ( ( N e. NN /\ G e. U ) -> ( N WSPathsN G ) = U_ x e. V U_ y e. ( V \ { x } ) ( x ( N WSPathsNOn G ) y ) )