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∈V∧B∈V∧A≠B∧J∈dom⁡I∧BC=I⁡J∧K∈dom⁡I∧CA=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→BC=I⁡J↔BC=I⁡K
6 eqeq2 ⊢I⁡K=CA→BC=I⁡K↔BC=CA
7 6 eqcoms ⊢CA=I⁡K→BC=I⁡K↔BC=CA
8 prcom ⊢CA=AC
9 8 eqeq1i ⊢CA=BC↔AC=BC
10 simpl ⊢A∈V∧B∈V→A∈V
11 simpr ⊢A∈V∧B∈V→B∈V
12 10 11 preq1b ⊢A∈V∧B∈V→AC=BC↔A=B
13 12 biimpcd ⊢AC=BC→A∈V∧B∈V→A=B
14 9 13 sylbi ⊢CA=BC→A∈V∧B∈V→A=B
15 14 eqcoms ⊢BC=CA→A∈V∧B∈V→A=B
16 7 15 syl6bi ⊢CA=I⁡K→BC=I⁡K→A∈V∧B∈V→A=B
17 16 adantl ⊢K∈dom⁡I∧CA=I⁡K→BC=I⁡K→A∈V∧B∈V→A=B
18 17 com12 ⊢BC=I⁡K→K∈dom⁡I∧CA=I⁡K→A∈V∧B∈V→A=B
19 5 18 syl6bi ⊢J=K→BC=I⁡J→K∈dom⁡I∧CA=I⁡K→A∈V∧B∈V→A=B
20 19 adantld ⊢J=K→J∈dom⁡I∧BC=I⁡J→K∈dom⁡I∧CA=I⁡K→A∈V∧B∈V→A=B
21 20 com14 ⊢A∈V∧B∈V→J∈dom⁡I∧BC=I⁡J→K∈dom⁡I∧CA=I⁡K→J=K→A=B
22 21 imp32 ⊢A∈V∧B∈V∧J∈dom⁡I∧BC=I⁡J∧K∈dom⁡I∧CA=I⁡K→J=K→A=B
23 22 necon3d ⊢A∈V∧B∈V∧J∈dom⁡I∧BC=I⁡J∧K∈dom⁡I∧CA=I⁡K→A≠B→J≠K
24 23 impancom ⊢A∈V∧B∈V∧A≠B→J∈dom⁡I∧BC=I⁡J∧K∈dom⁡I∧CA=I⁡K→J≠K
25 24 imp ⊢A∈V∧B∈V∧A≠B∧J∈dom⁡I∧BC=I⁡J∧K∈dom⁡I∧CA=I⁡K→J≠K