Theorem clwwlknon1sn

Description: The set of (closed) walks on vertex X of length 1 as words over the set of vertices is a singleton containing the singleton word consisting of X iff there is a loop at X . (Contributed by AV, 11-Feb-2022) (Revised by AV, 25-Feb-2022)

	Ref	Expression
Hypotheses	clwwlknon1.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	clwwlknon1.c	⊢ 𝐶 = ( ClWWalksNOn ‘ 𝐺 )
	clwwlknon1.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	clwwlknon1sn	⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝑋 𝐶 1 ) = { ⟨“ 𝑋 ”⟩ } ↔ { 𝑋 } ∈ 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		clwwlknon1.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		clwwlknon1.c	⊢ 𝐶 = ( ClWWalksNOn ‘ 𝐺 )
3		clwwlknon1.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
4		df-nel	⊢ ( { 𝑋 } ∉ 𝐸 ↔ ¬ { 𝑋 } ∈ 𝐸 )
5	1 2 3	clwwlknon1nloop	⊢ ( { 𝑋 } ∉ 𝐸 → ( 𝑋 𝐶 1 ) = ∅ )
6	5	adantl	⊢ ( ( 𝑋 ∈ 𝑉 ∧ { 𝑋 } ∉ 𝐸 ) → ( 𝑋 𝐶 1 ) = ∅ )
7		s1cli	⊢ ⟨“ 𝑋 ”⟩ ∈ Word V
8	7	elexi	⊢ ⟨“ 𝑋 ”⟩ ∈ V
9	8	snnz	⊢ { ⟨“ 𝑋 ”⟩ } ≠ ∅
10	9	nesymi	⊢ ¬ ∅ = { ⟨“ 𝑋 ”⟩ }
11		eqeq1	⊢ ( ( 𝑋 𝐶 1 ) = ∅ → ( ( 𝑋 𝐶 1 ) = { ⟨“ 𝑋 ”⟩ } ↔ ∅ = { ⟨“ 𝑋 ”⟩ } ) )
12	10 11	mtbiri	⊢ ( ( 𝑋 𝐶 1 ) = ∅ → ¬ ( 𝑋 𝐶 1 ) = { ⟨“ 𝑋 ”⟩ } )
13	6 12	syl	⊢ ( ( 𝑋 ∈ 𝑉 ∧ { 𝑋 } ∉ 𝐸 ) → ¬ ( 𝑋 𝐶 1 ) = { ⟨“ 𝑋 ”⟩ } )
14	13	ex	⊢ ( 𝑋 ∈ 𝑉 → ( { 𝑋 } ∉ 𝐸 → ¬ ( 𝑋 𝐶 1 ) = { ⟨“ 𝑋 ”⟩ } ) )
15	4 14	biimtrrid	⊢ ( 𝑋 ∈ 𝑉 → ( ¬ { 𝑋 } ∈ 𝐸 → ¬ ( 𝑋 𝐶 1 ) = { ⟨“ 𝑋 ”⟩ } ) )
16	15	con4d	⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝑋 𝐶 1 ) = { ⟨“ 𝑋 ”⟩ } → { 𝑋 } ∈ 𝐸 ) )
17	1 2 3	clwwlknon1loop	⊢ ( ( 𝑋 ∈ 𝑉 ∧ { 𝑋 } ∈ 𝐸 ) → ( 𝑋 𝐶 1 ) = { ⟨“ 𝑋 ”⟩ } )
18	17	ex	⊢ ( 𝑋 ∈ 𝑉 → ( { 𝑋 } ∈ 𝐸 → ( 𝑋 𝐶 1 ) = { ⟨“ 𝑋 ”⟩ } ) )
19	16 18	impbid	⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝑋 𝐶 1 ) = { ⟨“ 𝑋 ”⟩ } ↔ { 𝑋 } ∈ 𝐸 ) )