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 ) )