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 ⊢ W ∈ N WSPathsN G → N ∈ ℕ 0 ∧ G ∈ V ∧ W ∈ N WWalksN G ∧ ∃ f f SPaths ⁡ G W

Proof

Step Hyp Ref Expression
1 df-wspthsn ⊢ WSPathsN = n ∈ ℕ 0 , g ∈ V ⟼ w ∈ n WWalksN g | ∃ f f SPaths ⁡ g w
2 1 elmpocl ⊢ W ∈ N WSPathsN G → N ∈ ℕ 0 ∧ G ∈ V
3 simpl ⊢ N ∈ ℕ 0 ∧ G ∈ V ∧ W ∈ N WSPathsN G → N ∈ ℕ 0 ∧ G ∈ V
4 iswspthn ⊢ W ∈ N WSPathsN G ↔ W ∈ N WWalksN G ∧ ∃ f f SPaths ⁡ G W
5 4 a1i ⊢ N ∈ ℕ 0 ∧ G ∈ V → W ∈ N WSPathsN G ↔ W ∈ N WWalksN G ∧ ∃ f f SPaths ⁡ G W
6 5 biimpa ⊢ N ∈ ℕ 0 ∧ G ∈ V ∧ W ∈ N WSPathsN G → W ∈ N WWalksN G ∧ ∃ f f SPaths ⁡ G W
7 3anass ⊢ N ∈ ℕ 0 ∧ G ∈ V ∧ W ∈ N WWalksN G ∧ ∃ f f SPaths ⁡ G W ↔ N ∈ ℕ 0 ∧ G ∈ V ∧ W ∈ N WWalksN G ∧ ∃ f f SPaths ⁡ G W
8 3 6 7 sylanbrc ⊢ N ∈ ℕ 0 ∧ G ∈ V ∧ W ∈ N WSPathsN G → N ∈ ℕ 0 ∧ G ∈ V ∧ W ∈ N WWalksN G ∧ ∃ f f SPaths ⁡ G W
9 2 8 mpancom ⊢ W ∈ N WSPathsN G → N ∈ ℕ 0 ∧ G ∈ V ∧ W ∈ N WWalksN G ∧ ∃ f f SPaths ⁡ G W