This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrdi 
 |-  ( { 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 biimtrdi 
 |-  ( 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 )