Metamath Proof Explorer

Theorem clwlkclwwlkfolem

Description: Lemma for clwlkclwwlkfo . (Contributed by AV, 25-May-2022)

Ref Expression
Hypothesis clwlkclwwlkf.c ⊢ C = w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w
Assertion clwlkclwwlkfolem ⊢ W ∈ Word Vtx ⁡ G ∧ 1 ≤ W ∧ f W ++ ⟨“ W ⁡ 0 ”⟩ ∈ ClWalks ⁡ G → f W ++ ⟨“ W ⁡ 0 ”⟩ ∈ C

Proof

Step Hyp Ref Expression
1 clwlkclwwlkf.c ⊢ C = w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w
2 simp3 ⊢ W ∈ Word Vtx ⁡ G ∧ 1 ≤ W ∧ f W ++ ⟨“ W ⁡ 0 ”⟩ ∈ ClWalks ⁡ G → f W ++ ⟨“ W ⁡ 0 ”⟩ ∈ ClWalks ⁡ G
3 wrdlenccats1lenm1 ⊢ W ∈ Word Vtx ⁡ G → W ++ ⟨“ W ⁡ 0 ”⟩ − 1 = W
4 3 eqcomd ⊢ W ∈ Word Vtx ⁡ G → W = W ++ ⟨“ W ⁡ 0 ”⟩ − 1
5 4 breq2d ⊢ W ∈ Word Vtx ⁡ G → 1 ≤ W ↔ 1 ≤ W ++ ⟨“ W ⁡ 0 ”⟩ − 1
6 5 biimpa ⊢ W ∈ Word Vtx ⁡ G ∧ 1 ≤ W → 1 ≤ W ++ ⟨“ W ⁡ 0 ”⟩ − 1
7 6 3adant3 ⊢ W ∈ Word Vtx ⁡ G ∧ 1 ≤ W ∧ f W ++ ⟨“ W ⁡ 0 ”⟩ ∈ ClWalks ⁡ G → 1 ≤ W ++ ⟨“ W ⁡ 0 ”⟩ − 1
8 df-br ⊢ f ClWalks ⁡ G W ++ ⟨“ W ⁡ 0 ”⟩ ↔ f W ++ ⟨“ W ⁡ 0 ”⟩ ∈ ClWalks ⁡ G
9 clwlkiswlk ⊢ f ClWalks ⁡ G W ++ ⟨“ W ⁡ 0 ”⟩ → f Walks ⁡ G W ++ ⟨“ W ⁡ 0 ”⟩
10 wlklenvm1 ⊢ f Walks ⁡ G W ++ ⟨“ W ⁡ 0 ”⟩ → f = W ++ ⟨“ W ⁡ 0 ”⟩ − 1
11 9 10 syl ⊢ f ClWalks ⁡ G W ++ ⟨“ W ⁡ 0 ”⟩ → f = W ++ ⟨“ W ⁡ 0 ”⟩ − 1
12 8 11 sylbir ⊢ f W ++ ⟨“ W ⁡ 0 ”⟩ ∈ ClWalks ⁡ G → f = W ++ ⟨“ W ⁡ 0 ”⟩ − 1
13 12 3ad2ant3 ⊢ W ∈ Word Vtx ⁡ G ∧ 1 ≤ W ∧ f W ++ ⟨“ W ⁡ 0 ”⟩ ∈ ClWalks ⁡ G → f = W ++ ⟨“ W ⁡ 0 ”⟩ − 1
14 7 13 breqtrrd ⊢ W ∈ Word Vtx ⁡ G ∧ 1 ≤ W ∧ f W ++ ⟨“ W ⁡ 0 ”⟩ ∈ ClWalks ⁡ G → 1 ≤ f
15 vex ⊢ f ∈ V
16 ovex ⊢ W ++ ⟨“ W ⁡ 0 ”⟩ ∈ V
17 15 16 op1std ⊢ c = f W ++ ⟨“ W ⁡ 0 ”⟩ → 1 st ⁡ c = f
18 17 fveq2d ⊢ c = f W ++ ⟨“ W ⁡ 0 ”⟩ → 1 st ⁡ c = f
19 18 breq2d ⊢ c = f W ++ ⟨“ W ⁡ 0 ”⟩ → 1 ≤ 1 st ⁡ c ↔ 1 ≤ f
20 2fveq3 ⊢ w = c → 1 st ⁡ w = 1 st ⁡ c
21 20 breq2d ⊢ w = c → 1 ≤ 1 st ⁡ w ↔ 1 ≤ 1 st ⁡ c
22 21 cbvrabv ⊢ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w = c ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ c
23 1 22 eqtri ⊢ C = c ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ c
24 19 23 elrab2 ⊢ f W ++ ⟨“ W ⁡ 0 ”⟩ ∈ C ↔ f W ++ ⟨“ W ⁡ 0 ”⟩ ∈ ClWalks ⁡ G ∧ 1 ≤ f
25 2 14 24 sylanbrc ⊢ W ∈ Word Vtx ⁡ G ∧ 1 ≤ W ∧ f W ++ ⟨“ W ⁡ 0 ”⟩ ∈ ClWalks ⁡ G → f W ++ ⟨“ W ⁡ 0 ”⟩ ∈ C