Theorem clwwlknon1loop

Description: If there is a loop at vertex X , the set of (closed) walks on X of length 1 as words over the set of vertices is a singleton containing the singleton word consisting of X . (Contributed by AV, 11-Feb-2022) (Revised by AV, 25-Feb-2022) (Proof shortened by AV, 25-Mar-2022)

	Ref	Expression
Hypotheses	clwwlknon1.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	clwwlknon1.c	⊢ 𝐶 = ( ClWWalksNOn ‘ 𝐺 )
	clwwlknon1.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	clwwlknon1loop	⊢ ( ( 𝑋 ∈ 𝑉 ∧ { 𝑋 } ∈ 𝐸 ) → ( 𝑋 𝐶 1 ) = { ⟨“ 𝑋 ”⟩ } )

Proof

Step	Hyp	Ref	Expression
1		clwwlknon1.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		clwwlknon1.c	⊢ 𝐶 = ( ClWWalksNOn ‘ 𝐺 )
3		clwwlknon1.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
4		simprl	⊢ ( ( 𝑤 ∈ Word 𝑉 ∧ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) ) → 𝑤 = ⟨“ 𝑋 ”⟩ )
5		s1cl	⊢ ( 𝑋 ∈ 𝑉 → ⟨“ 𝑋 ”⟩ ∈ Word 𝑉 )
6	5	adantr	⊢ ( ( 𝑋 ∈ 𝑉 ∧ { 𝑋 } ∈ 𝐸 ) → ⟨“ 𝑋 ”⟩ ∈ Word 𝑉 )
7	6	adantr	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ { 𝑋 } ∈ 𝐸 ) ∧ 𝑤 = ⟨“ 𝑋 ”⟩ ) → ⟨“ 𝑋 ”⟩ ∈ Word 𝑉 )
8		eleq1	⊢ ( 𝑤 = ⟨“ 𝑋 ”⟩ → ( 𝑤 ∈ Word 𝑉 ↔ ⟨“ 𝑋 ”⟩ ∈ Word 𝑉 ) )
9	8	adantl	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ { 𝑋 } ∈ 𝐸 ) ∧ 𝑤 = ⟨“ 𝑋 ”⟩ ) → ( 𝑤 ∈ Word 𝑉 ↔ ⟨“ 𝑋 ”⟩ ∈ Word 𝑉 ) )
10	7 9	mpbird	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ { 𝑋 } ∈ 𝐸 ) ∧ 𝑤 = ⟨“ 𝑋 ”⟩ ) → 𝑤 ∈ Word 𝑉 )
11		simpr	⊢ ( ( 𝑋 ∈ 𝑉 ∧ { 𝑋 } ∈ 𝐸 ) → { 𝑋 } ∈ 𝐸 )
12	11	anim1ci	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ { 𝑋 } ∈ 𝐸 ) ∧ 𝑤 = ⟨“ 𝑋 ”⟩ ) → ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) )
13	10 12	jca	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ { 𝑋 } ∈ 𝐸 ) ∧ 𝑤 = ⟨“ 𝑋 ”⟩ ) → ( 𝑤 ∈ Word 𝑉 ∧ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) ) )
14	13	ex	⊢ ( ( 𝑋 ∈ 𝑉 ∧ { 𝑋 } ∈ 𝐸 ) → ( 𝑤 = ⟨“ 𝑋 ”⟩ → ( 𝑤 ∈ Word 𝑉 ∧ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) ) ) )
15	4 14	impbid2	⊢ ( ( 𝑋 ∈ 𝑉 ∧ { 𝑋 } ∈ 𝐸 ) → ( ( 𝑤 ∈ Word 𝑉 ∧ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) ) ↔ 𝑤 = ⟨“ 𝑋 ”⟩ ) )
16	15	alrimiv	⊢ ( ( 𝑋 ∈ 𝑉 ∧ { 𝑋 } ∈ 𝐸 ) → ∀ 𝑤 ( ( 𝑤 ∈ Word 𝑉 ∧ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) ) ↔ 𝑤 = ⟨“ 𝑋 ”⟩ ) )
17	1 2 3	clwwlknon1	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 𝐶 1 ) = { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) } )
18	17	eqeq1d	⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝑋 𝐶 1 ) = { ⟨“ 𝑋 ”⟩ } ↔ { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) } = { ⟨“ 𝑋 ”⟩ } ) )
19	18	adantr	⊢ ( ( 𝑋 ∈ 𝑉 ∧ { 𝑋 } ∈ 𝐸 ) → ( ( 𝑋 𝐶 1 ) = { ⟨“ 𝑋 ”⟩ } ↔ { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) } = { ⟨“ 𝑋 ”⟩ } ) )
20		rabeqsn	⊢ ( { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) } = { ⟨“ 𝑋 ”⟩ } ↔ ∀ 𝑤 ( ( 𝑤 ∈ Word 𝑉 ∧ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) ) ↔ 𝑤 = ⟨“ 𝑋 ”⟩ ) )
21	19 20	bitrdi	⊢ ( ( 𝑋 ∈ 𝑉 ∧ { 𝑋 } ∈ 𝐸 ) → ( ( 𝑋 𝐶 1 ) = { ⟨“ 𝑋 ”⟩ } ↔ ∀ 𝑤 ( ( 𝑤 ∈ Word 𝑉 ∧ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) ) ↔ 𝑤 = ⟨“ 𝑋 ”⟩ ) ) )
22	16 21	mpbird	⊢ ( ( 𝑋 ∈ 𝑉 ∧ { 𝑋 } ∈ 𝐸 ) → ( 𝑋 𝐶 1 ) = { ⟨“ 𝑋 ”⟩ } )