Theorem clwwlknon1nloop

Description: If there is no loop at vertex X , the set of (closed) walks on X of length 1 as words over the set of vertices is empty. (Contributed by AV, 11-Feb-2022) (Revised by AV, 25-Mar-2022)

	Ref	Expression
Hypotheses	clwwlknon1.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	clwwlknon1.c	⊢ 𝐶 = ( ClWWalksNOn ‘ 𝐺 )
	clwwlknon1.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	clwwlknon1nloop	⊢ ( { 𝑋 } ∉ 𝐸 → ( 𝑋 𝐶 1 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		clwwlknon1.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		clwwlknon1.c	⊢ 𝐶 = ( ClWWalksNOn ‘ 𝐺 )
3		clwwlknon1.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
4	1 2 3	clwwlknon1	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 𝐶 1 ) = { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) } )
5	4	adantr	⊢ ( ( 𝑋 ∈ 𝑉 ∧ { 𝑋 } ∉ 𝐸 ) → ( 𝑋 𝐶 1 ) = { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) } )
6		df-nel	⊢ ( { 𝑋 } ∉ 𝐸 ↔ ¬ { 𝑋 } ∈ 𝐸 )
7	6	biimpi	⊢ ( { 𝑋 } ∉ 𝐸 → ¬ { 𝑋 } ∈ 𝐸 )
8	7	olcd	⊢ ( { 𝑋 } ∉ 𝐸 → ( ¬ 𝑤 = ⟨“ 𝑋 ”⟩ ∨ ¬ { 𝑋 } ∈ 𝐸 ) )
9	8	ad2antlr	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ { 𝑋 } ∉ 𝐸 ) ∧ 𝑤 ∈ Word 𝑉 ) → ( ¬ 𝑤 = ⟨“ 𝑋 ”⟩ ∨ ¬ { 𝑋 } ∈ 𝐸 ) )
10		ianor	⊢ ( ¬ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) ↔ ( ¬ 𝑤 = ⟨“ 𝑋 ”⟩ ∨ ¬ { 𝑋 } ∈ 𝐸 ) )
11	9 10	sylibr	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ { 𝑋 } ∉ 𝐸 ) ∧ 𝑤 ∈ Word 𝑉 ) → ¬ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) )
12	11	ralrimiva	⊢ ( ( 𝑋 ∈ 𝑉 ∧ { 𝑋 } ∉ 𝐸 ) → ∀ 𝑤 ∈ Word 𝑉 ¬ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) )
13		rabeq0	⊢ ( { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) } = ∅ ↔ ∀ 𝑤 ∈ Word 𝑉 ¬ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) )
14	12 13	sylibr	⊢ ( ( 𝑋 ∈ 𝑉 ∧ { 𝑋 } ∉ 𝐸 ) → { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 = ⟨“ 𝑋 ”⟩ ∧ { 𝑋 } ∈ 𝐸 ) } = ∅ )
15	5 14	eqtrd	⊢ ( ( 𝑋 ∈ 𝑉 ∧ { 𝑋 } ∉ 𝐸 ) → ( 𝑋 𝐶 1 ) = ∅ )
16	2	oveqi	⊢ ( 𝑋 𝐶 1 ) = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 1 )
17	1	eleq2i	⊢ ( 𝑋 ∈ 𝑉 ↔ 𝑋 ∈ ( Vtx ‘ 𝐺 ) )
18	17	notbii	⊢ ( ¬ 𝑋 ∈ 𝑉 ↔ ¬ 𝑋 ∈ ( Vtx ‘ 𝐺 ) )
19	18	biimpi	⊢ ( ¬ 𝑋 ∈ 𝑉 → ¬ 𝑋 ∈ ( Vtx ‘ 𝐺 ) )
20	19	intnanrd	⊢ ( ¬ 𝑋 ∈ 𝑉 → ¬ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 1 ∈ ℕ ) )
21		clwwlknon0	⊢ ( ¬ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ 1 ∈ ℕ ) → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 1 ) = ∅ )
22	20 21	syl	⊢ ( ¬ 𝑋 ∈ 𝑉 → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 1 ) = ∅ )
23	16 22	syl5eq	⊢ ( ¬ 𝑋 ∈ 𝑉 → ( 𝑋 𝐶 1 ) = ∅ )
24	23	adantr	⊢ ( ( ¬ 𝑋 ∈ 𝑉 ∧ { 𝑋 } ∉ 𝐸 ) → ( 𝑋 𝐶 1 ) = ∅ )
25	15 24	pm2.61ian	⊢ ( { 𝑋 } ∉ 𝐸 → ( 𝑋 𝐶 1 ) = ∅ )