clwwlkfo

Description: Lemma 4 for clwwlkf1o : F is an onto function. (Contributed by Alexander van der Vekens, 29-Sep-2018) (Revised by AV, 26-Apr-2021) (Revised by AV, 1-Nov-2022)

	Ref	Expression
Hypotheses	clwwlkf1o.d	$⊢ D = \{w \in (N WWalksN G) \| lastS (w) = w (0)\}$
	clwwlkf1o.f	$⊢ F = (t \in D ⟼ t prefix N)$
Assertion	clwwlkfo	$⊢ N \in ℕ \to F : D \underset{onto}{⟶} N ClWWalksN G$

Proof

Step	Hyp	Ref	Expression
1		clwwlkf1o.d	$⊢ D = \{w \in (N WWalksN G) \| lastS (w) = w (0)\}$
2		clwwlkf1o.f	$⊢ F = (t \in D ⟼ t prefix N)$
3	1 2	clwwlkf	$⊢ N \in ℕ \to F : D ⟶ N ClWWalksN G$
4		eqid	$⊢ Vtx (G) = Vtx (G)$
5		eqid	$⊢ Edg (G) = Edg (G)$
6	4 5	clwwlknp	$⊢ p \in (N ClWWalksN G) \to ((p \in Word Vtx (G) \land \|p\| = N) \land \forall i \in (0 ..^N - 1) \{p (i), p (i + 1)\} \in Edg (G) \land \{lastS (p), p (0)\} \in Edg (G))$
7		simpr	$⊢ (((p \in Word Vtx (G) \land \|p\| = N) \land \forall i \in (0 ..^N - 1) \{p (i), p (i + 1)\} \in Edg (G) \land \{lastS (p), p (0)\} \in Edg (G)) \land N \in ℕ) \to N \in ℕ$
8		simpl1	$⊢ (((p \in Word Vtx (G) \land \|p\| = N) \land \forall i \in (0 ..^N - 1) \{p (i), p (i + 1)\} \in Edg (G) \land \{lastS (p), p (0)\} \in Edg (G)) \land N \in ℕ) \to (p \in Word Vtx (G) \land \|p\| = N)$
9		3simpc	$⊢ ((p \in Word Vtx (G) \land \|p\| = N) \land \forall i \in (0 ..^N - 1) \{p (i), p (i + 1)\} \in Edg (G) \land \{lastS (p), p (0)\} \in Edg (G)) \to (\forall i \in (0 ..^N - 1) \{p (i), p (i + 1)\} \in Edg (G) \land \{lastS (p), p (0)\} \in Edg (G))$
10	9	adantr	$⊢ (((p \in Word Vtx (G) \land \|p\| = N) \land \forall i \in (0 ..^N - 1) \{p (i), p (i + 1)\} \in Edg (G) \land \{lastS (p), p (0)\} \in Edg (G)) \land N \in ℕ) \to (\forall i \in (0 ..^N - 1) \{p (i), p (i + 1)\} \in Edg (G) \land \{lastS (p), p (0)\} \in Edg (G))$
11	1	clwwlkel	$⊢ (N \in ℕ \land (p \in Word Vtx (G) \land \|p\| = N) \land (\forall i \in (0 ..^N - 1) \{p (i), p (i + 1)\} \in Edg (G) \land \{lastS (p), p (0)\} \in Edg (G))) \to p ++ ⟨“ p (0) ”⟩ \in D$
12	7 8 10 11	syl3anc	$⊢ (((p \in Word Vtx (G) \land \|p\| = N) \land \forall i \in (0 ..^N - 1) \{p (i), p (i + 1)\} \in Edg (G) \land \{lastS (p), p (0)\} \in Edg (G)) \land N \in ℕ) \to p ++ ⟨“ p (0) ”⟩ \in D$
13		oveq2	$⊢ N = \|p\| \to (p ++ ⟨“ p (0) ”⟩) prefix N = (p ++ ⟨“ p (0) ”⟩) prefix \|p\|$
14	13	eqcoms	$⊢ \|p\| = N \to (p ++ ⟨“ p (0) ”⟩) prefix N = (p ++ ⟨“ p (0) ”⟩) prefix \|p\|$
15	14	adantl	$⊢ (p \in Word Vtx (G) \land \|p\| = N) \to (p ++ ⟨“ p (0) ”⟩) prefix N = (p ++ ⟨“ p (0) ”⟩) prefix \|p\|$
16	15	3ad2ant1	$⊢ ((p \in Word Vtx (G) \land \|p\| = N) \land \forall i \in (0 ..^N - 1) \{p (i), p (i + 1)\} \in Edg (G) \land \{lastS (p), p (0)\} \in Edg (G)) \to (p ++ ⟨“ p (0) ”⟩) prefix N = (p ++ ⟨“ p (0) ”⟩) prefix \|p\|$
17	16	adantr	$⊢ (((p \in Word Vtx (G) \land \|p\| = N) \land \forall i \in (0 ..^N - 1) \{p (i), p (i + 1)\} \in Edg (G) \land \{lastS (p), p (0)\} \in Edg (G)) \land N \in ℕ) \to (p ++ ⟨“ p (0) ”⟩) prefix N = (p ++ ⟨“ p (0) ”⟩) prefix \|p\|$
18		simpll	$⊢ ((p \in Word Vtx (G) \land \|p\| = N) \land N \in ℕ) \to p \in Word Vtx (G)$
19		fstwrdne0	$⊢ (N \in ℕ \land (p \in Word Vtx (G) \land \|p\| = N)) \to p (0) \in Vtx (G)$
20	19	ancoms	$⊢ ((p \in Word Vtx (G) \land \|p\| = N) \land N \in ℕ) \to p (0) \in Vtx (G)$
21	20	s1cld	$⊢ ((p \in Word Vtx (G) \land \|p\| = N) \land N \in ℕ) \to ⟨“ p (0) ”⟩ \in Word Vtx (G)$
22	18 21	jca	$⊢ ((p \in Word Vtx (G) \land \|p\| = N) \land N \in ℕ) \to (p \in Word Vtx (G) \land ⟨“ p (0) ”⟩ \in Word Vtx (G))$
23	22	3ad2antl1	$⊢ (((p \in Word Vtx (G) \land \|p\| = N) \land \forall i \in (0 ..^N - 1) \{p (i), p (i + 1)\} \in Edg (G) \land \{lastS (p), p (0)\} \in Edg (G)) \land N \in ℕ) \to (p \in Word Vtx (G) \land ⟨“ p (0) ”⟩ \in Word Vtx (G))$
24		pfxccat1	$⊢ (p \in Word Vtx (G) \land ⟨“ p (0) ”⟩ \in Word Vtx (G)) \to (p ++ ⟨“ p (0) ”⟩) prefix \|p\| = p$
25	23 24	syl	$⊢ (((p \in Word Vtx (G) \land \|p\| = N) \land \forall i \in (0 ..^N - 1) \{p (i), p (i + 1)\} \in Edg (G) \land \{lastS (p), p (0)\} \in Edg (G)) \land N \in ℕ) \to (p ++ ⟨“ p (0) ”⟩) prefix \|p\| = p$
26	17 25	eqtr2d	$⊢ (((p \in Word Vtx (G) \land \|p\| = N) \land \forall i \in (0 ..^N - 1) \{p (i), p (i + 1)\} \in Edg (G) \land \{lastS (p), p (0)\} \in Edg (G)) \land N \in ℕ) \to p = (p ++ ⟨“ p (0) ”⟩) prefix N$
27	12 26	jca	$⊢ (((p \in Word Vtx (G) \land \|p\| = N) \land \forall i \in (0 ..^N - 1) \{p (i), p (i + 1)\} \in Edg (G) \land \{lastS (p), p (0)\} \in Edg (G)) \land N \in ℕ) \to (p ++ ⟨“ p (0) ”⟩ \in D \land p = (p ++ ⟨“ p (0) ”⟩) prefix N)$
28	27	ex	$⊢ ((p \in Word Vtx (G) \land \|p\| = N) \land \forall i \in (0 ..^N - 1) \{p (i), p (i + 1)\} \in Edg (G) \land \{lastS (p), p (0)\} \in Edg (G)) \to (N \in ℕ \to (p ++ ⟨“ p (0) ”⟩ \in D \land p = (p ++ ⟨“ p (0) ”⟩) prefix N))$
29	6 28	syl	$⊢ p \in (N ClWWalksN G) \to (N \in ℕ \to (p ++ ⟨“ p (0) ”⟩ \in D \land p = (p ++ ⟨“ p (0) ”⟩) prefix N))$
30	29	impcom	$⊢ (N \in ℕ \land p \in (N ClWWalksN G)) \to (p ++ ⟨“ p (0) ”⟩ \in D \land p = (p ++ ⟨“ p (0) ”⟩) prefix N)$
31		oveq1	$⊢ x = p ++ ⟨“ p (0) ”⟩ \to x prefix N = (p ++ ⟨“ p (0) ”⟩) prefix N$
32	31	rspceeqv	$⊢ (p ++ ⟨“ p (0) ”⟩ \in D \land p = (p ++ ⟨“ p (0) ”⟩) prefix N) \to \exists x \in D p = x prefix N$
33	30 32	syl	$⊢ (N \in ℕ \land p \in (N ClWWalksN G)) \to \exists x \in D p = x prefix N$
34	1 2	clwwlkfv	$⊢ x \in D \to F (x) = x prefix N$
35	34	eqeq2d	$⊢ x \in D \to (p = F (x) \leftrightarrow p = x prefix N)$
36	35	adantl	$⊢ ((N \in ℕ \land p \in (N ClWWalksN G)) \land x \in D) \to (p = F (x) \leftrightarrow p = x prefix N)$
37	36	rexbidva	$⊢ (N \in ℕ \land p \in (N ClWWalksN G)) \to (\exists x \in D p = F (x) \leftrightarrow \exists x \in D p = x prefix N)$
38	33 37	mpbird	$⊢ (N \in ℕ \land p \in (N ClWWalksN G)) \to \exists x \in D p = F (x)$
39	38	ralrimiva	$⊢ N \in ℕ \to \forall p \in (N ClWWalksN G) \exists x \in D p = F (x)$
40		dffo3	$⊢ F : D \underset{onto}{⟶} N ClWWalksN G \leftrightarrow (F : D ⟶ N ClWWalksN G \land \forall p \in (N ClWWalksN G) \exists x \in D p = F (x))$
41	3 39 40	sylanbrc	$⊢ N \in ℕ \to F : D \underset{onto}{⟶} N ClWWalksN G$

Metamath Proof Explorer

Theorem clwwlkfo

Proof