Theorem loopclwwlkn1b

Description: The singleton word consisting of a vertex V represents a closed walk of length 1 iff there is a loop at vertex V . (Contributed by AV, 11-Feb-2022)

	Ref	Expression
Assertion	loopclwwlkn1b	⊢ ( 𝑉 ∈ ( Vtx ‘ 𝐺 ) → ( { 𝑉 } ∈ ( Edg ‘ 𝐺 ) ↔ ⟨“ 𝑉 ”⟩ ∈ ( 1 ClWWalksN 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		clwwlkn1	⊢ ( ⟨“ 𝑉 ”⟩ ∈ ( 1 ClWWalksN 𝐺 ) ↔ ( ( ♯ ‘ ⟨“ 𝑉 ”⟩ ) = 1 ∧ ⟨“ 𝑉 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( ⟨“ 𝑉 ”⟩ ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
2		s1fv	⊢ ( 𝑉 ∈ ( Vtx ‘ 𝐺 ) → ( ⟨“ 𝑉 ”⟩ ‘ 0 ) = 𝑉 )
3	2	sneqd	⊢ ( 𝑉 ∈ ( Vtx ‘ 𝐺 ) → { ( ⟨“ 𝑉 ”⟩ ‘ 0 ) } = { 𝑉 } )
4	3	eleq1d	⊢ ( 𝑉 ∈ ( Vtx ‘ 𝐺 ) → ( { ( ⟨“ 𝑉 ”⟩ ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ↔ { 𝑉 } ∈ ( Edg ‘ 𝐺 ) ) )
5	4	biimpcd	⊢ ( { ( ⟨“ 𝑉 ”⟩ ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) → ( 𝑉 ∈ ( Vtx ‘ 𝐺 ) → { 𝑉 } ∈ ( Edg ‘ 𝐺 ) ) )
6	5	3ad2ant3	⊢ ( ( ( ♯ ‘ ⟨“ 𝑉 ”⟩ ) = 1 ∧ ⟨“ 𝑉 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( ⟨“ 𝑉 ”⟩ ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( 𝑉 ∈ ( Vtx ‘ 𝐺 ) → { 𝑉 } ∈ ( Edg ‘ 𝐺 ) ) )
7	6	com12	⊢ ( 𝑉 ∈ ( Vtx ‘ 𝐺 ) → ( ( ( ♯ ‘ ⟨“ 𝑉 ”⟩ ) = 1 ∧ ⟨“ 𝑉 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( ⟨“ 𝑉 ”⟩ ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → { 𝑉 } ∈ ( Edg ‘ 𝐺 ) ) )
8		s1len	⊢ ( ♯ ‘ ⟨“ 𝑉 ”⟩ ) = 1
9	8	a1i	⊢ ( ( 𝑉 ∈ ( Vtx ‘ 𝐺 ) ∧ { 𝑉 } ∈ ( Edg ‘ 𝐺 ) ) → ( ♯ ‘ ⟨“ 𝑉 ”⟩ ) = 1 )
10		s1cl	⊢ ( 𝑉 ∈ ( Vtx ‘ 𝐺 ) → ⟨“ 𝑉 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) )
11	10	adantr	⊢ ( ( 𝑉 ∈ ( Vtx ‘ 𝐺 ) ∧ { 𝑉 } ∈ ( Edg ‘ 𝐺 ) ) → ⟨“ 𝑉 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) )
12	2	eqcomd	⊢ ( 𝑉 ∈ ( Vtx ‘ 𝐺 ) → 𝑉 = ( ⟨“ 𝑉 ”⟩ ‘ 0 ) )
13	12	sneqd	⊢ ( 𝑉 ∈ ( Vtx ‘ 𝐺 ) → { 𝑉 } = { ( ⟨“ 𝑉 ”⟩ ‘ 0 ) } )
14	13	eleq1d	⊢ ( 𝑉 ∈ ( Vtx ‘ 𝐺 ) → ( { 𝑉 } ∈ ( Edg ‘ 𝐺 ) ↔ { ( ⟨“ 𝑉 ”⟩ ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
15	14	biimpa	⊢ ( ( 𝑉 ∈ ( Vtx ‘ 𝐺 ) ∧ { 𝑉 } ∈ ( Edg ‘ 𝐺 ) ) → { ( ⟨“ 𝑉 ”⟩ ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) )
16	9 11 15	3jca	⊢ ( ( 𝑉 ∈ ( Vtx ‘ 𝐺 ) ∧ { 𝑉 } ∈ ( Edg ‘ 𝐺 ) ) → ( ( ♯ ‘ ⟨“ 𝑉 ”⟩ ) = 1 ∧ ⟨“ 𝑉 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( ⟨“ 𝑉 ”⟩ ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
17	16	ex	⊢ ( 𝑉 ∈ ( Vtx ‘ 𝐺 ) → ( { 𝑉 } ∈ ( Edg ‘ 𝐺 ) → ( ( ♯ ‘ ⟨“ 𝑉 ”⟩ ) = 1 ∧ ⟨“ 𝑉 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( ⟨“ 𝑉 ”⟩ ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
18	7 17	impbid	⊢ ( 𝑉 ∈ ( Vtx ‘ 𝐺 ) → ( ( ( ♯ ‘ ⟨“ 𝑉 ”⟩ ) = 1 ∧ ⟨“ 𝑉 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( ⟨“ 𝑉 ”⟩ ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ { 𝑉 } ∈ ( Edg ‘ 𝐺 ) ) )
19	1 18	syl5rbb	⊢ ( 𝑉 ∈ ( Vtx ‘ 𝐺 ) → ( { 𝑉 } ∈ ( Edg ‘ 𝐺 ) ↔ ⟨“ 𝑉 ”⟩ ∈ ( 1 ClWWalksN 𝐺 ) ) )