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

Metamath Proof Explorer

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 bitr2id ⊢ ( 𝑉 ∈ ( Vtx ‘ 𝐺 ) → ( { 𝑉 } ∈ ( Edg ‘ 𝐺 ) ↔ ⟨“ 𝑉 ”⟩ ∈ ( 1 ClWWalksN 𝐺 ) ) )