clwlkclwwlkf

Description: F is a function from the nonempty closed walks into the closed walks as word in a simple pseudograph. (Contributed by AV, 23-May-2022) (Revised by AV, 29-Oct-2022)

	Ref	Expression
Hypotheses	clwlkclwwlkf.c	$⊢ C = \{w \in ClWalks (G) \| 1 \leq \|1^{st} (w)\|\}$
	clwlkclwwlkf.f	$⊢ F = (c \in C ⟼ 2^{nd} (c) prefix (\|2^{nd} (c)\| - 1))$
Assertion	clwlkclwwlkf	$⊢ G \in USHGraph \to F : C ⟶ ClWWalks (G)$

Proof

Step	Hyp	Ref	Expression
1		clwlkclwwlkf.c	$⊢ C = \{w \in ClWalks (G) \| 1 \leq \|1^{st} (w)\|\}$
2		clwlkclwwlkf.f	$⊢ F = (c \in C ⟼ 2^{nd} (c) prefix (\|2^{nd} (c)\| - 1))$
3		eqid	$⊢ 1^{st} (c) = 1^{st} (c)$
4		eqid	$⊢ 2^{nd} (c) = 2^{nd} (c)$
5	1 3 4	clwlkclwwlkflem	$⊢ c \in C \to (1^{st} (c) Walks (G) 2^{nd} (c) \land 2^{nd} (c) (0) = 2^{nd} (c) (\|1^{st} (c)\|) \land \|1^{st} (c)\| \in ℕ)$
6		isclwlk	$⊢ 1^{st} (c) ClWalks (G) 2^{nd} (c) \leftrightarrow (1^{st} (c) Walks (G) 2^{nd} (c) \land 2^{nd} (c) (0) = 2^{nd} (c) (\|1^{st} (c)\|))$
7		fvex	$⊢ 1^{st} (c) \in V$
8		breq1	$⊢ f = 1^{st} (c) \to (f ClWalks (G) 2^{nd} (c) \leftrightarrow 1^{st} (c) ClWalks (G) 2^{nd} (c))$
9	7 8	spcev	$⊢ 1^{st} (c) ClWalks (G) 2^{nd} (c) \to \exists f f ClWalks (G) 2^{nd} (c)$
10	6 9	sylbir	$⊢ (1^{st} (c) Walks (G) 2^{nd} (c) \land 2^{nd} (c) (0) = 2^{nd} (c) (\|1^{st} (c)\|)) \to \exists f f ClWalks (G) 2^{nd} (c)$
11	10	3adant3	$⊢ (1^{st} (c) Walks (G) 2^{nd} (c) \land 2^{nd} (c) (0) = 2^{nd} (c) (\|1^{st} (c)\|) \land \|1^{st} (c)\| \in ℕ) \to \exists f f ClWalks (G) 2^{nd} (c)$
12	11	adantl	$⊢ (G \in USHGraph \land (1^{st} (c) Walks (G) 2^{nd} (c) \land 2^{nd} (c) (0) = 2^{nd} (c) (\|1^{st} (c)\|) \land \|1^{st} (c)\| \in ℕ)) \to \exists f f ClWalks (G) 2^{nd} (c)$
13		simpl	$⊢ (G \in USHGraph \land (1^{st} (c) Walks (G) 2^{nd} (c) \land 2^{nd} (c) (0) = 2^{nd} (c) (\|1^{st} (c)\|) \land \|1^{st} (c)\| \in ℕ)) \to G \in USHGraph$
14		eqid	$⊢ Vtx (G) = Vtx (G)$
15	14	wlkpwrd	$⊢ 1^{st} (c) Walks (G) 2^{nd} (c) \to 2^{nd} (c) \in Word Vtx (G)$
16	15	3ad2ant1	$⊢ (1^{st} (c) Walks (G) 2^{nd} (c) \land 2^{nd} (c) (0) = 2^{nd} (c) (\|1^{st} (c)\|) \land \|1^{st} (c)\| \in ℕ) \to 2^{nd} (c) \in Word Vtx (G)$
17	16	adantl	$⊢ (G \in USHGraph \land (1^{st} (c) Walks (G) 2^{nd} (c) \land 2^{nd} (c) (0) = 2^{nd} (c) (\|1^{st} (c)\|) \land \|1^{st} (c)\| \in ℕ)) \to 2^{nd} (c) \in Word Vtx (G)$
18		elnnnn0c	$⊢ \|1^{st} (c)\| \in ℕ \leftrightarrow (\|1^{st} (c)\| \in ℕ_{0} \land 1 \leq \|1^{st} (c)\|)$
19		nn0re	$⊢ \|1^{st} (c)\| \in ℕ_{0} \to \|1^{st} (c)\| \in ℝ$
20		1e2m1	$⊢ 1 = 2 - 1$
21	20	breq1i	$⊢ 1 \leq \|1^{st} (c)\| \leftrightarrow 2 - 1 \leq \|1^{st} (c)\|$
22	21	biimpi	$⊢ 1 \leq \|1^{st} (c)\| \to 2 - 1 \leq \|1^{st} (c)\|$
23		2re	$⊢ 2 \in ℝ$
24		1re	$⊢ 1 \in ℝ$
25		lesubadd	$⊢ (2 \in ℝ \land 1 \in ℝ \land \|1^{st} (c)\| \in ℝ) \to (2 - 1 \leq \|1^{st} (c)\| \leftrightarrow 2 \leq \|1^{st} (c)\| + 1)$
26	23 24 25	mp3an12	$⊢ \|1^{st} (c)\| \in ℝ \to (2 - 1 \leq \|1^{st} (c)\| \leftrightarrow 2 \leq \|1^{st} (c)\| + 1)$
27	22 26	imbitrid	$⊢ \|1^{st} (c)\| \in ℝ \to (1 \leq \|1^{st} (c)\| \to 2 \leq \|1^{st} (c)\| + 1)$
28	19 27	syl	$⊢ \|1^{st} (c)\| \in ℕ_{0} \to (1 \leq \|1^{st} (c)\| \to 2 \leq \|1^{st} (c)\| + 1)$
29	28	adantl	$⊢ (1^{st} (c) Walks (G) 2^{nd} (c) \land \|1^{st} (c)\| \in ℕ_{0}) \to (1 \leq \|1^{st} (c)\| \to 2 \leq \|1^{st} (c)\| + 1)$
30		wlklenvp1	$⊢ 1^{st} (c) Walks (G) 2^{nd} (c) \to \|2^{nd} (c)\| = \|1^{st} (c)\| + 1$
31	30	adantr	$⊢ (1^{st} (c) Walks (G) 2^{nd} (c) \land \|1^{st} (c)\| \in ℕ_{0}) \to \|2^{nd} (c)\| = \|1^{st} (c)\| + 1$
32	31	breq2d	$⊢ (1^{st} (c) Walks (G) 2^{nd} (c) \land \|1^{st} (c)\| \in ℕ_{0}) \to (2 \leq \|2^{nd} (c)\| \leftrightarrow 2 \leq \|1^{st} (c)\| + 1)$
33	29 32	sylibrd	$⊢ (1^{st} (c) Walks (G) 2^{nd} (c) \land \|1^{st} (c)\| \in ℕ_{0}) \to (1 \leq \|1^{st} (c)\| \to 2 \leq \|2^{nd} (c)\|)$
34	33	expimpd	$⊢ 1^{st} (c) Walks (G) 2^{nd} (c) \to ((\|1^{st} (c)\| \in ℕ_{0} \land 1 \leq \|1^{st} (c)\|) \to 2 \leq \|2^{nd} (c)\|)$
35	18 34	biimtrid	$⊢ 1^{st} (c) Walks (G) 2^{nd} (c) \to (\|1^{st} (c)\| \in ℕ \to 2 \leq \|2^{nd} (c)\|)$
36	35	a1d	$⊢ 1^{st} (c) Walks (G) 2^{nd} (c) \to (2^{nd} (c) (0) = 2^{nd} (c) (\|1^{st} (c)\|) \to (\|1^{st} (c)\| \in ℕ \to 2 \leq \|2^{nd} (c)\|))$
37	36	3imp	$⊢ (1^{st} (c) Walks (G) 2^{nd} (c) \land 2^{nd} (c) (0) = 2^{nd} (c) (\|1^{st} (c)\|) \land \|1^{st} (c)\| \in ℕ) \to 2 \leq \|2^{nd} (c)\|$
38	37	adantl	$⊢ (G \in USHGraph \land (1^{st} (c) Walks (G) 2^{nd} (c) \land 2^{nd} (c) (0) = 2^{nd} (c) (\|1^{st} (c)\|) \land \|1^{st} (c)\| \in ℕ)) \to 2 \leq \|2^{nd} (c)\|$
39		eqid	$⊢ iEdg (G) = iEdg (G)$
40	14 39	clwlkclwwlk	$⊢ (G \in USHGraph \land 2^{nd} (c) \in Word Vtx (G) \land 2 \leq \|2^{nd} (c)\|) \to (\exists f f ClWalks (G) 2^{nd} (c) \leftrightarrow (lastS (2^{nd} (c)) = 2^{nd} (c) (0) \land 2^{nd} (c) prefix (\|2^{nd} (c)\| - 1) \in ClWWalks (G)))$
41	13 17 38 40	syl3anc	$⊢ (G \in USHGraph \land (1^{st} (c) Walks (G) 2^{nd} (c) \land 2^{nd} (c) (0) = 2^{nd} (c) (\|1^{st} (c)\|) \land \|1^{st} (c)\| \in ℕ)) \to (\exists f f ClWalks (G) 2^{nd} (c) \leftrightarrow (lastS (2^{nd} (c)) = 2^{nd} (c) (0) \land 2^{nd} (c) prefix (\|2^{nd} (c)\| - 1) \in ClWWalks (G)))$
42	12 41	mpbid	$⊢ (G \in USHGraph \land (1^{st} (c) Walks (G) 2^{nd} (c) \land 2^{nd} (c) (0) = 2^{nd} (c) (\|1^{st} (c)\|) \land \|1^{st} (c)\| \in ℕ)) \to (lastS (2^{nd} (c)) = 2^{nd} (c) (0) \land 2^{nd} (c) prefix (\|2^{nd} (c)\| - 1) \in ClWWalks (G))$
43	5 42	sylan2	$⊢ (G \in USHGraph \land c \in C) \to (lastS (2^{nd} (c)) = 2^{nd} (c) (0) \land 2^{nd} (c) prefix (\|2^{nd} (c)\| - 1) \in ClWWalks (G))$
44	43	simprd	$⊢ (G \in USHGraph \land c \in C) \to 2^{nd} (c) prefix (\|2^{nd} (c)\| - 1) \in ClWWalks (G)$
45	44 2	fmptd	$⊢ G \in USHGraph \to F : C ⟶ ClWWalks (G)$

Metamath Proof Explorer

Theorem clwlkclwwlkf

Proof