Metamath Proof Explorer

Theorem wlkp1lem5

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 ⊢ 𝑁 = ( ♯ ‘ 𝐹 )
wlkp1.e ⊢ ( 𝜑 → 𝐸 ∈ ( Edg ‘ 𝐺 ) )
wlkp1.x ⊢ ( 𝜑 → { ( 𝑃 ‘ 𝑁 ) , 𝐶 } ⊆ 𝐸 )
wlkp1.u ⊢ ( 𝜑 → ( iEdg ‘ 𝑆 ) = ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) )
wlkp1.h ⊢ 𝐻 = ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } )
wlkp1.q ⊢ 𝑄 = ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } )
wlkp1.s ⊢ ( 𝜑 → ( Vtx ‘ 𝑆 ) = 𝑉 )
Assertion wlkp1lem5 ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑄 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑘 ) )

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 wlkp1.e ⊢ ( 𝜑 → 𝐸 ∈ ( Edg ‘ 𝐺 ) )
11 wlkp1.x ⊢ ( 𝜑 → { ( 𝑃 ‘ 𝑁 ) , 𝐶 } ⊆ 𝐸 )
12 wlkp1.u ⊢ ( 𝜑 → ( iEdg ‘ 𝑆 ) = ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) )
13 wlkp1.h ⊢ 𝐻 = ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } )
14 wlkp1.q ⊢ 𝑄 = ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } )
15 wlkp1.s ⊢ ( 𝜑 → ( Vtx ‘ 𝑆 ) = 𝑉 )
16 14 fveq1i ⊢ ( 𝑄 ‘ 𝑘 ) = ( ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) ‘ 𝑘 )
17 fzp1nel ⊢ ¬ ( 𝑁 + 1 ) ∈ ( 0 ... 𝑁 )
18 eleq1 ⊢ ( 𝑘 = ( 𝑁 + 1 ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↔ ( 𝑁 + 1 ) ∈ ( 0 ... 𝑁 ) ) )
19 18 notbid ⊢ ( 𝑘 = ( 𝑁 + 1 ) → ( ¬ 𝑘 ∈ ( 0 ... 𝑁 ) ↔ ¬ ( 𝑁 + 1 ) ∈ ( 0 ... 𝑁 ) ) )
20 19 eqcoms ⊢ ( ( 𝑁 + 1 ) = 𝑘 → ( ¬ 𝑘 ∈ ( 0 ... 𝑁 ) ↔ ¬ ( 𝑁 + 1 ) ∈ ( 0 ... 𝑁 ) ) )
21 17 20 mpbiri ⊢ ( ( 𝑁 + 1 ) = 𝑘 → ¬ 𝑘 ∈ ( 0 ... 𝑁 ) )
22 21 a1i ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) = 𝑘 → ¬ 𝑘 ∈ ( 0 ... 𝑁 ) ) )
23 22 con2d ⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ... 𝑁 ) → ¬ ( 𝑁 + 1 ) = 𝑘 ) )
24 23 imp ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ¬ ( 𝑁 + 1 ) = 𝑘 )
25 24 neqned ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 + 1 ) ≠ 𝑘 )
26 fvunsn ⊢ ( ( 𝑁 + 1 ) ≠ 𝑘 → ( ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) ‘ 𝑘 ) = ( 𝑃 ‘ 𝑘 ) )
27 25 26 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) ‘ 𝑘 ) = ( 𝑃 ‘ 𝑘 ) )
28 16 27 syl5eq ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑄 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑘 ) )
29 28 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑄 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑘 ) )