Metamath Proof Explorer

Theorem 0clwlkv

Description: Any vertex (more precisely, a pair of an empty set (of edges) and a singleton function to this vertex) determines a closed walk of length 0. (Contributed by AV, 11-Feb-2022)

Ref Expression
Hypothesis 0clwlk.v ⊢ V = Vtx ⁡ G
Assertion 0clwlkv ⊢ X ∈ V ∧ F = ∅ ∧ P : 0 ⟶ X → F ClWalks ⁡ G P

Proof

Step Hyp Ref Expression
1 0clwlk.v ⊢ V = Vtx ⁡ G
2 fz0sn ⊢ 0 … 0 = 0
3 2 eqcomi ⊢ 0 = 0 … 0
4 3 feq2i ⊢ P : 0 ⟶ X ↔ P : 0 … 0 ⟶ X
5 4 biimpi ⊢ P : 0 ⟶ X → P : 0 … 0 ⟶ X
6 5 3ad2ant3 ⊢ X ∈ V ∧ F = ∅ ∧ P : 0 ⟶ X → P : 0 … 0 ⟶ X
7 snssi ⊢ X ∈ V → X ⊆ V
8 7 3ad2ant1 ⊢ X ∈ V ∧ F = ∅ ∧ P : 0 ⟶ X → X ⊆ V
9 6 8 fssd ⊢ X ∈ V ∧ F = ∅ ∧ P : 0 ⟶ X → P : 0 … 0 ⟶ V
10 breq1 ⊢ F = ∅ → F ClWalks ⁡ G P ↔ ∅ ClWalks ⁡ G P
11 10 3ad2ant2 ⊢ X ∈ V ∧ F = ∅ ∧ P : 0 ⟶ X → F ClWalks ⁡ G P ↔ ∅ ClWalks ⁡ G P
12 1 1vgrex ⊢ X ∈ V → G ∈ V
13 1 0clwlk ⊢ G ∈ V → ∅ ClWalks ⁡ G P ↔ P : 0 … 0 ⟶ V
14 12 13 syl ⊢ X ∈ V → ∅ ClWalks ⁡ G P ↔ P : 0 … 0 ⟶ V
15 14 3ad2ant1 ⊢ X ∈ V ∧ F = ∅ ∧ P : 0 ⟶ X → ∅ ClWalks ⁡ G P ↔ P : 0 … 0 ⟶ V
16 11 15 bitrd ⊢ X ∈ V ∧ F = ∅ ∧ P : 0 ⟶ X → F ClWalks ⁡ G P ↔ P : 0 … 0 ⟶ V
17 9 16 mpbird ⊢ X ∈ V ∧ F = ∅ ∧ P : 0 ⟶ X → F ClWalks ⁡ G P