This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ⟶ 𝑉 ) )