Metamath Proof Explorer

Theorem wksv

Description: The class of walks is a set. (Contributed by AV, 15-Jan-2021)

Ref Expression
Assertion wksv ⊢ f p | f Walks ⁡ G p ∈ V

Proof

Step Hyp Ref Expression
1 fvex ⊢ Vtx ⁡ G ∈ V
2 fvex ⊢ iEdg ⁡ G ∈ V
3 2 dmex ⊢ dom ⁡ iEdg ⁡ G ∈ V
4 wrdexg ⊢ dom ⁡ iEdg ⁡ G ∈ V → Word dom ⁡ iEdg ⁡ G ∈ V
5 3 4 mp1i ⊢ Vtx ⁡ G ∈ V → Word dom ⁡ iEdg ⁡ G ∈ V
6 wrdexg ⊢ Vtx ⁡ G ∈ V → Word Vtx ⁡ G ∈ V
7 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
8 7 wlkf ⊢ f Walks ⁡ G p → f ∈ Word dom ⁡ iEdg ⁡ G
9 8 adantl ⊢ Vtx ⁡ G ∈ V ∧ f Walks ⁡ G p → f ∈ Word dom ⁡ iEdg ⁡ G
10 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
11 10 wlkpwrd ⊢ f Walks ⁡ G p → p ∈ Word Vtx ⁡ G
12 11 adantl ⊢ Vtx ⁡ G ∈ V ∧ f Walks ⁡ G p → p ∈ Word Vtx ⁡ G
13 5 6 9 12 opabex2 ⊢ Vtx ⁡ G ∈ V → f p | f Walks ⁡ G p ∈ V
14 1 13 ax-mp ⊢ f p | f Walks ⁡ G p ∈ V