Metamath Proof Explorer

Theorem wlkp1lem1

Description: Lemma for wlkp1 . (Contributed by AV, 6-Mar-2021)

Ref Expression
Hypotheses wlkp1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
wlkp1.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
wlkp1.f ⊢ ( 𝜑 → Fun 𝐼 )
wlkp1.a ⊢ ( 𝜑 → 𝐼 ∈ Fin )
wlkp1.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
wlkp1.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
wlkp1.d ⊢ ( 𝜑 → ¬ 𝐵 ∈ dom 𝐼 )
wlkp1.w ⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
wlkp1.n ⊢ 𝑁 = ( ♯ ‘ 𝐹 )
Assertion wlkp1lem1 ( 𝜑 → ¬ ( 𝑁 + 1 ) ∈ dom 𝑃 )

Proof

Step Hyp Ref Expression
1 wlkp1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 wlkp1.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 wlkp1.f ⊢ ( 𝜑 → Fun 𝐼 )
4 wlkp1.a ⊢ ( 𝜑 → 𝐼 ∈ Fin )
5 wlkp1.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
6 wlkp1.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
7 wlkp1.d ⊢ ( 𝜑 → ¬ 𝐵 ∈ dom 𝐼 )
8 wlkp1.w ⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
9 wlkp1.n ⊢ 𝑁 = ( ♯ ‘ 𝐹 )
10 wlkcl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
11 1 wlkp ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )
12 10 11 jca ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) )
13 fzp1nel ⊢ ¬ ( ( ♯ ‘ 𝐹 ) + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) )
14 13 a1i ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ¬ ( ( ♯ ‘ 𝐹 ) + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
15 9 oveq1i ⊢ ( 𝑁 + 1 ) = ( ( ♯ ‘ 𝐹 ) + 1 )
16 15 eleq1i ⊢ ( ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ↔ ( ( ♯ ‘ 𝐹 ) + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
17 14 16 sylnibr ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ¬ ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
18 eleq2 ⊢ ( dom 𝑃 = ( 0 ... ( ♯ ‘ 𝐹 ) ) → ( ( 𝑁 + 1 ) ∈ dom 𝑃 ↔ ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) )
19 18 notbid ⊢ ( dom 𝑃 = ( 0 ... ( ♯ ‘ 𝐹 ) ) → ( ¬ ( 𝑁 + 1 ) ∈ dom 𝑃 ↔ ¬ ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) )
20 17 19 syl5ibrcom ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( dom 𝑃 = ( 0 ... ( ♯ ‘ 𝐹 ) ) → ¬ ( 𝑁 + 1 ) ∈ dom 𝑃 ) )
21 fdm ⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 → dom 𝑃 = ( 0 ... ( ♯ ‘ 𝐹 ) ) )
22 20 21 impel ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) → ¬ ( 𝑁 + 1 ) ∈ dom 𝑃 )
23 8 12 22 3syl ⊢ ( 𝜑 → ¬ ( 𝑁 + 1 ) ∈ dom 𝑃 )