Metamath Proof Explorer

Theorem clwwlknonmpo

Description: ( ClWWalksNOnG ) is an operator mapping a vertex v and a nonnegative integer n to the set of closed walks on v of length n as words over the set of vertices in a graph G . (Contributed by AV, 25-Feb-2022) (Proof shortened by AV, 2-Mar-2024)

Ref Expression
Assertion clwwlknonmpo 
|- ( ClWWalksNOn ` G ) = ( v e. ( Vtx ` G ) , n e. NN0 |-> { w e. ( n ClWWalksN G ) | ( w ` 0 ) = v } )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( g = G -> ( Vtx ` g ) = ( Vtx ` G ) )
2 eqidd 
 |-  ( g = G -> NN0 = NN0 )
3 oveq2 
 |-  ( g = G -> ( n ClWWalksN g ) = ( n ClWWalksN G ) )
4 3 rabeqdv 
 |-  ( g = G -> { w e. ( n ClWWalksN g ) | ( w ` 0 ) = v } = { w e. ( n ClWWalksN G ) | ( w ` 0 ) = v } )
5 1 2 4 mpoeq123dv 
 |-  ( g = G -> ( v e. ( Vtx ` g ) , n e. NN0 |-> { w e. ( n ClWWalksN g ) | ( w ` 0 ) = v } ) = ( v e. ( Vtx ` G ) , n e. NN0 |-> { w e. ( n ClWWalksN G ) | ( w ` 0 ) = v } ) )
6 df-clwwlknon 
 |-  ClWWalksNOn = ( g e. _V |-> ( v e. ( Vtx ` g ) , n e. NN0 |-> { w e. ( n ClWWalksN g ) | ( w ` 0 ) = v } ) )
7 fvex 
 |-  ( Vtx ` G ) e. _V
8 nn0ex 
 |-  NN0 e. _V
9 7 8 mpoex 
 |-  ( v e. ( Vtx ` G ) , n e. NN0 |-> { w e. ( n ClWWalksN G ) | ( w ` 0 ) = v } ) e. _V
10 5 6 9 fvmpt 
 |-  ( G e. _V -> ( ClWWalksNOn ` G ) = ( v e. ( Vtx ` G ) , n e. NN0 |-> { w e. ( n ClWWalksN G ) | ( w ` 0 ) = v } ) )
11 fvprc 
 |-  ( -. G e. _V -> ( ClWWalksNOn ` G ) = (/) )
12 fvprc 
 |-  ( -. G e. _V -> ( Vtx ` G ) = (/) )
13 12 orcd 
 |-  ( -. G e. _V -> ( ( Vtx ` G ) = (/) \/ NN0 = (/) ) )
14 0mpo0 
 |-  ( ( ( Vtx ` G ) = (/) \/ NN0 = (/) ) -> ( v e. ( Vtx ` G ) , n e. NN0 |-> { w e. ( n ClWWalksN G ) | ( w ` 0 ) = v } ) = (/) )
15 13 14 syl 
 |-  ( -. G e. _V -> ( v e. ( Vtx ` G ) , n e. NN0 |-> { w e. ( n ClWWalksN G ) | ( w ` 0 ) = v } ) = (/) )
16 11 15 eqtr4d 
 |-  ( -. G e. _V -> ( ClWWalksNOn ` G ) = ( v e. ( Vtx ` G ) , n e. NN0 |-> { w e. ( n ClWWalksN G ) | ( w ` 0 ) = v } ) )
17 10 16 pm2.61i 
 |-  ( ClWWalksNOn ` G ) = ( v e. ( Vtx ` G ) , n e. NN0 |-> { w e. ( n ClWWalksN G ) | ( w ` 0 ) = v } )