Metamath Proof Explorer

Theorem numclwwlk3lem2lem

Description: Lemma for numclwwlk3lem2 : The set of closed vertices of a fixed length N on a fixed vertex V is the union of the set of closed walks of length N at V with the last but one vertex being V and the set of closed walks of length N at V with the last but one vertex not being V . (Contributed by AV, 1-May-2022)

Ref Expression
Hypotheses numclwwlk3lem2.c 
|- C = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } )
numclwwlk3lem2.h 
|- H = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) =/= v } )
Assertion numclwwlk3lem2lem 
|- ( ( X e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( X ( ClWWalksNOn ` G ) N ) = ( ( X H N ) u. ( X C N ) ) )

Proof

Step Hyp Ref Expression
1 numclwwlk3lem2.c 
 |-  C = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } )
2 numclwwlk3lem2.h 
 |-  H = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) =/= v } )
3 2 numclwwlkovh0 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( X H N ) = { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) =/= X } )
4 1 2clwwlk 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( X C N ) = { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } )
5 3 4 uneq12d 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( ( X H N ) u. ( X C N ) ) = ( { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) =/= X } u. { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } ) )
6 unrab 
 |-  ( { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) =/= X } u. { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } ) = { w e. ( X ( ClWWalksNOn ` G ) N ) | ( ( w ` ( N - 2 ) ) =/= X \/ ( w ` ( N - 2 ) ) = X ) }
7 exmidne 
 |-  ( ( w ` ( N - 2 ) ) = X \/ ( w ` ( N - 2 ) ) =/= X )
8 orcom 
 |-  ( ( ( w ` ( N - 2 ) ) =/= X \/ ( w ` ( N - 2 ) ) = X ) <-> ( ( w ` ( N - 2 ) ) = X \/ ( w ` ( N - 2 ) ) =/= X ) )
9 7 8 mpbir 
 |-  ( ( w ` ( N - 2 ) ) =/= X \/ ( w ` ( N - 2 ) ) = X )
10 9 a1i 
 |-  ( w e. ( X ( ClWWalksNOn ` G ) N ) -> ( ( w ` ( N - 2 ) ) =/= X \/ ( w ` ( N - 2 ) ) = X ) )
11 10 rabeqc 
 |-  { w e. ( X ( ClWWalksNOn ` G ) N ) | ( ( w ` ( N - 2 ) ) =/= X \/ ( w ` ( N - 2 ) ) = X ) } = ( X ( ClWWalksNOn ` G ) N )
12 6 11 eqtri 
 |-  ( { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) =/= X } u. { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } ) = ( X ( ClWWalksNOn ` G ) N )
13 5 12 eqtr2di 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( X ( ClWWalksNOn ` G ) N ) = ( ( X H N ) u. ( X C N ) ) )