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	⊢ 𝐶 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) }
	clwlkclwwlkf.f	⊢ 𝐹 = ( 𝑐 ∈ 𝐶 ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) )
Assertion	clwlkclwwlkf	⊢ ( 𝐺 ∈ USPGraph → 𝐹 : 𝐶 ⟶ ( ClWWalks ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		clwlkclwwlkf.c	⊢ 𝐶 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) }
2		clwlkclwwlkf.f	⊢ 𝐹 = ( 𝑐 ∈ 𝐶 ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) )
3		eqid	⊢ ( 1^st ‘ 𝑐 ) = ( 1^st ‘ 𝑐 )
4		eqid	⊢ ( 2^nd ‘ 𝑐 ) = ( 2^nd ‘ 𝑐 )
5	1 3 4	clwlkclwwlkflem	⊢ ( 𝑐 ∈ 𝐶 → ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) ∧ ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) = ( ( 2^nd ‘ 𝑐 ) ‘ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ℕ ) )
6		isclwlk	⊢ ( ( 1^st ‘ 𝑐 ) ( ClWalks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) ↔ ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) ∧ ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) = ( ( 2^nd ‘ 𝑐 ) ‘ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ) )
7		fvex	⊢ ( 1^st ‘ 𝑐 ) ∈ V
8		breq1	⊢ ( 𝑓 = ( 1^st ‘ 𝑐 ) → ( 𝑓 ( ClWalks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) ↔ ( 1^st ‘ 𝑐 ) ( ClWalks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) ) )
9	7 8	spcev	⊢ ( ( 1^st ‘ 𝑐 ) ( ClWalks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) → ∃ 𝑓 𝑓 ( ClWalks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) )
10	6 9	sylbir	⊢ ( ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) ∧ ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) = ( ( 2^nd ‘ 𝑐 ) ‘ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ) → ∃ 𝑓 𝑓 ( ClWalks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) )
11	10	3adant3	⊢ ( ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) ∧ ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) = ( ( 2^nd ‘ 𝑐 ) ‘ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ℕ ) → ∃ 𝑓 𝑓 ( ClWalks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) )
12	11	adantl	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) ∧ ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) = ( ( 2^nd ‘ 𝑐 ) ‘ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ℕ ) ) → ∃ 𝑓 𝑓 ( ClWalks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) )
13		simpl	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) ∧ ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) = ( ( 2^nd ‘ 𝑐 ) ‘ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ℕ ) ) → 𝐺 ∈ USPGraph )
14		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
15	14	wlkpwrd	⊢ ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) → ( 2^nd ‘ 𝑐 ) ∈ Word ( Vtx ‘ 𝐺 ) )
16	15	3ad2ant1	⊢ ( ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) ∧ ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) = ( ( 2^nd ‘ 𝑐 ) ‘ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ℕ ) → ( 2^nd ‘ 𝑐 ) ∈ Word ( Vtx ‘ 𝐺 ) )
17	16	adantl	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) ∧ ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) = ( ( 2^nd ‘ 𝑐 ) ‘ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ℕ ) ) → ( 2^nd ‘ 𝑐 ) ∈ Word ( Vtx ‘ 𝐺 ) )
18		elnnnn0c	⊢ ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ℕ ↔ ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ℕ₀ ∧ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) )
19		nn0re	⊢ ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ℕ₀ → ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ℝ )
20		1e2m1	⊢ 1 = ( 2 − 1 )
21	20	breq1i	⊢ ( 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ↔ ( 2 − 1 ) ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) )
22	21	biimpi	⊢ ( 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) → ( 2 − 1 ) ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) )
23		2re	⊢ 2 ∈ ℝ
24		1re	⊢ 1 ∈ ℝ
25		lesubadd	⊢ ( ( 2 ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ℝ ) → ( ( 2 − 1 ) ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ↔ 2 ≤ ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) + 1 ) ) )
26	23 24 25	mp3an12	⊢ ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ℝ → ( ( 2 − 1 ) ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ↔ 2 ≤ ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) + 1 ) ) )
27	22 26	imbitrid	⊢ ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ℝ → ( 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) → 2 ≤ ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) + 1 ) ) )
28	19 27	syl	⊢ ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ℕ₀ → ( 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) → 2 ≤ ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) + 1 ) ) )
29	28	adantl	⊢ ( ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ℕ₀ ) → ( 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) → 2 ≤ ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) + 1 ) ) )
30		wlklenvp1	⊢ ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) → ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) = ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) + 1 ) )
31	30	adantr	⊢ ( ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ℕ₀ ) → ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) = ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) + 1 ) )
32	31	breq2d	⊢ ( ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ℕ₀ ) → ( 2 ≤ ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) ↔ 2 ≤ ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) + 1 ) ) )
33	29 32	sylibrd	⊢ ( ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ℕ₀ ) → ( 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) → 2 ≤ ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) ) )
34	33	expimpd	⊢ ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) → ( ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ℕ₀ ∧ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) → 2 ≤ ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) ) )
35	18 34	biimtrid	⊢ ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) → ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ℕ → 2 ≤ ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) ) )
36	35	a1d	⊢ ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) → ( ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) = ( ( 2^nd ‘ 𝑐 ) ‘ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) → ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ℕ → 2 ≤ ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) ) ) )
37	36	3imp	⊢ ( ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) ∧ ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) = ( ( 2^nd ‘ 𝑐 ) ‘ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ℕ ) → 2 ≤ ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) )
38	37	adantl	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) ∧ ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) = ( ( 2^nd ‘ 𝑐 ) ‘ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ℕ ) ) → 2 ≤ ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) )
39		eqid	⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
40	14 39	clwlkclwwlk	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 2^nd ‘ 𝑐 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ 2 ≤ ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) ) → ( ∃ 𝑓 𝑓 ( ClWalks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) ↔ ( ( lastS ‘ ( 2^nd ‘ 𝑐 ) ) = ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) ∧ ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) ∈ ( ClWWalks ‘ 𝐺 ) ) ) )
41	13 17 38 40	syl3anc	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) ∧ ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) = ( ( 2^nd ‘ 𝑐 ) ‘ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ℕ ) ) → ( ∃ 𝑓 𝑓 ( ClWalks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) ↔ ( ( lastS ‘ ( 2^nd ‘ 𝑐 ) ) = ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) ∧ ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) ∈ ( ClWWalks ‘ 𝐺 ) ) ) )
42	12 41	mpbid	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) ∧ ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) = ( ( 2^nd ‘ 𝑐 ) ‘ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ℕ ) ) → ( ( lastS ‘ ( 2^nd ‘ 𝑐 ) ) = ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) ∧ ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) ∈ ( ClWWalks ‘ 𝐺 ) ) )
43	5 42	sylan2	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑐 ∈ 𝐶 ) → ( ( lastS ‘ ( 2^nd ‘ 𝑐 ) ) = ( ( 2^nd ‘ 𝑐 ) ‘ 0 ) ∧ ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) ∈ ( ClWWalks ‘ 𝐺 ) ) )
44	43	simprd	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑐 ∈ 𝐶 ) → ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) ∈ ( ClWWalks ‘ 𝐺 ) )
45	44 2	fmptd	⊢ ( 𝐺 ∈ USPGraph → 𝐹 : 𝐶 ⟶ ( ClWWalks ‘ 𝐺 ) )

Metamath Proof Explorer

Theorem clwlkclwwlkf

Proof