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

Metamath Proof Explorer

Theorem wlkp1lem7

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 wlkp1lem7 ( 𝜑 → { ( 𝑄 ‘ 𝑁 ) , ( 𝑄 ‘ ( 𝑁 + 1 ) ) } ⊆ ( ( 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 wlkp1.q ⊢ 𝑄 = ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } )
15 wlkp1.s ⊢ ( 𝜑 → ( Vtx ‘ 𝑆 ) = 𝑉 )
16 fveq2 ⊢ ( 𝑘 = 𝑁 → ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ 𝑁 ) )
17 fveq2 ⊢ ( 𝑘 = 𝑁 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑁 ) )
18 16 17 eqeq12d ⊢ ( 𝑘 = 𝑁 → ( ( 𝑄 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑘 ) ↔ ( 𝑄 ‘ 𝑁 ) = ( 𝑃 ‘ 𝑁 ) ) )
19 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 wlkp1lem5 ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑄 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑘 ) )
20 wlkcl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
21 9 eqcomi ⊢ ( ♯ ‘ 𝐹 ) = 𝑁
22 21 eleq1i ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ↔ 𝑁 ∈ ℕ0 )
23 nn0fz0 ⊢ ( 𝑁 ∈ ℕ0 ↔ 𝑁 ∈ ( 0 ... 𝑁 ) )
24 22 23 sylbb ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → 𝑁 ∈ ( 0 ... 𝑁 ) )
25 8 20 24 3syl ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ... 𝑁 ) )
26 18 19 25 rspcdva ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑁 ) = ( 𝑃 ‘ 𝑁 ) )
27 14 fveq1i ⊢ ( 𝑄 ‘ ( 𝑁 + 1 ) ) = ( ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) ‘ ( 𝑁 + 1 ) )
28 ovex ⊢ ( 𝑁 + 1 ) ∈ V
29 1 2 3 4 5 6 7 8 9 wlkp1lem1 ⊢ ( 𝜑 → ¬ ( 𝑁 + 1 ) ∈ dom 𝑃 )
30 fsnunfv ⊢ ( ( ( 𝑁 + 1 ) ∈ V ∧ 𝐶 ∈ 𝑉 ∧ ¬ ( 𝑁 + 1 ) ∈ dom 𝑃 ) → ( ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) ‘ ( 𝑁 + 1 ) ) = 𝐶 )
31 28 6 29 30 mp3an2i ⊢ ( 𝜑 → ( ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) ‘ ( 𝑁 + 1 ) ) = 𝐶 )
32 27 31 eqtrid ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑁 + 1 ) ) = 𝐶 )
33 26 32 preq12d ⊢ ( 𝜑 → { ( 𝑄 ‘ 𝑁 ) , ( 𝑄 ‘ ( 𝑁 + 1 ) ) } = { ( 𝑃 ‘ 𝑁 ) , 𝐶 } )
34 fsnunfv ⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐸 ∈ ( Edg ‘ 𝐺 ) ∧ ¬ 𝐵 ∈ dom 𝐼 ) → ( ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) ‘ 𝐵 ) = 𝐸 )
35 5 10 7 34 syl3anc ⊢ ( 𝜑 → ( ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) ‘ 𝐵 ) = 𝐸 )
36 11 33 35 3sstr4d ⊢ ( 𝜑 → { ( 𝑄 ‘ 𝑁 ) , ( 𝑄 ‘ ( 𝑁 + 1 ) ) } ⊆ ( ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) ‘ 𝐵 ) )
37 1 2 3 4 5 6 7 8 9 10 11 12 13 wlkp1lem3 ⊢ ( 𝜑 → ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑁 ) ) = ( ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) ‘ 𝐵 ) )
38 36 37 sseqtrrd ⊢ ( 𝜑 → { ( 𝑄 ‘ 𝑁 ) , ( 𝑄 ‘ ( 𝑁 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑁 ) ) )