Theorem 2cycl2d

Description: Construction of a 2-cycle from two given edges in a graph. (Contributed by BTernaryTau, 16-Oct-2023)

	Ref	Expression
Hypotheses	2cycl2d.1	⊢ 𝑃 = ⟨“ 𝐴 𝐵 𝐴 ”⟩
	2cycl2d.2	⊢ 𝐹 = ⟨“ 𝐽 𝐾 ”⟩
	2cycl2d.3	⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) )
	2cycl2d.4	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
	2cycl2d.5	⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) ∧ { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐾 ) ) )
	2cycl2d.6	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	2cycl2d.7	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	2cycl2d.8	⊢ ( 𝜑 → 𝐽 ≠ 𝐾 )
Assertion	2cycl2d	⊢ ( 𝜑 → 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		2cycl2d.1	⊢ 𝑃 = ⟨“ 𝐴 𝐵 𝐴 ”⟩
2		2cycl2d.2	⊢ 𝐹 = ⟨“ 𝐽 𝐾 ”⟩
3		2cycl2d.3	⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) )
4		2cycl2d.4	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
5		2cycl2d.5	⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) ∧ { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐾 ) ) )
6		2cycl2d.6	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
7		2cycl2d.7	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
8		2cycl2d.8	⊢ ( 𝜑 → 𝐽 ≠ 𝐾 )
9		simpl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 )
10	3 9	jccir	⊢ ( 𝜑 → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ∈ 𝑉 ) )
11		df-3an	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ↔ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ∈ 𝑉 ) )
12	10 11	sylibr	⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) )
13	4	necomd	⊢ ( 𝜑 → 𝐵 ≠ 𝐴 )
14	4 13	jca	⊢ ( 𝜑 → ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐴 ) )
15		prcom	⊢ { 𝐴 , 𝐵 } = { 𝐵 , 𝐴 }
16	15	sseq1i	⊢ ( { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐾 ) ↔ { 𝐵 , 𝐴 } ⊆ ( 𝐼 ‘ 𝐾 ) )
17	16	anbi2i	⊢ ( ( { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) ∧ { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐾 ) ) ↔ ( { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) ∧ { 𝐵 , 𝐴 } ⊆ ( 𝐼 ‘ 𝐾 ) ) )
18	5 17	sylib	⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) ∧ { 𝐵 , 𝐴 } ⊆ ( 𝐼 ‘ 𝐾 ) ) )
19		eqidd	⊢ ( 𝜑 → 𝐴 = 𝐴 )
20	1 2 12 14 18 6 7 8 19	2cycld	⊢ ( 𝜑 → 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 )