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 𝐼 ∧ { 𝐶 , 𝐴 } = ( 𝐼 ‘ 𝐾 ) ) ) ) → 𝐽 ≠ 𝐾 )