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 ⊢ 𝑉 = ( 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 biimtrdi ⊢ ( { 𝐶 , 𝐴 } = ( 𝐼 ‘ 𝐾 ) → ( { 𝐵 , 𝐶 } = ( 𝐼 ‘ 𝐾 ) → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 = 𝐵 ) ) )
17 16 adantl ⊢ ( ( 𝐾 ∈ dom 𝐼 ∧ { 𝐶 , 𝐴 } = ( 𝐼 ‘ 𝐾 ) ) → ( { 𝐵 , 𝐶 } = ( 𝐼 ‘ 𝐾 ) → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 = 𝐵 ) ) )
18 17 com12 ⊢ ( { 𝐵 , 𝐶 } = ( 𝐼 ‘ 𝐾 ) → ( ( 𝐾 ∈ dom 𝐼 ∧ { 𝐶 , 𝐴 } = ( 𝐼 ‘ 𝐾 ) ) → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 = 𝐵 ) ) )
19 5 18 biimtrdi ⊢ ( 𝐽 = 𝐾 → ( { 𝐵 , 𝐶 } = ( 𝐼 ‘ 𝐽 ) → ( ( 𝐾 ∈ 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 𝐼 ∧ { 𝐶 , 𝐴 } = ( 𝐼 ‘ 𝐾 ) ) ) ) → 𝐽 ≠ 𝐾 )