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	|- V = ( Vtx ` G )
	clwwlknon1.c	|- C = ( ClWWalksNOn ` G )
	clwwlknon1.e	|- E = ( Edg ` G )
Assertion	clwwlknon1loop	|- ( ( X e. V /\ { X } e. E ) -> ( X C 1 ) = { <" X "> } )

Proof

Step	Hyp	Ref	Expression
1		clwwlknon1.v	|- V = ( Vtx ` G )
2		clwwlknon1.c	|- C = ( ClWWalksNOn ` G )
3		clwwlknon1.e	|- E = ( Edg ` G )
4		simprl	|- ( ( w e. Word V /\ ( w = <" X "> /\ { X } e. E ) ) -> w = <" X "> )
5		s1cl	|- ( X e. V -> <" X "> e. Word V )
6	5	adantr	|- ( ( X e. V /\ { X } e. E ) -> <" X "> e. Word V )
7	6	adantr	|- ( ( ( X e. V /\ { X } e. E ) /\ w = <" X "> ) -> <" X "> e. Word V )
8		eleq1	|- ( w = <" X "> -> ( w e. Word V <-> <" X "> e. Word V ) )
9	8	adantl	|- ( ( ( X e. V /\ { X } e. E ) /\ w = <" X "> ) -> ( w e. Word V <-> <" X "> e. Word V ) )
10	7 9	mpbird	|- ( ( ( X e. V /\ { X } e. E ) /\ w = <" X "> ) -> w e. Word V )
11		simpr	|- ( ( X e. V /\ { X } e. E ) -> { X } e. E )
12	11	anim1ci	|- ( ( ( X e. V /\ { X } e. E ) /\ w = <" X "> ) -> ( w = <" X "> /\ { X } e. E ) )
13	10 12	jca	|- ( ( ( X e. V /\ { X } e. E ) /\ w = <" X "> ) -> ( w e. Word V /\ ( w = <" X "> /\ { X } e. E ) ) )
14	13	ex	|- ( ( X e. V /\ { X } e. E ) -> ( w = <" X "> -> ( w e. Word V /\ ( w = <" X "> /\ { X } e. E ) ) ) )
15	4 14	impbid2	|- ( ( X e. V /\ { X } e. E ) -> ( ( w e. Word V /\ ( w = <" X "> /\ { X } e. E ) ) <-> w = <" X "> ) )
16	15	alrimiv	|- ( ( X e. V /\ { X } e. E ) -> A. w ( ( w e. Word V /\ ( w = <" X "> /\ { X } e. E ) ) <-> w = <" X "> ) )
17	1 2 3	clwwlknon1	|- ( X e. V -> ( X C 1 ) = { w e. Word V | ( w = <" X "> /\ { X } e. E ) } )
18	17	eqeq1d	|- ( X e. V -> ( ( X C 1 ) = { <" X "> } <-> { w e. Word V | ( w = <" X "> /\ { X } e. E ) } = { <" X "> } ) )
19	18	adantr	|- ( ( X e. V /\ { X } e. E ) -> ( ( X C 1 ) = { <" X "> } <-> { w e. Word V | ( w = <" X "> /\ { X } e. E ) } = { <" X "> } ) )
20		rabeqsn	|- ( { w e. Word V | ( w = <" X "> /\ { X } e. E ) } = { <" X "> } <-> A. w ( ( w e. Word V /\ ( w = <" X "> /\ { X } e. E ) ) <-> w = <" X "> ) )
21	19 20	bitrdi	|- ( ( X e. V /\ { X } e. E ) -> ( ( X C 1 ) = { <" X "> } <-> A. w ( ( w e. Word V /\ ( w = <" X "> /\ { X } e. E ) ) <-> w = <" X "> ) ) )
22	16 21	mpbird	|- ( ( X e. V /\ { X } e. E ) -> ( X C 1 ) = { <" X "> } )