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 ‘ 𝐺 ) 𝑃 )