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

Proof

Step	Hyp	Ref	Expression
1		clwwlknon1.v	|- V = ( Vtx ` G )
2		clwwlknon1.c	|- C = ( ClWWalksNOn ` G )
3		clwwlknon1.e	|- E = ( Edg ` G )
4	1 2 3	clwwlknon1	|- ( X e. V -> ( X C 1 ) = { w e. Word V | ( w = <" X "> /\ { X } e. E ) } )
5	4	adantr	|- ( ( X e. V /\ { X } e/ E ) -> ( X C 1 ) = { w e. Word V | ( w = <" X "> /\ { X } e. E ) } )
6		df-nel	|- ( { X } e/ E <-> -. { X } e. E )
7	6	biimpi	|- ( { X } e/ E -> -. { X } e. E )
8	7	olcd	|- ( { X } e/ E -> ( -. w = <" X "> \/ -. { X } e. E ) )
9	8	ad2antlr	|- ( ( ( X e. V /\ { X } e/ E ) /\ w e. Word V ) -> ( -. w = <" X "> \/ -. { X } e. E ) )
10		ianor	|- ( -. ( w = <" X "> /\ { X } e. E ) <-> ( -. w = <" X "> \/ -. { X } e. E ) )
11	9 10	sylibr	|- ( ( ( X e. V /\ { X } e/ E ) /\ w e. Word V ) -> -. ( w = <" X "> /\ { X } e. E ) )
12	11	ralrimiva	|- ( ( X e. V /\ { X } e/ E ) -> A. w e. Word V -. ( w = <" X "> /\ { X } e. E ) )
13		rabeq0	|- ( { w e. Word V | ( w = <" X "> /\ { X } e. E ) } = (/) <-> A. w e. Word V -. ( w = <" X "> /\ { X } e. E ) )
14	12 13	sylibr	|- ( ( X e. V /\ { X } e/ E ) -> { w e. Word V | ( w = <" X "> /\ { X } e. E ) } = (/) )
15	5 14	eqtrd	|- ( ( X e. V /\ { X } e/ E ) -> ( X C 1 ) = (/) )
16	2	oveqi	|- ( X C 1 ) = ( X ( ClWWalksNOn ` G ) 1 )
17	1	eleq2i	|- ( X e. V <-> X e. ( Vtx ` G ) )
18	17	notbii	|- ( -. X e. V <-> -. X e. ( Vtx ` G ) )
19	18	biimpi	|- ( -. X e. V -> -. X e. ( Vtx ` G ) )
20	19	intnanrd	|- ( -. X e. V -> -. ( X e. ( Vtx ` G ) /\ 1 e. NN ) )
21		clwwlknon0	|- ( -. ( X e. ( Vtx ` G ) /\ 1 e. NN ) -> ( X ( ClWWalksNOn ` G ) 1 ) = (/) )
22	20 21	syl	|- ( -. X e. V -> ( X ( ClWWalksNOn ` G ) 1 ) = (/) )
23	16 22	syl5eq	|- ( -. X e. V -> ( X C 1 ) = (/) )
24	23	adantr	|- ( ( -. X e. V /\ { X } e/ E ) -> ( X C 1 ) = (/) )
25	15 24	pm2.61ian	|- ( { X } e/ E -> ( X C 1 ) = (/) )