Metamath Proof Explorer


Theorem uhgr3cyclexlem

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

Ref Expression
Hypotheses uhgr3cyclex.v 𝑉 = ( Vtx ‘ 𝐺 )
uhgr3cyclex.e 𝐸 = ( Edg ‘ 𝐺 )
uhgr3cyclex.i 𝐼 = ( iEdg ‘ 𝐺 )
Assertion uhgr3cyclexlem ( ( ( ( 𝐴𝑉𝐵𝑉 ) ∧ 𝐴𝐵 ) ∧ ( ( 𝐽 ∈ dom 𝐼 ∧ { 𝐵 , 𝐶 } = ( 𝐼𝐽 ) ) ∧ ( 𝐾 ∈ dom 𝐼 ∧ { 𝐶 , 𝐴 } = ( 𝐼𝐾 ) ) ) ) → 𝐽𝐾 )

Proof

Step Hyp Ref Expression
1 uhgr3cyclex.v 𝑉 = ( Vtx ‘ 𝐺 )
2 uhgr3cyclex.e 𝐸 = ( Edg ‘ 𝐺 )
3 uhgr3cyclex.i 𝐼 = ( iEdg ‘ 𝐺 )
4 fveq2 ( 𝐽 = 𝐾 → ( 𝐼𝐽 ) = ( 𝐼𝐾 ) )
5 4 eqeq2d ( 𝐽 = 𝐾 → ( { 𝐵 , 𝐶 } = ( 𝐼𝐽 ) ↔ { 𝐵 , 𝐶 } = ( 𝐼𝐾 ) ) )
6 eqeq2 ( ( 𝐼𝐾 ) = { 𝐶 , 𝐴 } → ( { 𝐵 , 𝐶 } = ( 𝐼𝐾 ) ↔ { 𝐵 , 𝐶 } = { 𝐶 , 𝐴 } ) )
7 6 eqcoms ( { 𝐶 , 𝐴 } = ( 𝐼𝐾 ) → ( { 𝐵 , 𝐶 } = ( 𝐼𝐾 ) ↔ { 𝐵 , 𝐶 } = { 𝐶 , 𝐴 } ) )
8 prcom { 𝐶 , 𝐴 } = { 𝐴 , 𝐶 }
9 8 eqeq1i ( { 𝐶 , 𝐴 } = { 𝐵 , 𝐶 } ↔ { 𝐴 , 𝐶 } = { 𝐵 , 𝐶 } )
10 simpl ( ( 𝐴𝑉𝐵𝑉 ) → 𝐴𝑉 )
11 simpr ( ( 𝐴𝑉𝐵𝑉 ) → 𝐵𝑉 )
12 10 11 preq1b ( ( 𝐴𝑉𝐵𝑉 ) → ( { 𝐴 , 𝐶 } = { 𝐵 , 𝐶 } ↔ 𝐴 = 𝐵 ) )
13 12 biimpcd ( { 𝐴 , 𝐶 } = { 𝐵 , 𝐶 } → ( ( 𝐴𝑉𝐵𝑉 ) → 𝐴 = 𝐵 ) )
14 9 13 sylbi ( { 𝐶 , 𝐴 } = { 𝐵 , 𝐶 } → ( ( 𝐴𝑉𝐵𝑉 ) → 𝐴 = 𝐵 ) )
15 14 eqcoms ( { 𝐵 , 𝐶 } = { 𝐶 , 𝐴 } → ( ( 𝐴𝑉𝐵𝑉 ) → 𝐴 = 𝐵 ) )
16 7 15 syl6bi ( { 𝐶 , 𝐴 } = ( 𝐼𝐾 ) → ( { 𝐵 , 𝐶 } = ( 𝐼𝐾 ) → ( ( 𝐴𝑉𝐵𝑉 ) → 𝐴 = 𝐵 ) ) )
17 16 adantl ( ( 𝐾 ∈ dom 𝐼 ∧ { 𝐶 , 𝐴 } = ( 𝐼𝐾 ) ) → ( { 𝐵 , 𝐶 } = ( 𝐼𝐾 ) → ( ( 𝐴𝑉𝐵𝑉 ) → 𝐴 = 𝐵 ) ) )
18 17 com12 ( { 𝐵 , 𝐶 } = ( 𝐼𝐾 ) → ( ( 𝐾 ∈ dom 𝐼 ∧ { 𝐶 , 𝐴 } = ( 𝐼𝐾 ) ) → ( ( 𝐴𝑉𝐵𝑉 ) → 𝐴 = 𝐵 ) ) )
19 5 18 syl6bi ( 𝐽 = 𝐾 → ( { 𝐵 , 𝐶 } = ( 𝐼𝐽 ) → ( ( 𝐾 ∈ dom 𝐼 ∧ { 𝐶 , 𝐴 } = ( 𝐼𝐾 ) ) → ( ( 𝐴𝑉𝐵𝑉 ) → 𝐴 = 𝐵 ) ) ) )
20 19 adantld ( 𝐽 = 𝐾 → ( ( 𝐽 ∈ dom 𝐼 ∧ { 𝐵 , 𝐶 } = ( 𝐼𝐽 ) ) → ( ( 𝐾 ∈ dom 𝐼 ∧ { 𝐶 , 𝐴 } = ( 𝐼𝐾 ) ) → ( ( 𝐴𝑉𝐵𝑉 ) → 𝐴 = 𝐵 ) ) ) )
21 20 com14 ( ( 𝐴𝑉𝐵𝑉 ) → ( ( 𝐽 ∈ dom 𝐼 ∧ { 𝐵 , 𝐶 } = ( 𝐼𝐽 ) ) → ( ( 𝐾 ∈ dom 𝐼 ∧ { 𝐶 , 𝐴 } = ( 𝐼𝐾 ) ) → ( 𝐽 = 𝐾𝐴 = 𝐵 ) ) ) )
22 21 imp32 ( ( ( 𝐴𝑉𝐵𝑉 ) ∧ ( ( 𝐽 ∈ dom 𝐼 ∧ { 𝐵 , 𝐶 } = ( 𝐼𝐽 ) ) ∧ ( 𝐾 ∈ dom 𝐼 ∧ { 𝐶 , 𝐴 } = ( 𝐼𝐾 ) ) ) ) → ( 𝐽 = 𝐾𝐴 = 𝐵 ) )
23 22 necon3d ( ( ( 𝐴𝑉𝐵𝑉 ) ∧ ( ( 𝐽 ∈ dom 𝐼 ∧ { 𝐵 , 𝐶 } = ( 𝐼𝐽 ) ) ∧ ( 𝐾 ∈ dom 𝐼 ∧ { 𝐶 , 𝐴 } = ( 𝐼𝐾 ) ) ) ) → ( 𝐴𝐵𝐽𝐾 ) )
24 23 impancom ( ( ( 𝐴𝑉𝐵𝑉 ) ∧ 𝐴𝐵 ) → ( ( ( 𝐽 ∈ dom 𝐼 ∧ { 𝐵 , 𝐶 } = ( 𝐼𝐽 ) ) ∧ ( 𝐾 ∈ dom 𝐼 ∧ { 𝐶 , 𝐴 } = ( 𝐼𝐾 ) ) ) → 𝐽𝐾 ) )
25 24 imp ( ( ( ( 𝐴𝑉𝐵𝑉 ) ∧ 𝐴𝐵 ) ∧ ( ( 𝐽 ∈ dom 𝐼 ∧ { 𝐵 , 𝐶 } = ( 𝐼𝐽 ) ) ∧ ( 𝐾 ∈ dom 𝐼 ∧ { 𝐶 , 𝐴 } = ( 𝐼𝐾 ) ) ) ) → 𝐽𝐾 )