wwlksnextsurj

	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	wwlksnextsurj	$⊢ W \in (N WWalksN G) \to F : D \underset{onto}{⟶} 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	1	wwlknbp	$⊢ W \in (N WWalksN G) \to (G \in V \land N \in ℕ_{0} \land W \in Word V)$
7		simp2	$⊢ (G \in V \land N \in ℕ_{0} \land W \in Word V) \to N \in ℕ_{0}$
8	1 2 3 4 5	wwlksnextfun	$⊢ N \in ℕ_{0} \to F : D ⟶ R$
9	6 7 8	3syl	$⊢ W \in (N WWalksN G) \to F : D ⟶ R$
10		preq2	$⊢ n = r \to \{lastS (W), n\} = \{lastS (W), r\}$
11	10	eleq1d	$⊢ n = r \to (\{lastS (W), n\} \in E \leftrightarrow \{lastS (W), r\} \in E)$
12	11 4	elrab2	$⊢ r \in R \leftrightarrow (r \in V \land \{lastS (W), r\} \in E)$
13	1 2	wwlksnext	$⊢ (W \in (N WWalksN G) \land r \in V \land \{lastS (W), r\} \in E) \to W ++ ⟨“ r ”⟩ \in ((N + 1) WWalksN G)$
14	13	3expb	$⊢ (W \in (N WWalksN G) \land (r \in V \land \{lastS (W), r\} \in E)) \to W ++ ⟨“ r ”⟩ \in ((N + 1) WWalksN G)$
15		s1cl	$⊢ r \in V \to ⟨“ r ”⟩ \in Word V$
16		pfxccat1	$⊢ (W \in Word V \land ⟨“ r ”⟩ \in Word V) \to (W ++ ⟨“ r ”⟩) prefix \|W\| = W$
17	15 16	sylan2	$⊢ (W \in Word V \land r \in V) \to (W ++ ⟨“ r ”⟩) prefix \|W\| = W$
18	17	ex	$⊢ W \in Word V \to (r \in V \to (W ++ ⟨“ r ”⟩) prefix \|W\| = W)$
19	18	adantr	$⊢ (W \in Word V \land \|W\| = N + 1) \to (r \in V \to (W ++ ⟨“ r ”⟩) prefix \|W\| = W)$
20		oveq2	$⊢ N + 1 = \|W\| \to (W ++ ⟨“ r ”⟩) prefix (N + 1) = (W ++ ⟨“ r ”⟩) prefix \|W\|$
21	20	eqcoms	$⊢ \|W\| = N + 1 \to (W ++ ⟨“ r ”⟩) prefix (N + 1) = (W ++ ⟨“ r ”⟩) prefix \|W\|$
22	21	eqeq1d	$⊢ \|W\| = N + 1 \to ((W ++ ⟨“ r ”⟩) prefix (N + 1) = W \leftrightarrow (W ++ ⟨“ r ”⟩) prefix \|W\| = W)$
23	22	adantl	$⊢ (W \in Word V \land \|W\| = N + 1) \to ((W ++ ⟨“ r ”⟩) prefix (N + 1) = W \leftrightarrow (W ++ ⟨“ r ”⟩) prefix \|W\| = W)$
24	19 23	sylibrd	$⊢ (W \in Word V \land \|W\| = N + 1) \to (r \in V \to (W ++ ⟨“ r ”⟩) prefix (N + 1) = W)$
25	24	3adant3	$⊢ (W \in Word V \land \|W\| = N + 1 \land \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in E) \to (r \in V \to (W ++ ⟨“ r ”⟩) prefix (N + 1) = W)$
26	1 2	wwlknp	$⊢ W \in (N WWalksN G) \to (W \in Word V \land \|W\| = N + 1 \land \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in E)$
27	25 26	syl11	$⊢ r \in V \to (W \in (N WWalksN G) \to (W ++ ⟨“ r ”⟩) prefix (N + 1) = W)$
28	27	adantr	$⊢ (r \in V \land \{lastS (W), r\} \in E) \to (W \in (N WWalksN G) \to (W ++ ⟨“ r ”⟩) prefix (N + 1) = W)$
29	28	impcom	$⊢ (W \in (N WWalksN G) \land (r \in V \land \{lastS (W), r\} \in E)) \to (W ++ ⟨“ r ”⟩) prefix (N + 1) = W$
30		lswccats1	$⊢ (W \in Word V \land r \in V) \to lastS (W ++ ⟨“ r ”⟩) = r$
31	30	eqcomd	$⊢ (W \in Word V \land r \in V) \to r = lastS (W ++ ⟨“ r ”⟩)$
32	31	ex	$⊢ W \in Word V \to (r \in V \to r = lastS (W ++ ⟨“ r ”⟩))$
33	32	3ad2ant3	$⊢ (G \in V \land N \in ℕ_{0} \land W \in Word V) \to (r \in V \to r = lastS (W ++ ⟨“ r ”⟩))$
34	6 33	syl	$⊢ W \in (N WWalksN G) \to (r \in V \to r = lastS (W ++ ⟨“ r ”⟩))$
35	34	imp	$⊢ (W \in (N WWalksN G) \land r \in V) \to r = lastS (W ++ ⟨“ r ”⟩)$
36	35	preq2d	$⊢ (W \in (N WWalksN G) \land r \in V) \to \{lastS (W), r\} = \{lastS (W), lastS (W ++ ⟨“ r ”⟩)\}$
37	36	eleq1d	$⊢ (W \in (N WWalksN G) \land r \in V) \to (\{lastS (W), r\} \in E \leftrightarrow \{lastS (W), lastS (W ++ ⟨“ r ”⟩)\} \in E)$
38	37	biimpd	$⊢ (W \in (N WWalksN G) \land r \in V) \to (\{lastS (W), r\} \in E \to \{lastS (W), lastS (W ++ ⟨“ r ”⟩)\} \in E)$
39	38	impr	$⊢ (W \in (N WWalksN G) \land (r \in V \land \{lastS (W), r\} \in E)) \to \{lastS (W), lastS (W ++ ⟨“ r ”⟩)\} \in E$
40	14 29 39	jca32	$⊢ (W \in (N WWalksN G) \land (r \in V \land \{lastS (W), r\} \in E)) \to (W ++ ⟨“ r ”⟩ \in ((N + 1) WWalksN G) \land ((W ++ ⟨“ r ”⟩) prefix (N + 1) = W \land \{lastS (W), lastS (W ++ ⟨“ r ”⟩)\} \in E))$
41	33 6	syl11	$⊢ r \in V \to (W \in (N WWalksN G) \to r = lastS (W ++ ⟨“ r ”⟩))$
42	41	adantr	$⊢ (r \in V \land \{lastS (W), r\} \in E) \to (W \in (N WWalksN G) \to r = lastS (W ++ ⟨“ r ”⟩))$
43	42	impcom	$⊢ (W \in (N WWalksN G) \land (r \in V \land \{lastS (W), r\} \in E)) \to r = lastS (W ++ ⟨“ r ”⟩)$
44		ovexd	$⊢ (W \in (N WWalksN G) \land (r \in V \land \{lastS (W), r\} \in E)) \to W ++ ⟨“ r ”⟩ \in V$
45		eleq1	$⊢ d = W ++ ⟨“ r ”⟩ \to (d \in ((N + 1) WWalksN G) \leftrightarrow W ++ ⟨“ r ”⟩ \in ((N + 1) WWalksN G))$
46		oveq1	$⊢ d = W ++ ⟨“ r ”⟩ \to d prefix (N + 1) = (W ++ ⟨“ r ”⟩) prefix (N + 1)$
47	46	eqeq1d	$⊢ d = W ++ ⟨“ r ”⟩ \to (d prefix (N + 1) = W \leftrightarrow (W ++ ⟨“ r ”⟩) prefix (N + 1) = W)$
48		fveq2	$⊢ d = W ++ ⟨“ r ”⟩ \to lastS (d) = lastS (W ++ ⟨“ r ”⟩)$
49	48	preq2d	$⊢ d = W ++ ⟨“ r ”⟩ \to \{lastS (W), lastS (d)\} = \{lastS (W), lastS (W ++ ⟨“ r ”⟩)\}$
50	49	eleq1d	$⊢ d = W ++ ⟨“ r ”⟩ \to (\{lastS (W), lastS (d)\} \in E \leftrightarrow \{lastS (W), lastS (W ++ ⟨“ r ”⟩)\} \in E)$
51	47 50	anbi12d	$⊢ d = W ++ ⟨“ r ”⟩ \to ((d prefix (N + 1) = W \land \{lastS (W), lastS (d)\} \in E) \leftrightarrow ((W ++ ⟨“ r ”⟩) prefix (N + 1) = W \land \{lastS (W), lastS (W ++ ⟨“ r ”⟩)\} \in E))$
52	45 51	anbi12d	$⊢ d = W ++ ⟨“ r ”⟩ \to ((d \in ((N + 1) WWalksN G) \land (d prefix (N + 1) = W \land \{lastS (W), lastS (d)\} \in E)) \leftrightarrow (W ++ ⟨“ r ”⟩ \in ((N + 1) WWalksN G) \land ((W ++ ⟨“ r ”⟩) prefix (N + 1) = W \land \{lastS (W), lastS (W ++ ⟨“ r ”⟩)\} \in E)))$
53	48	eqeq2d	$⊢ d = W ++ ⟨“ r ”⟩ \to (r = lastS (d) \leftrightarrow r = lastS (W ++ ⟨“ r ”⟩))$
54	52 53	anbi12d	$⊢ d = W ++ ⟨“ r ”⟩ \to (((d \in ((N + 1) WWalksN G) \land (d prefix (N + 1) = W \land \{lastS (W), lastS (d)\} \in E)) \land r = lastS (d)) \leftrightarrow ((W ++ ⟨“ r ”⟩ \in ((N + 1) WWalksN G) \land ((W ++ ⟨“ r ”⟩) prefix (N + 1) = W \land \{lastS (W), lastS (W ++ ⟨“ r ”⟩)\} \in E)) \land r = lastS (W ++ ⟨“ r ”⟩)))$
55	54	bicomd	$⊢ d = W ++ ⟨“ r ”⟩ \to (((W ++ ⟨“ r ”⟩ \in ((N + 1) WWalksN G) \land ((W ++ ⟨“ r ”⟩) prefix (N + 1) = W \land \{lastS (W), lastS (W ++ ⟨“ r ”⟩)\} \in E)) \land r = lastS (W ++ ⟨“ r ”⟩)) \leftrightarrow ((d \in ((N + 1) WWalksN G) \land (d prefix (N + 1) = W \land \{lastS (W), lastS (d)\} \in E)) \land r = lastS (d)))$
56	55	adantl	$⊢ ((W \in (N WWalksN G) \land (r \in V \land \{lastS (W), r\} \in E)) \land d = W ++ ⟨“ r ”⟩) \to (((W ++ ⟨“ r ”⟩ \in ((N + 1) WWalksN G) \land ((W ++ ⟨“ r ”⟩) prefix (N + 1) = W \land \{lastS (W), lastS (W ++ ⟨“ r ”⟩)\} \in E)) \land r = lastS (W ++ ⟨“ r ”⟩)) \leftrightarrow ((d \in ((N + 1) WWalksN G) \land (d prefix (N + 1) = W \land \{lastS (W), lastS (d)\} \in E)) \land r = lastS (d)))$
57	56	biimpd	$⊢ ((W \in (N WWalksN G) \land (r \in V \land \{lastS (W), r\} \in E)) \land d = W ++ ⟨“ r ”⟩) \to (((W ++ ⟨“ r ”⟩ \in ((N + 1) WWalksN G) \land ((W ++ ⟨“ r ”⟩) prefix (N + 1) = W \land \{lastS (W), lastS (W ++ ⟨“ r ”⟩)\} \in E)) \land r = lastS (W ++ ⟨“ r ”⟩)) \to ((d \in ((N + 1) WWalksN G) \land (d prefix (N + 1) = W \land \{lastS (W), lastS (d)\} \in E)) \land r = lastS (d)))$
58	44 57	spcimedv	$⊢ (W \in (N WWalksN G) \land (r \in V \land \{lastS (W), r\} \in E)) \to (((W ++ ⟨“ r ”⟩ \in ((N + 1) WWalksN G) \land ((W ++ ⟨“ r ”⟩) prefix (N + 1) = W \land \{lastS (W), lastS (W ++ ⟨“ r ”⟩)\} \in E)) \land r = lastS (W ++ ⟨“ r ”⟩)) \to \exists d ((d \in ((N + 1) WWalksN G) \land (d prefix (N + 1) = W \land \{lastS (W), lastS (d)\} \in E)) \land r = lastS (d)))$
59	40 43 58	mp2and	$⊢ (W \in (N WWalksN G) \land (r \in V \land \{lastS (W), r\} \in E)) \to \exists d ((d \in ((N + 1) WWalksN G) \land (d prefix (N + 1) = W \land \{lastS (W), lastS (d)\} \in E)) \land r = lastS (d))$
60		oveq1	$⊢ w = d \to w prefix (N + 1) = d prefix (N + 1)$
61	60	eqeq1d	$⊢ w = d \to (w prefix (N + 1) = W \leftrightarrow d prefix (N + 1) = W)$
62		fveq2	$⊢ w = d \to lastS (w) = lastS (d)$
63	62	preq2d	$⊢ w = d \to \{lastS (W), lastS (w)\} = \{lastS (W), lastS (d)\}$
64	63	eleq1d	$⊢ w = d \to (\{lastS (W), lastS (w)\} \in E \leftrightarrow \{lastS (W), lastS (d)\} \in E)$
65	61 64	anbi12d	$⊢ w = d \to ((w prefix (N + 1) = W \land \{lastS (W), lastS (w)\} \in E) \leftrightarrow (d prefix (N + 1) = W \land \{lastS (W), lastS (d)\} \in E))$
66	65	elrab	$⊢ d \in \{w \in ((N + 1) WWalksN G) \| (w prefix (N + 1) = W \land \{lastS (W), lastS (w)\} \in E)\} \leftrightarrow (d \in ((N + 1) WWalksN G) \land (d prefix (N + 1) = W \land \{lastS (W), lastS (d)\} \in E))$
67	66	anbi1i	$⊢ (d \in \{w \in ((N + 1) WWalksN G) \| (w prefix (N + 1) = W \land \{lastS (W), lastS (w)\} \in E)\} \land r = lastS (d)) \leftrightarrow ((d \in ((N + 1) WWalksN G) \land (d prefix (N + 1) = W \land \{lastS (W), lastS (d)\} \in E)) \land r = lastS (d))$
68	67	exbii	$⊢ \exists d (d \in \{w \in ((N + 1) WWalksN G) \| (w prefix (N + 1) = W \land \{lastS (W), lastS (w)\} \in E)\} \land r = lastS (d)) \leftrightarrow \exists d ((d \in ((N + 1) WWalksN G) \land (d prefix (N + 1) = W \land \{lastS (W), lastS (d)\} \in E)) \land r = lastS (d))$
69	59 68	sylibr	$⊢ (W \in (N WWalksN G) \land (r \in V \land \{lastS (W), r\} \in E)) \to \exists d (d \in \{w \in ((N + 1) WWalksN G) \| (w prefix (N + 1) = W \land \{lastS (W), lastS (w)\} \in E)\} \land r = lastS (d))$
70		df-rex	$⊢ \exists d \in \{w \in ((N + 1) WWalksN G) \| (w prefix (N + 1) = W \land \{lastS (W), lastS (w)\} \in E)\} r = lastS (d) \leftrightarrow \exists d (d \in \{w \in ((N + 1) WWalksN G) \| (w prefix (N + 1) = W \land \{lastS (W), lastS (w)\} \in E)\} \land r = lastS (d))$
71	69 70	sylibr	$⊢ (W \in (N WWalksN G) \land (r \in V \land \{lastS (W), r\} \in E)) \to \exists d \in \{w \in ((N + 1) WWalksN G) \| (w prefix (N + 1) = W \land \{lastS (W), lastS (w)\} \in E)\} r = lastS (d)$
72	1 2 3	wwlksnextwrd	$⊢ W \in (N WWalksN G) \to D = \{w \in ((N + 1) WWalksN G) \| (w prefix (N + 1) = W \land \{lastS (W), lastS (w)\} \in E)\}$
73	72	adantr	$⊢ (W \in (N WWalksN G) \land (r \in V \land \{lastS (W), r\} \in E)) \to D = \{w \in ((N + 1) WWalksN G) \| (w prefix (N + 1) = W \land \{lastS (W), lastS (w)\} \in E)\}$
74	73	rexeqdv	$⊢ (W \in (N WWalksN G) \land (r \in V \land \{lastS (W), r\} \in E)) \to (\exists d \in D r = lastS (d) \leftrightarrow \exists d \in \{w \in ((N + 1) WWalksN G) \| (w prefix (N + 1) = W \land \{lastS (W), lastS (w)\} \in E)\} r = lastS (d))$
75	71 74	mpbird	$⊢ (W \in (N WWalksN G) \land (r \in V \land \{lastS (W), r\} \in E)) \to \exists d \in D r = lastS (d)$
76		fveq2	$⊢ t = d \to lastS (t) = lastS (d)$
77		fvex	$⊢ lastS (d) \in V$
78	76 5 77	fvmpt	$⊢ d \in D \to F (d) = lastS (d)$
79	78	eqeq2d	$⊢ d \in D \to (r = F (d) \leftrightarrow r = lastS (d))$
80	79	rexbiia	$⊢ \exists d \in D r = F (d) \leftrightarrow \exists d \in D r = lastS (d)$
81	75 80	sylibr	$⊢ (W \in (N WWalksN G) \land (r \in V \land \{lastS (W), r\} \in E)) \to \exists d \in D r = F (d)$
82	12 81	sylan2b	$⊢ (W \in (N WWalksN G) \land r \in R) \to \exists d \in D r = F (d)$
83	82	ralrimiva	$⊢ W \in (N WWalksN G) \to \forall r \in R \exists d \in D r = F (d)$
84		dffo3	$⊢ F : D \underset{onto}{⟶} R \leftrightarrow (F : D ⟶ R \land \forall r \in R \exists d \in D r = F (d))$
85	9 83 84	sylanbrc	$⊢ W \in (N WWalksN G) \to F : D \underset{onto}{⟶} R$

Metamath Proof Explorer

Theorem wwlksnextsurj

Proof