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

Metamath Proof Explorer

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 ‘ 𝐺 ) 𝑊 ) )