Metamath Proof Explorer


Theorem s2elclwwlknon2

Description: Sufficient conditions of a doubleton word to represent a closed walk on vertex X of length 2 . (Contributed by AV, 11-May-2022)

Ref Expression
Hypotheses clwwlknon2.c 𝐶 = ( ClWWalksNOn ‘ 𝐺 )
clwwlknon2x.v 𝑉 = ( Vtx ‘ 𝐺 )
clwwlknon2x.e 𝐸 = ( Edg ‘ 𝐺 )
Assertion s2elclwwlknon2 ( ( 𝑋𝑉𝑌𝑉 ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ⟨“ 𝑋 𝑌 ”⟩ ∈ ( 𝑋 𝐶 2 ) )

Proof

Step Hyp Ref Expression
1 clwwlknon2.c 𝐶 = ( ClWWalksNOn ‘ 𝐺 )
2 clwwlknon2x.v 𝑉 = ( Vtx ‘ 𝐺 )
3 clwwlknon2x.e 𝐸 = ( Edg ‘ 𝐺 )
4 s2cl ( ( 𝑋𝑉𝑌𝑉 ) → ⟨“ 𝑋 𝑌 ”⟩ ∈ Word 𝑉 )
5 4 3adant3 ( ( 𝑋𝑉𝑌𝑉 ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ⟨“ 𝑋 𝑌 ”⟩ ∈ Word 𝑉 )
6 s2len ( ♯ ‘ ⟨“ 𝑋 𝑌 ”⟩ ) = 2
7 6 a1i ( ( 𝑋𝑉𝑌𝑉 ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( ♯ ‘ ⟨“ 𝑋 𝑌 ”⟩ ) = 2 )
8 s2fv0 ( 𝑋𝑉 → ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 0 ) = 𝑋 )
9 8 adantr ( ( 𝑋𝑉𝑌𝑉 ) → ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 0 ) = 𝑋 )
10 s2fv1 ( 𝑌𝑉 → ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 1 ) = 𝑌 )
11 10 adantl ( ( 𝑋𝑉𝑌𝑉 ) → ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 1 ) = 𝑌 )
12 9 11 preq12d ( ( 𝑋𝑉𝑌𝑉 ) → { ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 0 ) , ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 1 ) } = { 𝑋 , 𝑌 } )
13 12 eqcomd ( ( 𝑋𝑉𝑌𝑉 ) → { 𝑋 , 𝑌 } = { ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 0 ) , ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 1 ) } )
14 13 eleq1d ( ( 𝑋𝑉𝑌𝑉 ) → ( { 𝑋 , 𝑌 } ∈ 𝐸 ↔ { ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 0 ) , ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 1 ) } ∈ 𝐸 ) )
15 14 biimp3a ( ( 𝑋𝑉𝑌𝑉 ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → { ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 0 ) , ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 1 ) } ∈ 𝐸 )
16 9 3adant3 ( ( 𝑋𝑉𝑌𝑉 ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 0 ) = 𝑋 )
17 7 15 16 3jca ( ( 𝑋𝑉𝑌𝑉 ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( ( ♯ ‘ ⟨“ 𝑋 𝑌 ”⟩ ) = 2 ∧ { ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 0 ) , ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 1 ) } ∈ 𝐸 ∧ ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 0 ) = 𝑋 ) )
18 fveqeq2 ( 𝑤 = ⟨“ 𝑋 𝑌 ”⟩ → ( ( ♯ ‘ 𝑤 ) = 2 ↔ ( ♯ ‘ ⟨“ 𝑋 𝑌 ”⟩ ) = 2 ) )
19 fveq1 ( 𝑤 = ⟨“ 𝑋 𝑌 ”⟩ → ( 𝑤 ‘ 0 ) = ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 0 ) )
20 fveq1 ( 𝑤 = ⟨“ 𝑋 𝑌 ”⟩ → ( 𝑤 ‘ 1 ) = ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 1 ) )
21 19 20 preq12d ( 𝑤 = ⟨“ 𝑋 𝑌 ”⟩ → { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } = { ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 0 ) , ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 1 ) } )
22 21 eleq1d ( 𝑤 = ⟨“ 𝑋 𝑌 ”⟩ → ( { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝐸 ↔ { ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 0 ) , ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 1 ) } ∈ 𝐸 ) )
23 19 eqeq1d ( 𝑤 = ⟨“ 𝑋 𝑌 ”⟩ → ( ( 𝑤 ‘ 0 ) = 𝑋 ↔ ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 0 ) = 𝑋 ) )
24 18 22 23 3anbi123d ( 𝑤 = ⟨“ 𝑋 𝑌 ”⟩ → ( ( ( ♯ ‘ 𝑤 ) = 2 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝐸 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ↔ ( ( ♯ ‘ ⟨“ 𝑋 𝑌 ”⟩ ) = 2 ∧ { ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 0 ) , ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 1 ) } ∈ 𝐸 ∧ ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 0 ) = 𝑋 ) ) )
25 1 2 3 clwwlknon2x ( 𝑋 𝐶 2 ) = { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝐸 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) }
26 24 25 elrab2 ( ⟨“ 𝑋 𝑌 ”⟩ ∈ ( 𝑋 𝐶 2 ) ↔ ( ⟨“ 𝑋 𝑌 ”⟩ ∈ Word 𝑉 ∧ ( ( ♯ ‘ ⟨“ 𝑋 𝑌 ”⟩ ) = 2 ∧ { ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 0 ) , ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 1 ) } ∈ 𝐸 ∧ ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 0 ) = 𝑋 ) ) )
27 5 17 26 sylanbrc ( ( 𝑋𝑉𝑌𝑉 ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ⟨“ 𝑋 𝑌 ”⟩ ∈ ( 𝑋 𝐶 2 ) )