Theorem 0clwlk

Description: A pair of an empty set (of edges) and a second set (of vertices) is a closed walk if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Mar-2018) (Revised by AV, 17-Feb-2021) (Revised by AV, 30-Oct-2021)

	Ref	Expression
Hypothesis	0clwlk.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	0clwlk	⊢ ( 𝐺 ∈ 𝑋 → ( ∅ ( ClWalks ‘ 𝐺 ) 𝑃 ↔ 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		0clwlk.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2	1	0wlk	⊢ ( 𝐺 ∈ 𝑋 → ( ∅ ( Walks ‘ 𝐺 ) 𝑃 ↔ 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ) )
3	2	anbi2d	⊢ ( 𝐺 ∈ 𝑋 → ( ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ ∅ ) ) ∧ ∅ ( Walks ‘ 𝐺 ) 𝑃 ) ↔ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ ∅ ) ) ∧ 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ) ) )
4		isclwlk	⊢ ( ∅ ( ClWalks ‘ 𝐺 ) 𝑃 ↔ ( ∅ ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ ∅ ) ) ) )
5	4	biancomi	⊢ ( ∅ ( ClWalks ‘ 𝐺 ) 𝑃 ↔ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ ∅ ) ) ∧ ∅ ( Walks ‘ 𝐺 ) 𝑃 ) )
6		hash0	⊢ ( ♯ ‘ ∅ ) = 0
7	6	eqcomi	⊢ 0 = ( ♯ ‘ ∅ )
8	7	fveq2i	⊢ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ ∅ ) )
9	8	biantrur	⊢ ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ↔ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ ∅ ) ) ∧ 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ) )
10	3 5 9	3bitr4g	⊢ ( 𝐺 ∈ 𝑋 → ( ∅ ( ClWalks ‘ 𝐺 ) 𝑃 ↔ 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ) )