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	syl5eq	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑁 + 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 ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑁 ) ) )