Theorem 2cycl2d

Description: Construction of a 2-cycle from two given edges in a graph. (Contributed by BTernaryTau, 16-Oct-2023)

	Ref	Expression
Hypotheses	2cycl2d.1	|- P = <" A B A ">
	2cycl2d.2	|- F = <" J K ">
	2cycl2d.3	|- ( ph -> ( A e. V /\ B e. V ) )
	2cycl2d.4	|- ( ph -> A =/= B )
	2cycl2d.5	|- ( ph -> ( { A , B } C_ ( I ` J ) /\ { A , B } C_ ( I ` K ) ) )
	2cycl2d.6	|- V = ( Vtx ` G )
	2cycl2d.7	|- I = ( iEdg ` G )
	2cycl2d.8	|- ( ph -> J =/= K )
Assertion	2cycl2d	|- ( ph -> F ( Cycles ` G ) P )

Proof

Step	Hyp	Ref	Expression
1		2cycl2d.1	|- P = <" A B A ">
2		2cycl2d.2	|- F = <" J K ">
3		2cycl2d.3	|- ( ph -> ( A e. V /\ B e. V ) )
4		2cycl2d.4	|- ( ph -> A =/= B )
5		2cycl2d.5	|- ( ph -> ( { A , B } C_ ( I ` J ) /\ { A , B } C_ ( I ` K ) ) )
6		2cycl2d.6	|- V = ( Vtx ` G )
7		2cycl2d.7	|- I = ( iEdg ` G )
8		2cycl2d.8	|- ( ph -> J =/= K )
9		simpl	|- ( ( A e. V /\ B e. V ) -> A e. V )
10	3 9	jccir	|- ( ph -> ( ( A e. V /\ B e. V ) /\ A e. V ) )
11		df-3an	|- ( ( A e. V /\ B e. V /\ A e. V ) <-> ( ( A e. V /\ B e. V ) /\ A e. V ) )
12	10 11	sylibr	|- ( ph -> ( A e. V /\ B e. V /\ A e. V ) )
13	4	necomd	|- ( ph -> B =/= A )
14	4 13	jca	|- ( ph -> ( A =/= B /\ B =/= A ) )
15		prcom	|- { A , B } = { B , A }
16	15	sseq1i	|- ( { A , B } C_ ( I ` K ) <-> { B , A } C_ ( I ` K ) )
17	16	anbi2i	|- ( ( { A , B } C_ ( I ` J ) /\ { A , B } C_ ( I ` K ) ) <-> ( { A , B } C_ ( I ` J ) /\ { B , A } C_ ( I ` K ) ) )
18	5 17	sylib	|- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , A } C_ ( I ` K ) ) )
19		eqidd	|- ( ph -> A = A )
20	1 2 12 14 18 6 7 8 19	2cycld	|- ( ph -> F ( Cycles ` G ) P )