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

Metamath Proof Explorer

Theorem wlkp1lem3

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 ⊢ 𝐻 = ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } )
Assertion wlkp1lem3 ( 𝜑 → ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑁 ) ) = ( ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) ‘ 𝐵 ) )

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 13 a1i ⊢ ( 𝜑 → 𝐻 = ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) )
15 14 fveq1d ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑁 ) = ( ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) ‘ 𝑁 ) )
16 9 fvexi ⊢ 𝑁 ∈ V
17 2 wlkf ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ Word dom 𝐼 )
18 lencl ⊢ ( 𝐹 ∈ Word dom 𝐼 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
19 wrddm ⊢ ( 𝐹 ∈ Word dom 𝐼 → dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
20 fzonel ⊢ ¬ ( ♯ ‘ 𝐹 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) )
21 9 a1i ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑁 = ( ♯ ‘ 𝐹 ) )
22 simpr ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
23 21 22 eleq12d ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑁 ∈ dom 𝐹 ↔ ( ♯ ‘ 𝐹 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
24 20 23 mtbiri ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ¬ 𝑁 ∈ dom 𝐹 )
25 18 19 24 syl2anc ⊢ ( 𝐹 ∈ Word dom 𝐼 → ¬ 𝑁 ∈ dom 𝐹 )
26 8 17 25 3syl ⊢ ( 𝜑 → ¬ 𝑁 ∈ dom 𝐹 )
27 fsnunfv ⊢ ( ( 𝑁 ∈ V ∧ 𝐵 ∈ 𝑊 ∧ ¬ 𝑁 ∈ dom 𝐹 ) → ( ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) ‘ 𝑁 ) = 𝐵 )
28 16 5 26 27 mp3an2i ⊢ ( 𝜑 → ( ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) ‘ 𝑁 ) = 𝐵 )
29 15 28 eqtrd ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑁 ) = 𝐵 )
30 12 29 fveq12d ⊢ ( 𝜑 → ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑁 ) ) = ( ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) ‘ 𝐵 ) )