Theorem wspthnp

Description: Properties of a set being a simple path of a fixed length as word. (Contributed by AV, 18-May-2021)

	Ref	Expression
Assertion	wspthnp	⊢ ( 𝑊 ∈ ( 𝑁 WSPathsN 𝐺 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 ) )

Proof

Step	Hyp	Ref	Expression
1		df-wspthsn	⊢ WSPathsN = ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝑔 ) ∣ ∃ 𝑓 𝑓 ( SPaths ‘ 𝑔 ) 𝑤 } )
2	1	elmpocl	⊢ ( 𝑊 ∈ ( 𝑁 WSPathsN 𝐺 ) → ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) )
3		simpl	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ 𝑊 ∈ ( 𝑁 WSPathsN 𝐺 ) ) → ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) )
4		iswspthn	⊢ ( 𝑊 ∈ ( 𝑁 WSPathsN 𝐺 ) ↔ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 ) )
5	4	a1i	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( 𝑊 ∈ ( 𝑁 WSPathsN 𝐺 ) ↔ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 ) ) )
6	5	biimpa	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ 𝑊 ∈ ( 𝑁 WSPathsN 𝐺 ) ) → ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 ) )
7		3anass	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 ) ↔ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 ) ) )
8	3 6 7	sylanbrc	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ 𝑊 ∈ ( 𝑁 WSPathsN 𝐺 ) ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 ) )
9	2 8	mpancom	⊢ ( 𝑊 ∈ ( 𝑁 WSPathsN 𝐺 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 ) )