Metamath Proof Explorer

Theorem clwlknf1oclwwlknlem3

Description: Lemma 3 for clwlknf1oclwwlkn : The bijective function of clwlknf1oclwwlkn is the bijective function of clwlkclwwlkf1o restricted to the closed walks with a fixed positive length. (Contributed by AV, 26-May-2022) (Revised by AV, 1-Nov-2022)

Ref Expression
Hypotheses clwlknf1oclwwlkn.a ⊢ A = 1 st ⁡ c
clwlknf1oclwwlkn.b ⊢ B = 2 nd ⁡ c
clwlknf1oclwwlkn.c ⊢ C = w ∈ ClWalks ⁡ G | 1 st ⁡ w = N
clwlknf1oclwwlkn.f ⊢ F = c ∈ C ⟼ B prefix A
Assertion clwlknf1oclwwlknlem3 ⊢ G ∈ USHGraph ∧ N ∈ ℕ → F = c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w ⟼ B prefix A ↾ C

Proof

Step Hyp Ref Expression
1 clwlknf1oclwwlkn.a ⊢ A = 1 st ⁡ c
2 clwlknf1oclwwlkn.b ⊢ B = 2 nd ⁡ c
3 clwlknf1oclwwlkn.c ⊢ C = w ∈ ClWalks ⁡ G | 1 st ⁡ w = N
4 clwlknf1oclwwlkn.f ⊢ F = c ∈ C ⟼ B prefix A
5 nnge1 ⊢ N ∈ ℕ → 1 ≤ N
6 breq2 ⊢ 1 st ⁡ w = N → 1 ≤ 1 st ⁡ w ↔ 1 ≤ N
7 5 6 syl5ibrcom ⊢ N ∈ ℕ → 1 st ⁡ w = N → 1 ≤ 1 st ⁡ w
8 7 ad2antlr ⊢ G ∈ USHGraph ∧ N ∈ ℕ ∧ w ∈ ClWalks ⁡ G → 1 st ⁡ w = N → 1 ≤ 1 st ⁡ w
9 8 ss2rabdv ⊢ G ∈ USHGraph ∧ N ∈ ℕ → w ∈ ClWalks ⁡ G | 1 st ⁡ w = N ⊆ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w
10 3 9 eqsstrid ⊢ G ∈ USHGraph ∧ N ∈ ℕ → C ⊆ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w
11 10 resmptd ⊢ G ∈ USHGraph ∧ N ∈ ℕ → c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w ⟼ B prefix A ↾ C = c ∈ C ⟼ B prefix A
12 4 11 eqtr4id ⊢ G ∈ USHGraph ∧ N ∈ ℕ → F = c ∈ w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w ⟼ B prefix A ↾ C