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