This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clwlknf1oclwwlknlem2

Description: Lemma 2 for clwlknf1oclwwlkn : The closed walks of a positive length are nonempty closed walks of this length. (Contributed by AV, 26-May-2022)

		Ref	Expression
	Assertion	clwlknf1oclwwlknlem2	$⊢ N \in ℕ \to \{w \in ClWalks (G) \| \|1^{st} (w)\| = N\} = \{c \in ClWalks (G) \| (1 \leq \|1^{st} (c)\| \land \|1^{st} (c)\| = N)\}$

Proof

Step	Hyp	Ref	Expression
1		2fveq3	$⊢ w = c \to \|1^{st} (w)\| = \|1^{st} (c)\|$
2	1	eqeq1d	$⊢ w = c \to (\|1^{st} (w)\| = N \leftrightarrow \|1^{st} (c)\| = N)$
3	2	cbvrabv	$⊢ \{w \in ClWalks (G) \| \|1^{st} (w)\| = N\} = \{c \in ClWalks (G) \| \|1^{st} (c)\| = N\}$
4		nnge1	$⊢ N \in ℕ \to 1 \leq N$
5		breq2	$⊢ \|1^{st} (c)\| = N \to (1 \leq \|1^{st} (c)\| \leftrightarrow 1 \leq N)$
6	4 5	syl5ibrcom	$⊢ N \in ℕ \to (\|1^{st} (c)\| = N \to 1 \leq \|1^{st} (c)\|)$
7	6	pm4.71rd	$⊢ N \in ℕ \to (\|1^{st} (c)\| = N \leftrightarrow (1 \leq \|1^{st} (c)\| \land \|1^{st} (c)\| = N))$
8	7	rabbidv	$⊢ N \in ℕ \to \{c \in ClWalks (G) \| \|1^{st} (c)\| = N\} = \{c \in ClWalks (G) \| (1 \leq \|1^{st} (c)\| \land \|1^{st} (c)\| = N)\}$
9	3 8	eqtrid	$⊢ N \in ℕ \to \{w \in ClWalks (G) \| \|1^{st} (w)\| = N\} = \{c \in ClWalks (G) \| (1 \leq \|1^{st} (c)\| \land \|1^{st} (c)\| = N)\}$