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

Metamath Proof Explorer

Theorem 0clwlkv

Description: Any vertex (more precisely, a pair of an empty set (of edges) and a singleton function to this vertex) determines a closed walk of length 0. (Contributed by AV, 11-Feb-2022)

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

Proof

Step Hyp Ref Expression
1 0clwlk.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 fz0sn ⊢ ( 0 ... 0 ) = { 0 }
3 2 eqcomi ⊢ { 0 } = ( 0 ... 0 )
4 3 feq2i ⊢ ( 𝑃 : { 0 } ⟶ { 𝑋 } ↔ 𝑃 : ( 0 ... 0 ) ⟶ { 𝑋 } )
5 4 biimpi ⊢ ( 𝑃 : { 0 } ⟶ { 𝑋 } → 𝑃 : ( 0 ... 0 ) ⟶ { 𝑋 } )
6 5 3ad2ant3 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 = ∅ ∧ 𝑃 : { 0 } ⟶ { 𝑋 } ) → 𝑃 : ( 0 ... 0 ) ⟶ { 𝑋 } )
7 snssi ⊢ ( 𝑋 ∈ 𝑉 → { 𝑋 } ⊆ 𝑉 )
8 7 3ad2ant1 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 = ∅ ∧ 𝑃 : { 0 } ⟶ { 𝑋 } ) → { 𝑋 } ⊆ 𝑉 )
9 6 8 fssd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 = ∅ ∧ 𝑃 : { 0 } ⟶ { 𝑋 } ) → 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 )
10 breq1 ⊢ ( 𝐹 = ∅ → ( 𝐹 ( ClWalks ‘ 𝐺 ) 𝑃 ↔ ∅ ( ClWalks ‘ 𝐺 ) 𝑃 ) )
11 10 3ad2ant2 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 = ∅ ∧ 𝑃 : { 0 } ⟶ { 𝑋 } ) → ( 𝐹 ( ClWalks ‘ 𝐺 ) 𝑃 ↔ ∅ ( ClWalks ‘ 𝐺 ) 𝑃 ) )
12 1 1vgrex ⊢ ( 𝑋 ∈ 𝑉 → 𝐺 ∈ V )
13 1 0clwlk ⊢ ( 𝐺 ∈ V → ( ∅ ( ClWalks ‘ 𝐺 ) 𝑃 ↔ 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ) )
14 12 13 syl ⊢ ( 𝑋 ∈ 𝑉 → ( ∅ ( ClWalks ‘ 𝐺 ) 𝑃 ↔ 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ) )
15 14 3ad2ant1 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 = ∅ ∧ 𝑃 : { 0 } ⟶ { 𝑋 } ) → ( ∅ ( ClWalks ‘ 𝐺 ) 𝑃 ↔ 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ) )
16 11 15 bitrd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 = ∅ ∧ 𝑃 : { 0 } ⟶ { 𝑋 } ) → ( 𝐹 ( ClWalks ‘ 𝐺 ) 𝑃 ↔ 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ) )
17 9 16 mpbird ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 = ∅ ∧ 𝑃 : { 0 } ⟶ { 𝑋 } ) → 𝐹 ( ClWalks ‘ 𝐺 ) 𝑃 )