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 ‘ 𝐺 ) = ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) , 𝑛 ∈ ℕ0 ↦ { 𝑤 ∈ ( 𝑛 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) )
2		eqidd	⊢ ( 𝑔 = 𝐺 → ℕ0 = ℕ0 )
3		oveq2	⊢ ( 𝑔 = 𝐺 → ( 𝑛 ClWWalksN 𝑔 ) = ( 𝑛 ClWWalksN 𝐺 ) )
4	3	rabeqdv	⊢ ( 𝑔 = 𝐺 → { 𝑤 ∈ ( 𝑛 ClWWalksN 𝑔 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } = { 𝑤 ∈ ( 𝑛 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } )
5	1 2 4	mpoeq123dv	⊢ ( 𝑔 = 𝐺 → ( 𝑣 ∈ ( Vtx ‘ 𝑔 ) , 𝑛 ∈ ℕ0 ↦ { 𝑤 ∈ ( 𝑛 ClWWalksN 𝑔 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } ) = ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) , 𝑛 ∈ ℕ0 ↦ { 𝑤 ∈ ( 𝑛 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } ) )
6		df-clwwlknon	⊢ ClWWalksNOn = ( 𝑔 ∈ V ↦ ( 𝑣 ∈ ( Vtx ‘ 𝑔 ) , 𝑛 ∈ ℕ0 ↦ { 𝑤 ∈ ( 𝑛 ClWWalksN 𝑔 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } ) )
7		fvex	⊢ ( Vtx ‘ 𝐺 ) ∈ V
8		nn0ex	⊢ ℕ0 ∈ V
9	7 8	mpoex	⊢ ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) , 𝑛 ∈ ℕ0 ↦ { 𝑤 ∈ ( 𝑛 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } ) ∈ V
10	5 6 9	fvmpt	⊢ ( 𝐺 ∈ V → ( ClWWalksNOn ‘ 𝐺 ) = ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) , 𝑛 ∈ ℕ0 ↦ { 𝑤 ∈ ( 𝑛 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } ) )
11		fvprc	⊢ ( ¬ 𝐺 ∈ V → ( ClWWalksNOn ‘ 𝐺 ) = ∅ )
12		fvprc	⊢ ( ¬ 𝐺 ∈ V → ( Vtx ‘ 𝐺 ) = ∅ )
13	12	orcd	⊢ ( ¬ 𝐺 ∈ V → ( ( Vtx ‘ 𝐺 ) = ∅ ∨ ℕ0 = ∅ ) )
14		0mpo0	⊢ ( ( ( Vtx ‘ 𝐺 ) = ∅ ∨ ℕ0 = ∅ ) → ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) , 𝑛 ∈ ℕ0 ↦ { 𝑤 ∈ ( 𝑛 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } ) = ∅ )
15	13 14	syl	⊢ ( ¬ 𝐺 ∈ V → ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) , 𝑛 ∈ ℕ0 ↦ { 𝑤 ∈ ( 𝑛 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } ) = ∅ )
16	11 15	eqtr4d	⊢ ( ¬ 𝐺 ∈ V → ( ClWWalksNOn ‘ 𝐺 ) = ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) , 𝑛 ∈ ℕ0 ↦ { 𝑤 ∈ ( 𝑛 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } ) )
17	10 16	pm2.61i	⊢ ( ClWWalksNOn ‘ 𝐺 ) = ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) , 𝑛 ∈ ℕ0 ↦ { 𝑤 ∈ ( 𝑛 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } )