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 \in ClWalks (G) \| \|1^{st} (w)\| = N\}$
	clwlknf1oclwwlkn.f	$⊢ F = (c \in C ⟼ B prefix \|A\|)$
Assertion	clwlknf1oclwwlknlem3	$⊢ (G \in USHGraph \land N \in ℕ) \to F = {(c \in \{w \in ClWalks (G) \| 1 \leq \|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 \in ClWalks (G) \| \|1^{st} (w)\| = N\}$
4		clwlknf1oclwwlkn.f	$⊢ F = (c \in C ⟼ B prefix \|A\|)$
5		nnge1	$⊢ N \in ℕ \to 1 \leq N$
6		breq2	$⊢ \|1^{st} (w)\| = N \to (1 \leq \|1^{st} (w)\| \leftrightarrow 1 \leq N)$
7	5 6	syl5ibrcom	$⊢ N \in ℕ \to (\|1^{st} (w)\| = N \to 1 \leq \|1^{st} (w)\|)$
8	7	ad2antlr	$⊢ ((G \in USHGraph \land N \in ℕ) \land w \in ClWalks (G)) \to (\|1^{st} (w)\| = N \to 1 \leq \|1^{st} (w)\|)$
9	8	ss2rabdv	$⊢ (G \in USHGraph \land N \in ℕ) \to \{w \in ClWalks (G) \| \|1^{st} (w)\| = N\} \subseteq \{w \in ClWalks (G) \| 1 \leq \|1^{st} (w)\|\}$
10	3 9	eqsstrid	$⊢ (G \in USHGraph \land N \in ℕ) \to C \subseteq \{w \in ClWalks (G) \| 1 \leq \|1^{st} (w)\|\}$
11	10	resmptd	$⊢ (G \in USHGraph \land N \in ℕ) \to {(c \in \{w \in ClWalks (G) \| 1 \leq \|1^{st} (w)\|\} ⟼ B prefix \|A\|) ↾}_{C} = (c \in C ⟼ B prefix \|A\|)$
12	4 11	eqtr4id	$⊢ (G \in USHGraph \land N \in ℕ) \to F = {(c \in \{w \in ClWalks (G) \| 1 \leq \|1^{st} (w)\|\} ⟼ B prefix \|A\|) ↾}_{C}$

Metamath Proof Explorer

Theorem clwlknf1oclwwlknlem3

Proof