Metamath Proof Explorer

Theorem wlkreslem

Description: Lemma for wlkres . (Contributed by AV, 5-Mar-2021) (Revised by AV, 30-Nov-2022)

Ref Expression
Hypotheses wlkres.v ⊢ V = Vtx ⁡ G
wlkres.i ⊢ I = iEdg ⁡ G
wlkres.d ⊢ φ → F Walks ⁡ G P
wlkres.n ⊢ φ → N ∈ 0 ..^ F
wlkres.s ⊢ φ → Vtx ⁡ S = V
Assertion wlkreslem ⊢ φ → S ∈ V

Proof

Step Hyp Ref Expression
1 wlkres.v ⊢ V = Vtx ⁡ G
2 wlkres.i ⊢ I = iEdg ⁡ G
3 wlkres.d ⊢ φ → F Walks ⁡ G P
4 wlkres.n ⊢ φ → N ∈ 0 ..^ F
5 wlkres.s ⊢ φ → Vtx ⁡ S = V
6 ax-1 ⊢ S ∈ V → φ → S ∈ V
7 df-nel ⊢ S ∉ V ↔ ¬ S ∈ V
8 df-br ⊢ F Walks ⁡ G P ↔ F P ∈ Walks ⁡ G
9 ne0i ⊢ F P ∈ Walks ⁡ G → Walks ⁡ G ≠ ∅
10 5 1 eqtrdi ⊢ φ → Vtx ⁡ S = Vtx ⁡ G
11 10 anim1ci ⊢ φ ∧ S ∉ V → S ∉ V ∧ Vtx ⁡ S = Vtx ⁡ G
12 wlk0prc ⊢ S ∉ V ∧ Vtx ⁡ S = Vtx ⁡ G → Walks ⁡ G = ∅
13 eqneqall ⊢ Walks ⁡ G = ∅ → Walks ⁡ G ≠ ∅ → S ∈ V
14 11 12 13 3syl ⊢ φ ∧ S ∉ V → Walks ⁡ G ≠ ∅ → S ∈ V
15 14 expcom ⊢ S ∉ V → φ → Walks ⁡ G ≠ ∅ → S ∈ V
16 15 com13 ⊢ Walks ⁡ G ≠ ∅ → φ → S ∉ V → S ∈ V
17 9 16 syl ⊢ F P ∈ Walks ⁡ G → φ → S ∉ V → S ∈ V
18 8 17 sylbi ⊢ F Walks ⁡ G P → φ → S ∉ V → S ∈ V
19 3 18 mpcom ⊢ φ → S ∉ V → S ∈ V
20 19 com12 ⊢ S ∉ V → φ → S ∈ V
21 7 20 sylbir ⊢ ¬ S ∈ V → φ → S ∈ V
22 6 21 pm2.61i ⊢ φ → S ∈ V