Metamath Proof Explorer

Theorem clwwlkn1loopb

Description: A word represents a closed walk of length 1 iff this word is a singleton word consisting of a vertex with an attached loop. (Contributed by AV, 11-Feb-2022)

Ref Expression
Assertion clwwlkn1loopb ( 𝑊 ∈ ( 1 ClWWalksN 𝐺 ) ↔ ∃ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝑊 = ⟨“ 𝑣 ”⟩ ∧ { 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 clwwlkn1 ⊢ ( 𝑊 ∈ ( 1 ClWWalksN 𝐺 ) ↔ ( ( ♯ ‘ 𝑊 ) = 1 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
2 wrdl1exs1 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ∃ 𝑣 ∈ ( Vtx ‘ 𝐺 ) 𝑊 = ⟨“ 𝑣 ”⟩ )
3 fveq1 ⊢ ( 𝑊 = ⟨“ 𝑣 ”⟩ → ( 𝑊 ‘ 0 ) = ( ⟨“ 𝑣 ”⟩ ‘ 0 ) )
4 s1fv ⊢ ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) → ( ⟨“ 𝑣 ”⟩ ‘ 0 ) = 𝑣 )
5 3 4 sylan9eq ⊢ ( ( 𝑊 = ⟨“ 𝑣 ”⟩ ∧ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝑊 ‘ 0 ) = 𝑣 )
6 5 sneqd ⊢ ( ( 𝑊 = ⟨“ 𝑣 ”⟩ ∧ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ) → { ( 𝑊 ‘ 0 ) } = { 𝑣 } )
7 6 eleq1d ⊢ ( ( 𝑊 = ⟨“ 𝑣 ”⟩ ∧ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ) → ( { ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ↔ { 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) )
8 7 biimpd ⊢ ( ( 𝑊 = ⟨“ 𝑣 ”⟩ ∧ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ) → ( { ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) → { 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) )
9 8 ex ⊢ ( 𝑊 = ⟨“ 𝑣 ”⟩ → ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) → ( { ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) → { 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) ) )
10 9 com13 ⊢ ( { ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) → ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) → ( 𝑊 = ⟨“ 𝑣 ”⟩ → { 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) ) )
11 10 imp ⊢ ( ( { ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ∧ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝑊 = ⟨“ 𝑣 ”⟩ → { 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) )
12 11 ancld ⊢ ( ( { ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ∧ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝑊 = ⟨“ 𝑣 ”⟩ → ( 𝑊 = ⟨“ 𝑣 ”⟩ ∧ { 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) ) )
13 12 reximdva ⊢ ( { ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) → ( ∃ 𝑣 ∈ ( Vtx ‘ 𝐺 ) 𝑊 = ⟨“ 𝑣 ”⟩ → ∃ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝑊 = ⟨“ 𝑣 ”⟩ ∧ { 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) ) )
14 2 13 syl5com ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( { ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) → ∃ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝑊 = ⟨“ 𝑣 ”⟩ ∧ { 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) ) )
15 14 expcom ⊢ ( ( ♯ ‘ 𝑊 ) = 1 → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( { ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) → ∃ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝑊 = ⟨“ 𝑣 ”⟩ ∧ { 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
16 15 3imp ⊢ ( ( ( ♯ ‘ 𝑊 ) = 1 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ∃ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝑊 = ⟨“ 𝑣 ”⟩ ∧ { 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) )
17 s1len ⊢ ( ♯ ‘ ⟨“ 𝑣 ”⟩ ) = 1
18 17 a1i ⊢ ( ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) ∧ { 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) → ( ♯ ‘ ⟨“ 𝑣 ”⟩ ) = 1 )
19 s1cl ⊢ ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) → ⟨“ 𝑣 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) )
20 19 adantr ⊢ ( ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) ∧ { 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) → ⟨“ 𝑣 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) )
21 4 eqcomd ⊢ ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) → 𝑣 = ( ⟨“ 𝑣 ”⟩ ‘ 0 ) )
22 21 sneqd ⊢ ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) → { 𝑣 } = { ( ⟨“ 𝑣 ”⟩ ‘ 0 ) } )
23 22 eleq1d ⊢ ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) → ( { 𝑣 } ∈ ( Edg ‘ 𝐺 ) ↔ { ( ⟨“ 𝑣 ”⟩ ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
24 23 biimpd ⊢ ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) → ( { 𝑣 } ∈ ( Edg ‘ 𝐺 ) → { ( ⟨“ 𝑣 ”⟩ ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
25 24 imp ⊢ ( ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) ∧ { 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) → { ( ⟨“ 𝑣 ”⟩ ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) )
26 18 20 25 3jca ⊢ ( ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) ∧ { 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) → ( ( ♯ ‘ ⟨“ 𝑣 ”⟩ ) = 1 ∧ ⟨“ 𝑣 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( ⟨“ 𝑣 ”⟩ ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
27 26 adantrl ⊢ ( ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑊 = ⟨“ 𝑣 ”⟩ ∧ { 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) ) → ( ( ♯ ‘ ⟨“ 𝑣 ”⟩ ) = 1 ∧ ⟨“ 𝑣 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( ⟨“ 𝑣 ”⟩ ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
28 fveqeq2 ⊢ ( 𝑊 = ⟨“ 𝑣 ”⟩ → ( ( ♯ ‘ 𝑊 ) = 1 ↔ ( ♯ ‘ ⟨“ 𝑣 ”⟩ ) = 1 ) )
29 eleq1 ⊢ ( 𝑊 = ⟨“ 𝑣 ”⟩ → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ↔ ⟨“ 𝑣 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) ) )
30 3 sneqd ⊢ ( 𝑊 = ⟨“ 𝑣 ”⟩ → { ( 𝑊 ‘ 0 ) } = { ( ⟨“ 𝑣 ”⟩ ‘ 0 ) } )
31 30 eleq1d ⊢ ( 𝑊 = ⟨“ 𝑣 ”⟩ → ( { ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( ⟨“ 𝑣 ”⟩ ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
32 28 29 31 3anbi123d ⊢ ( 𝑊 = ⟨“ 𝑣 ”⟩ → ( ( ( ♯ ‘ 𝑊 ) = 1 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( ( ♯ ‘ ⟨“ 𝑣 ”⟩ ) = 1 ∧ ⟨“ 𝑣 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( ⟨“ 𝑣 ”⟩ ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
33 32 ad2antrl ⊢ ( ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑊 = ⟨“ 𝑣 ”⟩ ∧ { 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) ) → ( ( ( ♯ ‘ 𝑊 ) = 1 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( ( ♯ ‘ ⟨“ 𝑣 ”⟩ ) = 1 ∧ ⟨“ 𝑣 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( ⟨“ 𝑣 ”⟩ ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
34 27 33 mpbird ⊢ ( ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑊 = ⟨“ 𝑣 ”⟩ ∧ { 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) ) → ( ( ♯ ‘ 𝑊 ) = 1 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
35 34 rexlimiva ⊢ ( ∃ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝑊 = ⟨“ 𝑣 ”⟩ ∧ { 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) → ( ( ♯ ‘ 𝑊 ) = 1 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
36 16 35 impbii ⊢ ( ( ( ♯ ‘ 𝑊 ) = 1 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ∃ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝑊 = ⟨“ 𝑣 ”⟩ ∧ { 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) )
37 1 36 bitri ⊢ ( 𝑊 ∈ ( 1 ClWWalksN 𝐺 ) ↔ ∃ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝑊 = ⟨“ 𝑣 ”⟩ ∧ { 𝑣 } ∈ ( Edg ‘ 𝐺 ) ) )