Theorem uhgr3cyclexlem

Description: Lemma for uhgr3cyclex . (Contributed by AV, 12-Feb-2021)

	Ref	Expression
Hypotheses	uhgr3cyclex.v	|- V = ( Vtx ` G )
	uhgr3cyclex.e	|- E = ( Edg ` G )
	uhgr3cyclex.i	|- I = ( iEdg ` G )
Assertion	uhgr3cyclexlem	|- ( ( ( ( A e. V /\ B e. V ) /\ A =/= B ) /\ ( ( J e. dom I /\ { B , C } = ( I ` J ) ) /\ ( K e. dom I /\ { C , A } = ( I ` K ) ) ) ) -> J =/= K )

Proof

Step	Hyp	Ref	Expression
1		uhgr3cyclex.v	|- V = ( Vtx ` G )
2		uhgr3cyclex.e	|- E = ( Edg ` G )
3		uhgr3cyclex.i	|- I = ( iEdg ` G )
4		fveq2	|- ( J = K -> ( I ` J ) = ( I ` K ) )
5	4	eqeq2d	|- ( J = K -> ( { B , C } = ( I ` J ) <-> { B , C } = ( I ` K ) ) )
6		eqeq2	|- ( ( I ` K ) = { C , A } -> ( { B , C } = ( I ` K ) <-> { B , C } = { C , A } ) )
7	6	eqcoms	|- ( { C , A } = ( I ` K ) -> ( { B , C } = ( I ` K ) <-> { B , C } = { C , A } ) )
8		prcom	|- { C , A } = { A , C }
9	8	eqeq1i	|- ( { C , A } = { B , C } <-> { A , C } = { B , C } )
10		simpl	|- ( ( A e. V /\ B e. V ) -> A e. V )
11		simpr	|- ( ( A e. V /\ B e. V ) -> B e. V )
12	10 11	preq1b	|- ( ( A e. V /\ B e. V ) -> ( { A , C } = { B , C } <-> A = B ) )
13	12	biimpcd	|- ( { A , C } = { B , C } -> ( ( A e. V /\ B e. V ) -> A = B ) )
14	9 13	sylbi	|- ( { C , A } = { B , C } -> ( ( A e. V /\ B e. V ) -> A = B ) )
15	14	eqcoms	|- ( { B , C } = { C , A } -> ( ( A e. V /\ B e. V ) -> A = B ) )
16	7 15	syl6bi	|- ( { C , A } = ( I ` K ) -> ( { B , C } = ( I ` K ) -> ( ( A e. V /\ B e. V ) -> A = B ) ) )
17	16	adantl	|- ( ( K e. dom I /\ { C , A } = ( I ` K ) ) -> ( { B , C } = ( I ` K ) -> ( ( A e. V /\ B e. V ) -> A = B ) ) )
18	17	com12	|- ( { B , C } = ( I ` K ) -> ( ( K e. dom I /\ { C , A } = ( I ` K ) ) -> ( ( A e. V /\ B e. V ) -> A = B ) ) )
19	5 18	syl6bi	|- ( J = K -> ( { B , C } = ( I ` J ) -> ( ( K e. dom I /\ { C , A } = ( I ` K ) ) -> ( ( A e. V /\ B e. V ) -> A = B ) ) ) )
20	19	adantld	|- ( J = K -> ( ( J e. dom I /\ { B , C } = ( I ` J ) ) -> ( ( K e. dom I /\ { C , A } = ( I ` K ) ) -> ( ( A e. V /\ B e. V ) -> A = B ) ) ) )
21	20	com14	|- ( ( A e. V /\ B e. V ) -> ( ( J e. dom I /\ { B , C } = ( I ` J ) ) -> ( ( K e. dom I /\ { C , A } = ( I ` K ) ) -> ( J = K -> A = B ) ) ) )
22	21	imp32	|- ( ( ( A e. V /\ B e. V ) /\ ( ( J e. dom I /\ { B , C } = ( I ` J ) ) /\ ( K e. dom I /\ { C , A } = ( I ` K ) ) ) ) -> ( J = K -> A = B ) )
23	22	necon3d	|- ( ( ( A e. V /\ B e. V ) /\ ( ( J e. dom I /\ { B , C } = ( I ` J ) ) /\ ( K e. dom I /\ { C , A } = ( I ` K ) ) ) ) -> ( A =/= B -> J =/= K ) )
24	23	impancom	|- ( ( ( A e. V /\ B e. V ) /\ A =/= B ) -> ( ( ( J e. dom I /\ { B , C } = ( I ` J ) ) /\ ( K e. dom I /\ { C , A } = ( I ` K ) ) ) -> J =/= K ) )
25	24	imp	|- ( ( ( ( A e. V /\ B e. V ) /\ A =/= B ) /\ ( ( J e. dom I /\ { B , C } = ( I ` J ) ) /\ ( K e. dom I /\ { C , A } = ( I ` K ) ) ) ) -> J =/= K )