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

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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
wlkres.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
wlkres.d ⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
wlkres.n ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
wlkres.s ⊢ ( 𝜑 → ( Vtx ‘ 𝑆 ) = 𝑉 )
Assertion wlkreslem ( 𝜑 → 𝑆 ∈ V )

Proof

Step Hyp Ref Expression
1 wlkres.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 wlkres.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 wlkres.d ⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
4 wlkres.n ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
5 wlkres.s ⊢ ( 𝜑 → ( Vtx ‘ 𝑆 ) = 𝑉 )
6 ax-1 ⊢ ( 𝑆 ∈ V → ( 𝜑 → 𝑆 ∈ V ) )
7 df-nel ⊢ ( 𝑆 ∉ V ↔ ¬ 𝑆 ∈ V )
8 df-br ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ ⟨ 𝐹 , 𝑃 ⟩ ∈ ( Walks ‘ 𝐺 ) )
9 ne0i ⊢ ( ⟨ 𝐹 , 𝑃 ⟩ ∈ ( Walks ‘ 𝐺 ) → ( Walks ‘ 𝐺 ) ≠ ∅ )
10 5 1 eqtrdi ⊢ ( 𝜑 → ( Vtx ‘ 𝑆 ) = ( Vtx ‘ 𝐺 ) )
11 10 anim1ci ⊢ ( ( 𝜑 ∧ 𝑆 ∉ V ) → ( 𝑆 ∉ V ∧ ( Vtx ‘ 𝑆 ) = ( Vtx ‘ 𝐺 ) ) )
12 wlk0prc ⊢ ( ( 𝑆 ∉ V ∧ ( Vtx ‘ 𝑆 ) = ( Vtx ‘ 𝐺 ) ) → ( Walks ‘ 𝐺 ) = ∅ )
13 eqneqall ⊢ ( ( Walks ‘ 𝐺 ) = ∅ → ( ( Walks ‘ 𝐺 ) ≠ ∅ → 𝑆 ∈ V ) )
14 11 12 13 3syl ⊢ ( ( 𝜑 ∧ 𝑆 ∉ V ) → ( ( Walks ‘ 𝐺 ) ≠ ∅ → 𝑆 ∈ V ) )
15 14 expcom ⊢ ( 𝑆 ∉ V → ( 𝜑 → ( ( Walks ‘ 𝐺 ) ≠ ∅ → 𝑆 ∈ V ) ) )
16 15 com13 ⊢ ( ( Walks ‘ 𝐺 ) ≠ ∅ → ( 𝜑 → ( 𝑆 ∉ V → 𝑆 ∈ V ) ) )
17 9 16 syl ⊢ ( ⟨ 𝐹 , 𝑃 ⟩ ∈ ( Walks ‘ 𝐺 ) → ( 𝜑 → ( 𝑆 ∉ V → 𝑆 ∈ V ) ) )
18 8 17 sylbi ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝜑 → ( 𝑆 ∉ V → 𝑆 ∈ V ) ) )
19 3 18 mpcom ⊢ ( 𝜑 → ( 𝑆 ∉ V → 𝑆 ∈ V ) )
20 19 com12 ⊢ ( 𝑆 ∉ V → ( 𝜑 → 𝑆 ∈ V ) )
21 7 20 sylbir ⊢ ( ¬ 𝑆 ∈ V → ( 𝜑 → 𝑆 ∈ V ) )
22 6 21 pm2.61i ⊢ ( 𝜑 → 𝑆 ∈ V )