Theorem wwlksnextfun

Description: Lemma for wwlksnextbij . (Contributed by Alexander van der Vekens, 7-Aug-2018) (Revised by AV, 18-Apr-2021) (Revised by AV, 27-Oct-2022)

	Ref	Expression
Hypotheses	wwlksnextbij0.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	wwlksnextbij0.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	wwlksnextbij0.d	⊢ 𝐷 = { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ∧ ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) }
	wwlksnextbij0.r	⊢ 𝑅 = { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑊 ) , 𝑛 } ∈ 𝐸 }
	wwlksnextbij0.f	⊢ 𝐹 = ( 𝑡 ∈ 𝐷 ↦ ( lastS ‘ 𝑡 ) )
Assertion	wwlksnextfun	⊢ ( 𝑁 ∈ ℕ0 → 𝐹 : 𝐷 ⟶ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		wwlksnextbij0.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		wwlksnextbij0.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		wwlksnextbij0.d	⊢ 𝐷 = { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ∧ ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) }
4		wwlksnextbij0.r	⊢ 𝑅 = { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑊 ) , 𝑛 } ∈ 𝐸 }
5		wwlksnextbij0.f	⊢ 𝐹 = ( 𝑡 ∈ 𝐷 ↦ ( lastS ‘ 𝑡 ) )
6		fveqeq2	⊢ ( 𝑤 = 𝑡 → ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ↔ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ) )
7		oveq1	⊢ ( 𝑤 = 𝑡 → ( 𝑤 prefix ( 𝑁 + 1 ) ) = ( 𝑡 prefix ( 𝑁 + 1 ) ) )
8	7	eqeq1d	⊢ ( 𝑤 = 𝑡 → ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ↔ ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ) )
9		fveq2	⊢ ( 𝑤 = 𝑡 → ( lastS ‘ 𝑤 ) = ( lastS ‘ 𝑡 ) )
10	9	preq2d	⊢ ( 𝑤 = 𝑡 → { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } = { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } )
11	10	eleq1d	⊢ ( 𝑤 = 𝑡 → ( { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ↔ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) )
12	6 8 11	3anbi123d	⊢ ( 𝑤 = 𝑡 → ( ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ∧ ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) ↔ ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ∧ ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) ) )
13	12 3	elrab2	⊢ ( 𝑡 ∈ 𝐷 ↔ ( 𝑡 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ∧ ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) ) )
14		simpll	⊢ ( ( ( 𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ) → 𝑡 ∈ Word 𝑉 )
15		nn0re	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
16		2re	⊢ 2 ∈ ℝ
17	16	a1i	⊢ ( 𝑁 ∈ ℕ0 → 2 ∈ ℝ )
18		nn0ge0	⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 )
19		2pos	⊢ 0 < 2
20	19	a1i	⊢ ( 𝑁 ∈ ℕ0 → 0 < 2 )
21	15 17 18 20	addgegt0d	⊢ ( 𝑁 ∈ ℕ0 → 0 < ( 𝑁 + 2 ) )
22	21	ad2antlr	⊢ ( ( ( 𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ) → 0 < ( 𝑁 + 2 ) )
23		breq2	⊢ ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) → ( 0 < ( ♯ ‘ 𝑡 ) ↔ 0 < ( 𝑁 + 2 ) ) )
24	23	adantl	⊢ ( ( ( 𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ) → ( 0 < ( ♯ ‘ 𝑡 ) ↔ 0 < ( 𝑁 + 2 ) ) )
25	22 24	mpbird	⊢ ( ( ( 𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ) → 0 < ( ♯ ‘ 𝑡 ) )
26		hashgt0n0	⊢ ( ( 𝑡 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑡 ) ) → 𝑡 ≠ ∅ )
27	14 25 26	syl2anc	⊢ ( ( ( 𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ) → 𝑡 ≠ ∅ )
28	14 27	jca	⊢ ( ( ( 𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ) → ( 𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅ ) )
29	28	expcom	⊢ ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) → ( ( 𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅ ) ) )
30	29	3ad2ant1	⊢ ( ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ∧ ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) → ( ( 𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅ ) ) )
31	30	expd	⊢ ( ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ∧ ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) → ( 𝑡 ∈ Word 𝑉 → ( 𝑁 ∈ ℕ0 → ( 𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅ ) ) ) )
32	31	impcom	⊢ ( ( 𝑡 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ∧ ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) ) → ( 𝑁 ∈ ℕ0 → ( 𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅ ) ) )
33	32	impcom	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ∧ ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) ) ) → ( 𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅ ) )
34		lswcl	⊢ ( ( 𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅ ) → ( lastS ‘ 𝑡 ) ∈ 𝑉 )
35	33 34	syl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ∧ ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) ) ) → ( lastS ‘ 𝑡 ) ∈ 𝑉 )
36		simprr3	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ∧ ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) ) ) → { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 )
37	35 36	jca	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑡 ) = ( 𝑁 + 2 ) ∧ ( 𝑡 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) ) ) → ( ( lastS ‘ 𝑡 ) ∈ 𝑉 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) )
38	13 37	sylan2b	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑡 ∈ 𝐷 ) → ( ( lastS ‘ 𝑡 ) ∈ 𝑉 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) )
39		preq2	⊢ ( 𝑛 = ( lastS ‘ 𝑡 ) → { ( lastS ‘ 𝑊 ) , 𝑛 } = { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } )
40	39	eleq1d	⊢ ( 𝑛 = ( lastS ‘ 𝑡 ) → ( { ( lastS ‘ 𝑊 ) , 𝑛 } ∈ 𝐸 ↔ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) )
41	40 4	elrab2	⊢ ( ( lastS ‘ 𝑡 ) ∈ 𝑅 ↔ ( ( lastS ‘ 𝑡 ) ∈ 𝑉 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑡 ) } ∈ 𝐸 ) )
42	38 41	sylibr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑡 ∈ 𝐷 ) → ( lastS ‘ 𝑡 ) ∈ 𝑅 )
43	42 5	fmptd	⊢ ( 𝑁 ∈ ℕ0 → 𝐹 : 𝐷 ⟶ 𝑅 )