Theorem s2elclwwlknon2

Description: Sufficient conditions of a doubleton word to represent a closed walk on vertex X of length 2 . (Contributed by AV, 11-May-2022)

	Ref	Expression
Hypotheses	clwwlknon2.c	|- C = ( ClWWalksNOn ` G )
	clwwlknon2x.v	|- V = ( Vtx ` G )
	clwwlknon2x.e	|- E = ( Edg ` G )
Assertion	s2elclwwlknon2	|- ( ( X e. V /\ Y e. V /\ { X , Y } e. E ) -> <" X Y "> e. ( X C 2 ) )

Proof

Step	Hyp	Ref	Expression
1		clwwlknon2.c	|- C = ( ClWWalksNOn ` G )
2		clwwlknon2x.v	|- V = ( Vtx ` G )
3		clwwlknon2x.e	|- E = ( Edg ` G )
4		s2cl	|- ( ( X e. V /\ Y e. V ) -> <" X Y "> e. Word V )
5	4	3adant3	|- ( ( X e. V /\ Y e. V /\ { X , Y } e. E ) -> <" X Y "> e. Word V )
6		s2len	|- ( # ` <" X Y "> ) = 2
7	6	a1i	|- ( ( X e. V /\ Y e. V /\ { X , Y } e. E ) -> ( # ` <" X Y "> ) = 2 )
8		s2fv0	|- ( X e. V -> ( <" X Y "> ` 0 ) = X )
9	8	adantr	|- ( ( X e. V /\ Y e. V ) -> ( <" X Y "> ` 0 ) = X )
10		s2fv1	|- ( Y e. V -> ( <" X Y "> ` 1 ) = Y )
11	10	adantl	|- ( ( X e. V /\ Y e. V ) -> ( <" X Y "> ` 1 ) = Y )
12	9 11	preq12d	|- ( ( X e. V /\ Y e. V ) -> { ( <" X Y "> ` 0 ) , ( <" X Y "> ` 1 ) } = { X , Y } )
13	12	eqcomd	|- ( ( X e. V /\ Y e. V ) -> { X , Y } = { ( <" X Y "> ` 0 ) , ( <" X Y "> ` 1 ) } )
14	13	eleq1d	|- ( ( X e. V /\ Y e. V ) -> ( { X , Y } e. E <-> { ( <" X Y "> ` 0 ) , ( <" X Y "> ` 1 ) } e. E ) )
15	14	biimp3a	|- ( ( X e. V /\ Y e. V /\ { X , Y } e. E ) -> { ( <" X Y "> ` 0 ) , ( <" X Y "> ` 1 ) } e. E )
16	9	3adant3	|- ( ( X e. V /\ Y e. V /\ { X , Y } e. E ) -> ( <" X Y "> ` 0 ) = X )
17	7 15 16	3jca	|- ( ( X e. V /\ Y e. V /\ { X , Y } e. E ) -> ( ( # ` <" X Y "> ) = 2 /\ { ( <" X Y "> ` 0 ) , ( <" X Y "> ` 1 ) } e. E /\ ( <" X Y "> ` 0 ) = X ) )
18		fveqeq2	|- ( w = <" X Y "> -> ( ( # ` w ) = 2 <-> ( # ` <" X Y "> ) = 2 ) )
19		fveq1	|- ( w = <" X Y "> -> ( w ` 0 ) = ( <" X Y "> ` 0 ) )
20		fveq1	|- ( w = <" X Y "> -> ( w ` 1 ) = ( <" X Y "> ` 1 ) )
21	19 20	preq12d	|- ( w = <" X Y "> -> { ( w ` 0 ) , ( w ` 1 ) } = { ( <" X Y "> ` 0 ) , ( <" X Y "> ` 1 ) } )
22	21	eleq1d	|- ( w = <" X Y "> -> ( { ( w ` 0 ) , ( w ` 1 ) } e. E <-> { ( <" X Y "> ` 0 ) , ( <" X Y "> ` 1 ) } e. E ) )
23	19	eqeq1d	|- ( w = <" X Y "> -> ( ( w ` 0 ) = X <-> ( <" X Y "> ` 0 ) = X ) )
24	18 22 23	3anbi123d	|- ( w = <" X Y "> -> ( ( ( # ` w ) = 2 /\ { ( w ` 0 ) , ( w ` 1 ) } e. E /\ ( w ` 0 ) = X ) <-> ( ( # ` <" X Y "> ) = 2 /\ { ( <" X Y "> ` 0 ) , ( <" X Y "> ` 1 ) } e. E /\ ( <" X Y "> ` 0 ) = X ) ) )
25	1 2 3	clwwlknon2x	|- ( X C 2 ) = { w e. Word V | ( ( # ` w ) = 2 /\ { ( w ` 0 ) , ( w ` 1 ) } e. E /\ ( w ` 0 ) = X ) }
26	24 25	elrab2	|- ( <" X Y "> e. ( X C 2 ) <-> ( <" X Y "> e. Word V /\ ( ( # ` <" X Y "> ) = 2 /\ { ( <" X Y "> ` 0 ) , ( <" X Y "> ` 1 ) } e. E /\ ( <" X Y "> ` 0 ) = X ) ) )
27	5 17 26	sylanbrc	|- ( ( X e. V /\ Y e. V /\ { X , Y } e. E ) -> <" X Y "> e. ( X C 2 ) )