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	$⊢ P = ⟨“ A B A ”⟩$
	2cycl2d.2	$⊢ F = ⟨“ J K ”⟩$
	2cycl2d.3	$⊢ φ \to (A \in V \land B \in V)$
	2cycl2d.4	$⊢ φ \to A \neq B$
	2cycl2d.5	$⊢ φ \to (\{A, B\} \subseteq I (J) \land \{A, B\} \subseteq I (K))$
	2cycl2d.6	$⊢ V = Vtx (G)$
	2cycl2d.7	$⊢ I = iEdg (G)$
	2cycl2d.8	$⊢ φ \to J \neq K$
Assertion	2cycl2d	$⊢ φ \to F Cycles (G) P$

Step	Hyp	Ref	Expression
1		2cycl2d.1	$⊢ P = ⟨“ A B A ”⟩$
2		2cycl2d.2	$⊢ F = ⟨“ J K ”⟩$
3		2cycl2d.3	$⊢ φ \to (A \in V \land B \in V)$
4		2cycl2d.4	$⊢ φ \to A \neq B$
5		2cycl2d.5	$⊢ φ \to (\{A, B\} \subseteq I (J) \land \{A, B\} \subseteq I (K))$
6		2cycl2d.6	$⊢ V = Vtx (G)$
7		2cycl2d.7	$⊢ I = iEdg (G)$
8		2cycl2d.8	$⊢ φ \to J \neq K$
9		simpl	$⊢ (A \in V \land B \in V) \to A \in V$
10	3 9	jccir	$⊢ φ \to ((A \in V \land B \in V) \land A \in V)$
11		df-3an	$⊢ (A \in V \land B \in V \land A \in V) \leftrightarrow ((A \in V \land B \in V) \land A \in V)$
12	10 11	sylibr	$⊢ φ \to (A \in V \land B \in V \land A \in V)$
13	4	necomd	$⊢ φ \to B \neq A$
14	4 13	jca	$⊢ φ \to (A \neq B \land B \neq A)$
15		prcom	$⊢ \{A, B\} = \{B, A\}$
16	15	sseq1i	$⊢ \{A, B\} \subseteq I (K) \leftrightarrow \{B, A\} \subseteq I (K)$
17	16	anbi2i	$⊢ (\{A, B\} \subseteq I (J) \land \{A, B\} \subseteq I (K)) \leftrightarrow (\{A, B\} \subseteq I (J) \land \{B, A\} \subseteq I (K))$
18	5 17	sylib	$⊢ φ \to (\{A, B\} \subseteq I (J) \land \{B, A\} \subseteq I (K))$
19		eqidd	$⊢ φ \to A = A$
20	1 2 12 14 18 6 7 8 19	2cycld	$⊢ φ \to F Cycles (G) P$

Metamath Proof Explorer