Metamath Proof Explorer

Theorem 2cycld

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

Ref Expression
Hypotheses 2cycld.1 ⊢ P = ⟨“ ABC ”⟩
2cycld.2 ⊢ F = ⟨“ JK ”⟩
2cycld.3 ⊢ φ → A ∈ V ∧ B ∈ V ∧ C ∈ V
2cycld.4 ⊢ φ → A ≠ B ∧ B ≠ C
2cycld.5 ⊢ φ → A B ⊆ I ⁡ J ∧ B C ⊆ I ⁡ K
2cycld.6 ⊢ V = Vtx ⁡ G
2cycld.7 ⊢ I = iEdg ⁡ G
2cycld.8 ⊢ φ → J ≠ K
2cycld.9 ⊢ φ → A = C
Assertion 2cycld ⊢ φ → F Cycles ⁡ G P

Proof

Step Hyp Ref Expression
1 2cycld.1 ⊢ P = ⟨“ ABC ”⟩
2 2cycld.2 ⊢ F = ⟨“ JK ”⟩
3 2cycld.3 ⊢ φ → A ∈ V ∧ B ∈ V ∧ C ∈ V
4 2cycld.4 ⊢ φ → A ≠ B ∧ B ≠ C
5 2cycld.5 ⊢ φ → A B ⊆ I ⁡ J ∧ B C ⊆ I ⁡ K
6 2cycld.6 ⊢ V = Vtx ⁡ G
7 2cycld.7 ⊢ I = iEdg ⁡ G
8 2cycld.8 ⊢ φ → J ≠ K
9 2cycld.9 ⊢ φ → A = C
10 1 2 3 4 5 6 7 8 2pthd ⊢ φ → F Paths ⁡ G P
11 1 fveq1i ⊢ P ⁡ 0 = ⟨“ ABC ”⟩ ⁡ 0
12 s3fv0 ⊢ A ∈ V → ⟨“ ABC ”⟩ ⁡ 0 = A
13 11 12 eqtrid ⊢ A ∈ V → P ⁡ 0 = A
14 13 3ad2ant1 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → P ⁡ 0 = A
15 14 adantr ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A = C → P ⁡ 0 = A
16 simpr ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A = C → A = C
17 2 fveq2i ⊢ F = ⟨“ JK ”⟩
18 s2len ⊢ ⟨“ JK ”⟩ = 2
19 17 18 eqtri ⊢ F = 2
20 1 19 fveq12i ⊢ P ⁡ F = ⟨“ ABC ”⟩ ⁡ 2
21 s3fv2 ⊢ C ∈ V → ⟨“ ABC ”⟩ ⁡ 2 = C
22 20 21 eqtr2id ⊢ C ∈ V → C = P ⁡ F
23 22 3ad2ant3 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → C = P ⁡ F
24 23 adantr ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A = C → C = P ⁡ F
25 15 16 24 3eqtrd ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A = C → P ⁡ 0 = P ⁡ F
26 3 9 25 syl2anc ⊢ φ → P ⁡ 0 = P ⁡ F
27 iscycl ⊢ F Cycles ⁡ G P ↔ F Paths ⁡ G P ∧ P ⁡ 0 = P ⁡ F
28 10 26 27 sylanbrc ⊢ φ → F Cycles ⁡ G P