wwlksnextfun

	Ref	Expression
Hypotheses	wwlksnextbij0.v	$⊢ V = Vtx (G)$
	wwlksnextbij0.e	$⊢ E = Edg (G)$
	wwlksnextbij0.d	$⊢ D = \{w \in Word V \| (\|w\| = N + 2 \land w prefix (N + 1) = W \land \{lastS (W), lastS (w)\} \in E)\}$
	wwlksnextbij0.r	$⊢ R = \{n \in V \| \{lastS (W), n\} \in E\}$
	wwlksnextbij0.f	$⊢ F = (t \in D ⟼ lastS (t))$
Assertion	wwlksnextfun	$⊢ N \in ℕ_{0} \to F : D ⟶ R$

Proof

Step	Hyp	Ref	Expression
1		wwlksnextbij0.v	$⊢ V = Vtx (G)$
2		wwlksnextbij0.e	$⊢ E = Edg (G)$
3		wwlksnextbij0.d	$⊢ D = \{w \in Word V \| (\|w\| = N + 2 \land w prefix (N + 1) = W \land \{lastS (W), lastS (w)\} \in E)\}$
4		wwlksnextbij0.r	$⊢ R = \{n \in V \| \{lastS (W), n\} \in E\}$
5		wwlksnextbij0.f	$⊢ F = (t \in D ⟼ lastS (t))$
6		fveqeq2	$⊢ w = t \to (\|w\| = N + 2 \leftrightarrow \|t\| = N + 2)$
7		oveq1	$⊢ w = t \to w prefix (N + 1) = t prefix (N + 1)$
8	7	eqeq1d	$⊢ w = t \to (w prefix (N + 1) = W \leftrightarrow t prefix (N + 1) = W)$
9		fveq2	$⊢ w = t \to lastS (w) = lastS (t)$
10	9	preq2d	$⊢ w = t \to \{lastS (W), lastS (w)\} = \{lastS (W), lastS (t)\}$
11	10	eleq1d	$⊢ w = t \to (\{lastS (W), lastS (w)\} \in E \leftrightarrow \{lastS (W), lastS (t)\} \in E)$
12	6 8 11	3anbi123d	$⊢ w = t \to ((\|w\| = N + 2 \land w prefix (N + 1) = W \land \{lastS (W), lastS (w)\} \in E) \leftrightarrow (\|t\| = N + 2 \land t prefix (N + 1) = W \land \{lastS (W), lastS (t)\} \in E))$
13	12 3	elrab2	$⊢ t \in D \leftrightarrow (t \in Word V \land (\|t\| = N + 2 \land t prefix (N + 1) = W \land \{lastS (W), lastS (t)\} \in E))$
14		simpll	$⊢ ((t \in Word V \land N \in ℕ_{0}) \land \|t\| = N + 2) \to t \in Word V$
15		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
16		2re	$⊢ 2 \in ℝ$
17	16	a1i	$⊢ N \in ℕ_{0} \to 2 \in ℝ$
18		nn0ge0	$⊢ N \in ℕ_{0} \to 0 \leq N$
19		2pos	$⊢ 0 < 2$
20	19	a1i	$⊢ N \in ℕ_{0} \to 0 < 2$
21	15 17 18 20	addgegt0d	$⊢ N \in ℕ_{0} \to 0 < N + 2$
22	21	ad2antlr	$⊢ ((t \in Word V \land N \in ℕ_{0}) \land \|t\| = N + 2) \to 0 < N + 2$
23		breq2	$⊢ \|t\| = N + 2 \to (0 < \|t\| \leftrightarrow 0 < N + 2)$
24	23	adantl	$⊢ ((t \in Word V \land N \in ℕ_{0}) \land \|t\| = N + 2) \to (0 < \|t\| \leftrightarrow 0 < N + 2)$
25	22 24	mpbird	$⊢ ((t \in Word V \land N \in ℕ_{0}) \land \|t\| = N + 2) \to 0 < \|t\|$
26		hashgt0n0	$⊢ (t \in Word V \land 0 < \|t\|) \to t \neq \emptyset$
27	14 25 26	syl2anc	$⊢ ((t \in Word V \land N \in ℕ_{0}) \land \|t\| = N + 2) \to t \neq \emptyset$
28	14 27	jca	$⊢ ((t \in Word V \land N \in ℕ_{0}) \land \|t\| = N + 2) \to (t \in Word V \land t \neq \emptyset)$
29	28	expcom	$⊢ \|t\| = N + 2 \to ((t \in Word V \land N \in ℕ_{0}) \to (t \in Word V \land t \neq \emptyset))$
30	29	3ad2ant1	$⊢ (\|t\| = N + 2 \land t prefix (N + 1) = W \land \{lastS (W), lastS (t)\} \in E) \to ((t \in Word V \land N \in ℕ_{0}) \to (t \in Word V \land t \neq \emptyset))$
31	30	expd	$⊢ (\|t\| = N + 2 \land t prefix (N + 1) = W \land \{lastS (W), lastS (t)\} \in E) \to (t \in Word V \to (N \in ℕ_{0} \to (t \in Word V \land t \neq \emptyset)))$
32	31	impcom	$⊢ (t \in Word V \land (\|t\| = N + 2 \land t prefix (N + 1) = W \land \{lastS (W), lastS (t)\} \in E)) \to (N \in ℕ_{0} \to (t \in Word V \land t \neq \emptyset))$
33	32	impcom	$⊢ (N \in ℕ_{0} \land (t \in Word V \land (\|t\| = N + 2 \land t prefix (N + 1) = W \land \{lastS (W), lastS (t)\} \in E))) \to (t \in Word V \land t \neq \emptyset)$
34		lswcl	$⊢ (t \in Word V \land t \neq \emptyset) \to lastS (t) \in V$
35	33 34	syl	$⊢ (N \in ℕ_{0} \land (t \in Word V \land (\|t\| = N + 2 \land t prefix (N + 1) = W \land \{lastS (W), lastS (t)\} \in E))) \to lastS (t) \in V$
36		simprr3	$⊢ (N \in ℕ_{0} \land (t \in Word V \land (\|t\| = N + 2 \land t prefix (N + 1) = W \land \{lastS (W), lastS (t)\} \in E))) \to \{lastS (W), lastS (t)\} \in E$
37	35 36	jca	$⊢ (N \in ℕ_{0} \land (t \in Word V \land (\|t\| = N + 2 \land t prefix (N + 1) = W \land \{lastS (W), lastS (t)\} \in E))) \to (lastS (t) \in V \land \{lastS (W), lastS (t)\} \in E)$
38	13 37	sylan2b	$⊢ (N \in ℕ_{0} \land t \in D) \to (lastS (t) \in V \land \{lastS (W), lastS (t)\} \in E)$
39		preq2	$⊢ n = lastS (t) \to \{lastS (W), n\} = \{lastS (W), lastS (t)\}$
40	39	eleq1d	$⊢ n = lastS (t) \to (\{lastS (W), n\} \in E \leftrightarrow \{lastS (W), lastS (t)\} \in E)$
41	40 4	elrab2	$⊢ lastS (t) \in R \leftrightarrow (lastS (t) \in V \land \{lastS (W), lastS (t)\} \in E)$
42	38 41	sylibr	$⊢ (N \in ℕ_{0} \land t \in D) \to lastS (t) \in R$
43	42 5	fmptd	$⊢ N \in ℕ_{0} \to F : D ⟶ R$

Metamath Proof Explorer

Theorem wwlksnextfun

Proof