Metamath Proof Explorer


Theorem wlkp1lem2

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 wlkp1lem2 ( 𝜑 → ( ♯ ‘ 𝐻 ) = ( 𝑁 + 1 ) )

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 fveq2i ( ♯ ‘ 𝐻 ) = ( ♯ ‘ ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) )
15 14 a1i ( 𝜑 → ( ♯ ‘ 𝐻 ) = ( ♯ ‘ ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) ) )
16 opex 𝑁 , 𝐵 ⟩ ∈ V
17 2 wlkf ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃𝐹 ∈ Word dom 𝐼 )
18 wrdfin ( 𝐹 ∈ Word dom 𝐼𝐹 ∈ Fin )
19 8 17 18 3syl ( 𝜑𝐹 ∈ Fin )
20 fzonel ¬ ( ♯ ‘ 𝐹 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) )
21 20 a1i ( 𝜑 → ¬ ( ♯ ‘ 𝐹 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
22 eleq1 ( 𝑁 = ( ♯ ‘ 𝐹 ) → ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↔ ( ♯ ‘ 𝐹 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
23 22 notbid ( 𝑁 = ( ♯ ‘ 𝐹 ) → ( ¬ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↔ ¬ ( ♯ ‘ 𝐹 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
24 21 23 syl5ibr ( 𝑁 = ( ♯ ‘ 𝐹 ) → ( 𝜑 → ¬ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
25 9 24 ax-mp ( 𝜑 → ¬ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
26 wrdfn ( 𝐹 ∈ Word dom 𝐼𝐹 Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
27 8 17 26 3syl ( 𝜑𝐹 Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
28 fnop ( ( 𝐹 Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ⟨ 𝑁 , 𝐵 ⟩ ∈ 𝐹 ) → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
29 28 ex ( 𝐹 Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ⟨ 𝑁 , 𝐵 ⟩ ∈ 𝐹𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
30 27 29 syl ( 𝜑 → ( ⟨ 𝑁 , 𝐵 ⟩ ∈ 𝐹𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
31 25 30 mtod ( 𝜑 → ¬ ⟨ 𝑁 , 𝐵 ⟩ ∈ 𝐹 )
32 19 31 jca ( 𝜑 → ( 𝐹 ∈ Fin ∧ ¬ ⟨ 𝑁 , 𝐵 ⟩ ∈ 𝐹 ) )
33 hashunsng ( ⟨ 𝑁 , 𝐵 ⟩ ∈ V → ( ( 𝐹 ∈ Fin ∧ ¬ ⟨ 𝑁 , 𝐵 ⟩ ∈ 𝐹 ) → ( ♯ ‘ ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) )
34 16 32 33 mpsyl ( 𝜑 → ( ♯ ‘ ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) ) = ( ( ♯ ‘ 𝐹 ) + 1 ) )
35 9 eqcomi ( ♯ ‘ 𝐹 ) = 𝑁
36 35 a1i ( 𝜑 → ( ♯ ‘ 𝐹 ) = 𝑁 )
37 36 oveq1d ( 𝜑 → ( ( ♯ ‘ 𝐹 ) + 1 ) = ( 𝑁 + 1 ) )
38 15 34 37 3eqtrd ( 𝜑 → ( ♯ ‘ 𝐻 ) = ( 𝑁 + 1 ) )