Theorem clwwlknon1sn

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

	Ref	Expression
Hypotheses	clwwlknon1.v	|- V = ( Vtx ` G )
	clwwlknon1.c	|- C = ( ClWWalksNOn ` G )
	clwwlknon1.e	|- E = ( Edg ` G )
Assertion	clwwlknon1sn	|- ( X e. V -> ( ( X C 1 ) = { <" X "> } <-> { X } e. E ) )

Proof

Step	Hyp	Ref	Expression
1		clwwlknon1.v	|- V = ( Vtx ` G )
2		clwwlknon1.c	|- C = ( ClWWalksNOn ` G )
3		clwwlknon1.e	|- E = ( Edg ` G )
4		df-nel	|- ( { X } e/ E <-> -. { X } e. E )
5	1 2 3	clwwlknon1nloop	|- ( { X } e/ E -> ( X C 1 ) = (/) )
6	5	adantl	|- ( ( X e. V /\ { X } e/ E ) -> ( X C 1 ) = (/) )
7		s1cli	|- <" X "> e. Word _V
8	7	elexi	|- <" X "> e. _V
9	8	snnz	|- { <" X "> } =/= (/)
10	9	nesymi	|- -. (/) = { <" X "> }
11		eqeq1	|- ( ( X C 1 ) = (/) -> ( ( X C 1 ) = { <" X "> } <-> (/) = { <" X "> } ) )
12	10 11	mtbiri	|- ( ( X C 1 ) = (/) -> -. ( X C 1 ) = { <" X "> } )
13	6 12	syl	|- ( ( X e. V /\ { X } e/ E ) -> -. ( X C 1 ) = { <" X "> } )
14	13	ex	|- ( X e. V -> ( { X } e/ E -> -. ( X C 1 ) = { <" X "> } ) )
15	4 14	syl5bir	|- ( X e. V -> ( -. { X } e. E -> -. ( X C 1 ) = { <" X "> } ) )
16	15	con4d	|- ( X e. V -> ( ( X C 1 ) = { <" X "> } -> { X } e. E ) )
17	1 2 3	clwwlknon1loop	|- ( ( X e. V /\ { X } e. E ) -> ( X C 1 ) = { <" X "> } )
18	17	ex	|- ( X e. V -> ( { X } e. E -> ( X C 1 ) = { <" X "> } ) )
19	16 18	impbid	|- ( X e. V -> ( ( X C 1 ) = { <" X "> } <-> { X } e. E ) )