Theorem clwwlk0on0

Description: There is no word over the set of vertices representing a closed walk on vertex X of length 0 in a graph G . (Contributed by AV, 17-Feb-2022) (Revised by AV, 25-Feb-2022)

	Ref	Expression
Assertion	clwwlk0on0	⊢ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 0 ) = ∅

Proof

Step	Hyp	Ref	Expression
1		eqeq2	⊢ ( 𝑣 = 𝑋 → ( ( 𝑤 ‘ 0 ) = 𝑣 ↔ ( 𝑤 ‘ 0 ) = 𝑋 ) )
2	1	rabbidv	⊢ ( 𝑣 = 𝑋 → { 𝑤 ∈ ( 𝑛 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } = { 𝑤 ∈ ( 𝑛 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } )
3		oveq1	⊢ ( 𝑛 = 0 → ( 𝑛 ClWWalksN 𝐺 ) = ( 0 ClWWalksN 𝐺 ) )
4		clwwlkn0	⊢ ( 0 ClWWalksN 𝐺 ) = ∅
5	3 4	eqtrdi	⊢ ( 𝑛 = 0 → ( 𝑛 ClWWalksN 𝐺 ) = ∅ )
6	5	rabeqdv	⊢ ( 𝑛 = 0 → { 𝑤 ∈ ( 𝑛 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } = { 𝑤 ∈ ∅ ∣ ( 𝑤 ‘ 0 ) = 𝑋 } )
7		clwwlknonmpo	⊢ ( ClWWalksNOn ‘ 𝐺 ) = ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) , 𝑛 ∈ ℕ0 ↦ { 𝑤 ∈ ( 𝑛 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } )
8		0ex	⊢ ∅ ∈ V
9	8	rabex	⊢ { 𝑤 ∈ ∅ ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ∈ V
10	2 6 7 9	ovmpo	⊢ ( ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 0 ∈ ℕ0 ) → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 0 ) = { 𝑤 ∈ ∅ ∣ ( 𝑤 ‘ 0 ) = 𝑋 } )
11		rab0	⊢ { 𝑤 ∈ ∅ ∣ ( 𝑤 ‘ 0 ) = 𝑋 } = ∅
12	10 11	eqtrdi	⊢ ( ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 0 ∈ ℕ0 ) → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 0 ) = ∅ )
13	7	mpondm0	⊢ ( ¬ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 0 ∈ ℕ0 ) → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 0 ) = ∅ )
14	12 13	pm2.61i	⊢ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 0 ) = ∅