Metamath Proof Explorer

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 ⊢ P = ⟨“ ABA ”⟩
2cycl2d.2 ⊢ F = ⟨“ JK ”⟩
2cycl2d.3 ⊢ φ → A ∈ V ∧ B ∈ V
2cycl2d.4 ⊢ φ → A ≠ B
2cycl2d.5 ⊢ φ → A B ⊆ I ⁡ J ∧ A B ⊆ I ⁡ K
2cycl2d.6 ⊢ V = Vtx ⁡ G
2cycl2d.7 ⊢ I = iEdg ⁡ G
2cycl2d.8 ⊢ φ → J ≠ K
Assertion 2cycl2d ⊢ φ → F Cycles ⁡ G P

Proof

Step Hyp Ref Expression
1 2cycl2d.1 ⊢ P = ⟨“ ABA ”⟩
2 2cycl2d.2 ⊢ F = ⟨“ JK ”⟩
3 2cycl2d.3 ⊢ φ → A ∈ V ∧ B ∈ V
4 2cycl2d.4 ⊢ φ → A ≠ B
5 2cycl2d.5 ⊢ φ → A B ⊆ I ⁡ J ∧ A B ⊆ I ⁡ K
6 2cycl2d.6 ⊢ V = Vtx ⁡ G
7 2cycl2d.7 ⊢ I = iEdg ⁡ G
8 2cycl2d.8 ⊢ φ → J ≠ K
9 simpl ⊢ A ∈ V ∧ B ∈ V → A ∈ V
10 3 9 jccir ⊢ φ → A ∈ V ∧ B ∈ V ∧ A ∈ V
11 df-3an ⊢ A ∈ V ∧ B ∈ V ∧ A ∈ V ↔ A ∈ V ∧ B ∈ V ∧ A ∈ V
12 10 11 sylibr ⊢ φ → A ∈ V ∧ B ∈ V ∧ A ∈ V
13 4 necomd ⊢ φ → B ≠ A
14 4 13 jca ⊢ φ → A ≠ B ∧ B ≠ A
15 prcom ⊢ A B = B A
16 15 sseq1i ⊢ A B ⊆ I ⁡ K ↔ B A ⊆ I ⁡ K
17 16 anbi2i ⊢ A B ⊆ I ⁡ J ∧ A B ⊆ I ⁡ K ↔ A B ⊆ I ⁡ J ∧ B A ⊆ I ⁡ K
18 5 17 sylib ⊢ φ → A B ⊆ I ⁡ J ∧ B A ⊆ I ⁡ K
19 eqidd ⊢ φ → A = A
20 1 2 12 14 18 6 7 8 19 2cycld ⊢ φ → F Cycles ⁡ G P