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	⊢ ( 𝑁 ∈ ℕ → { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 } = { 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ) } )

Proof

Step	Hyp	Ref	Expression
1		2fveq3	⊢ ( 𝑤 = 𝑐 → ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) )
2	1	eqeq1d	⊢ ( 𝑤 = 𝑐 → ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 ↔ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ) )
3	2	cbvrabv	⊢ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 } = { 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 }
4		nnge1	⊢ ( 𝑁 ∈ ℕ → 1 ≤ 𝑁 )
5		breq2	⊢ ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 → ( 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ↔ 1 ≤ 𝑁 ) )
6	4 5	syl5ibrcom	⊢ ( 𝑁 ∈ ℕ → ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 → 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) )
7	6	pm4.71rd	⊢ ( 𝑁 ∈ ℕ → ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ↔ ( 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ) ) )
8	7	rabbidv	⊢ ( 𝑁 ∈ ℕ → { 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 } = { 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ) } )
9	3 8	syl5eq	⊢ ( 𝑁 ∈ ℕ → { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 𝑁 } = { 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ) } )