clwlkclwwlkf1

Description: F is a one-to-one function from the nonempty closed walks into the closed walks as words in a simple pseudograph. (Contributed by Alexander van der Vekens, 5-Jul-2018) (Revised by AV, 3-May-2021) (Revised by AV, 29-Oct-2022)

	Ref	Expression
Hypotheses	clwlkclwwlkf.c	⊢ 𝐶 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) }
	clwlkclwwlkf.f	⊢ 𝐹 = ( 𝑐 ∈ 𝐶 ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) )
Assertion	clwlkclwwlkf1	⊢ ( 𝐺 ∈ USPGraph → 𝐹 : 𝐶 –1-1→ ( ClWWalks ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		clwlkclwwlkf.c	⊢ 𝐶 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) }
2		clwlkclwwlkf.f	⊢ 𝐹 = ( 𝑐 ∈ 𝐶 ↦ ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) )
3	1 2	clwlkclwwlkf	⊢ ( 𝐺 ∈ USPGraph → 𝐹 : 𝐶 ⟶ ( ClWWalks ‘ 𝐺 ) )
4		fveq2	⊢ ( 𝑐 = 𝑥 → ( 2^nd ‘ 𝑐 ) = ( 2^nd ‘ 𝑥 ) )
5		2fveq3	⊢ ( 𝑐 = 𝑥 → ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) = ( ♯ ‘ ( 2^nd ‘ 𝑥 ) ) )
6	5	oveq1d	⊢ ( 𝑐 = 𝑥 → ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) = ( ( ♯ ‘ ( 2^nd ‘ 𝑥 ) ) − 1 ) )
7	4 6	oveq12d	⊢ ( 𝑐 = 𝑥 → ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) = ( ( 2^nd ‘ 𝑥 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑥 ) ) − 1 ) ) )
8		id	⊢ ( 𝑥 ∈ 𝐶 → 𝑥 ∈ 𝐶 )
9		ovexd	⊢ ( 𝑥 ∈ 𝐶 → ( ( 2^nd ‘ 𝑥 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑥 ) ) − 1 ) ) ∈ V )
10	2 7 8 9	fvmptd3	⊢ ( 𝑥 ∈ 𝐶 → ( 𝐹 ‘ 𝑥 ) = ( ( 2^nd ‘ 𝑥 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑥 ) ) − 1 ) ) )
11		fveq2	⊢ ( 𝑐 = 𝑦 → ( 2^nd ‘ 𝑐 ) = ( 2^nd ‘ 𝑦 ) )
12		2fveq3	⊢ ( 𝑐 = 𝑦 → ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) = ( ♯ ‘ ( 2^nd ‘ 𝑦 ) ) )
13	12	oveq1d	⊢ ( 𝑐 = 𝑦 → ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) = ( ( ♯ ‘ ( 2^nd ‘ 𝑦 ) ) − 1 ) )
14	11 13	oveq12d	⊢ ( 𝑐 = 𝑦 → ( ( 2^nd ‘ 𝑐 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) − 1 ) ) = ( ( 2^nd ‘ 𝑦 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑦 ) ) − 1 ) ) )
15		id	⊢ ( 𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐶 )
16		ovexd	⊢ ( 𝑦 ∈ 𝐶 → ( ( 2^nd ‘ 𝑦 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑦 ) ) − 1 ) ) ∈ V )
17	2 14 15 16	fvmptd3	⊢ ( 𝑦 ∈ 𝐶 → ( 𝐹 ‘ 𝑦 ) = ( ( 2^nd ‘ 𝑦 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑦 ) ) − 1 ) ) )
18	10 17	eqeqan12d	⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( ( 2^nd ‘ 𝑥 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑥 ) ) − 1 ) ) = ( ( 2^nd ‘ 𝑦 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑦 ) ) − 1 ) ) ) )
19	18	adantl	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( ( 2^nd ‘ 𝑥 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑥 ) ) − 1 ) ) = ( ( 2^nd ‘ 𝑦 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑦 ) ) − 1 ) ) ) )
20		simplrl	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑥 ) ) − 1 ) ) = ( ( 2^nd ‘ 𝑦 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑦 ) ) − 1 ) ) ) → 𝑥 ∈ 𝐶 )
21		simplrr	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑥 ) ) − 1 ) ) = ( ( 2^nd ‘ 𝑦 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑦 ) ) − 1 ) ) ) → 𝑦 ∈ 𝐶 )
22		eqid	⊢ ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑥 )
23		eqid	⊢ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑥 )
24	1 22 23	clwlkclwwlkflem	⊢ ( 𝑥 ∈ 𝐶 → ( ( 1^st ‘ 𝑥 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑥 ) ∧ ( ( 2^nd ‘ 𝑥 ) ‘ 0 ) = ( ( 2^nd ‘ 𝑥 ) ‘ ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) ∈ ℕ ) )
25		wlklenvm1	⊢ ( ( 1^st ‘ 𝑥 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑥 ) → ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) = ( ( ♯ ‘ ( 2^nd ‘ 𝑥 ) ) − 1 ) )
26	25	eqcomd	⊢ ( ( 1^st ‘ 𝑥 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑥 ) → ( ( ♯ ‘ ( 2^nd ‘ 𝑥 ) ) − 1 ) = ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) )
27	26	3ad2ant1	⊢ ( ( ( 1^st ‘ 𝑥 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑥 ) ∧ ( ( 2^nd ‘ 𝑥 ) ‘ 0 ) = ( ( 2^nd ‘ 𝑥 ) ‘ ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) ∈ ℕ ) → ( ( ♯ ‘ ( 2^nd ‘ 𝑥 ) ) − 1 ) = ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) )
28	24 27	syl	⊢ ( 𝑥 ∈ 𝐶 → ( ( ♯ ‘ ( 2^nd ‘ 𝑥 ) ) − 1 ) = ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) )
29	28	adantr	⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) → ( ( ♯ ‘ ( 2^nd ‘ 𝑥 ) ) − 1 ) = ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) )
30	29	oveq2d	⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) → ( ( 2^nd ‘ 𝑥 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑥 ) ) − 1 ) ) = ( ( 2^nd ‘ 𝑥 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) ) )
31		eqid	⊢ ( 1^st ‘ 𝑦 ) = ( 1^st ‘ 𝑦 )
32		eqid	⊢ ( 2^nd ‘ 𝑦 ) = ( 2^nd ‘ 𝑦 )
33	1 31 32	clwlkclwwlkflem	⊢ ( 𝑦 ∈ 𝐶 → ( ( 1^st ‘ 𝑦 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑦 ) ∧ ( ( 2^nd ‘ 𝑦 ) ‘ 0 ) = ( ( 2^nd ‘ 𝑦 ) ‘ ( ♯ ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑦 ) ) ∈ ℕ ) )
34		wlklenvm1	⊢ ( ( 1^st ‘ 𝑦 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑦 ) → ( ♯ ‘ ( 1^st ‘ 𝑦 ) ) = ( ( ♯ ‘ ( 2^nd ‘ 𝑦 ) ) − 1 ) )
35	34	eqcomd	⊢ ( ( 1^st ‘ 𝑦 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑦 ) → ( ( ♯ ‘ ( 2^nd ‘ 𝑦 ) ) − 1 ) = ( ♯ ‘ ( 1^st ‘ 𝑦 ) ) )
36	35	3ad2ant1	⊢ ( ( ( 1^st ‘ 𝑦 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑦 ) ∧ ( ( 2^nd ‘ 𝑦 ) ‘ 0 ) = ( ( 2^nd ‘ 𝑦 ) ‘ ( ♯ ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑦 ) ) ∈ ℕ ) → ( ( ♯ ‘ ( 2^nd ‘ 𝑦 ) ) − 1 ) = ( ♯ ‘ ( 1^st ‘ 𝑦 ) ) )
37	33 36	syl	⊢ ( 𝑦 ∈ 𝐶 → ( ( ♯ ‘ ( 2^nd ‘ 𝑦 ) ) − 1 ) = ( ♯ ‘ ( 1^st ‘ 𝑦 ) ) )
38	37	adantl	⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) → ( ( ♯ ‘ ( 2^nd ‘ 𝑦 ) ) − 1 ) = ( ♯ ‘ ( 1^st ‘ 𝑦 ) ) )
39	38	oveq2d	⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) → ( ( 2^nd ‘ 𝑦 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑦 ) ) − 1 ) ) = ( ( 2^nd ‘ 𝑦 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑦 ) ) ) )
40	30 39	eqeq12d	⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) → ( ( ( 2^nd ‘ 𝑥 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑥 ) ) − 1 ) ) = ( ( 2^nd ‘ 𝑦 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑦 ) ) − 1 ) ) ↔ ( ( 2^nd ‘ 𝑥 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) ) = ( ( 2^nd ‘ 𝑦 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑦 ) ) ) ) )
41	40	adantl	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( ( 2^nd ‘ 𝑥 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑥 ) ) − 1 ) ) = ( ( 2^nd ‘ 𝑦 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑦 ) ) − 1 ) ) ↔ ( ( 2^nd ‘ 𝑥 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) ) = ( ( 2^nd ‘ 𝑦 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑦 ) ) ) ) )
42	41	biimpa	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑥 ) ) − 1 ) ) = ( ( 2^nd ‘ 𝑦 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑦 ) ) − 1 ) ) ) → ( ( 2^nd ‘ 𝑥 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) ) = ( ( 2^nd ‘ 𝑦 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑦 ) ) ) )
43	20 21 42	3jca	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑥 ) ) − 1 ) ) = ( ( 2^nd ‘ 𝑦 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑦 ) ) − 1 ) ) ) → ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ∧ ( ( 2^nd ‘ 𝑥 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) ) = ( ( 2^nd ‘ 𝑦 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑦 ) ) ) ) )
44	1 22 23 31 32	clwlkclwwlkf1lem2	⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ∧ ( ( 2^nd ‘ 𝑥 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) ) = ( ( 2^nd ‘ 𝑦 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑦 ) ) ) ) → ( ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) = ( ♯ ‘ ( 1^st ‘ 𝑦 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) ) ( ( 2^nd ‘ 𝑥 ) ‘ 𝑖 ) = ( ( 2^nd ‘ 𝑦 ) ‘ 𝑖 ) ) )
45		simpl	⊢ ( ( ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) = ( ♯ ‘ ( 1^st ‘ 𝑦 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) ) ( ( 2^nd ‘ 𝑥 ) ‘ 𝑖 ) = ( ( 2^nd ‘ 𝑦 ) ‘ 𝑖 ) ) → ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) = ( ♯ ‘ ( 1^st ‘ 𝑦 ) ) )
46	43 44 45	3syl	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑥 ) ) − 1 ) ) = ( ( 2^nd ‘ 𝑦 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑦 ) ) − 1 ) ) ) → ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) = ( ♯ ‘ ( 1^st ‘ 𝑦 ) ) )
47	1 22 23 31 32	clwlkclwwlkf1lem3	⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ∧ ( ( 2^nd ‘ 𝑥 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) ) = ( ( 2^nd ‘ 𝑦 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑦 ) ) ) ) → ∀ 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) ) ( ( 2^nd ‘ 𝑥 ) ‘ 𝑖 ) = ( ( 2^nd ‘ 𝑦 ) ‘ 𝑖 ) )
48	43 47	syl	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑥 ) ) − 1 ) ) = ( ( 2^nd ‘ 𝑦 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑦 ) ) − 1 ) ) ) → ∀ 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) ) ( ( 2^nd ‘ 𝑥 ) ‘ 𝑖 ) = ( ( 2^nd ‘ 𝑦 ) ‘ 𝑖 ) )
49		simpl	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → 𝐺 ∈ USPGraph )
50		wlkcpr	⊢ ( 𝑥 ∈ ( Walks ‘ 𝐺 ) ↔ ( 1^st ‘ 𝑥 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑥 ) )
51	50	biimpri	⊢ ( ( 1^st ‘ 𝑥 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑥 ) → 𝑥 ∈ ( Walks ‘ 𝐺 ) )
52	51	3ad2ant1	⊢ ( ( ( 1^st ‘ 𝑥 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑥 ) ∧ ( ( 2^nd ‘ 𝑥 ) ‘ 0 ) = ( ( 2^nd ‘ 𝑥 ) ‘ ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) ∈ ℕ ) → 𝑥 ∈ ( Walks ‘ 𝐺 ) )
53	24 52	syl	⊢ ( 𝑥 ∈ 𝐶 → 𝑥 ∈ ( Walks ‘ 𝐺 ) )
54		wlkcpr	⊢ ( 𝑦 ∈ ( Walks ‘ 𝐺 ) ↔ ( 1^st ‘ 𝑦 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑦 ) )
55	54	biimpri	⊢ ( ( 1^st ‘ 𝑦 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑦 ) → 𝑦 ∈ ( Walks ‘ 𝐺 ) )
56	55	3ad2ant1	⊢ ( ( ( 1^st ‘ 𝑦 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑦 ) ∧ ( ( 2^nd ‘ 𝑦 ) ‘ 0 ) = ( ( 2^nd ‘ 𝑦 ) ‘ ( ♯ ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑦 ) ) ∈ ℕ ) → 𝑦 ∈ ( Walks ‘ 𝐺 ) )
57	33 56	syl	⊢ ( 𝑦 ∈ 𝐶 → 𝑦 ∈ ( Walks ‘ 𝐺 ) )
58	53 57	anim12i	⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑦 ∈ ( Walks ‘ 𝐺 ) ) )
59	58	adantl	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑦 ∈ ( Walks ‘ 𝐺 ) ) )
60		eqidd	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) = ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) )
61	49 59 60	3jca	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝐺 ∈ USPGraph ∧ ( 𝑥 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑦 ∈ ( Walks ‘ 𝐺 ) ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) = ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) ) )
62	61	adantr	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑥 ) ) − 1 ) ) = ( ( 2^nd ‘ 𝑦 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑦 ) ) − 1 ) ) ) → ( 𝐺 ∈ USPGraph ∧ ( 𝑥 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑦 ∈ ( Walks ‘ 𝐺 ) ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) = ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) ) )
63		uspgr2wlkeq	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝑥 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑦 ∈ ( Walks ‘ 𝐺 ) ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) = ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) ) → ( 𝑥 = 𝑦 ↔ ( ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) = ( ♯ ‘ ( 1^st ‘ 𝑦 ) ) ∧ ∀ 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) ) ( ( 2^nd ‘ 𝑥 ) ‘ 𝑖 ) = ( ( 2^nd ‘ 𝑦 ) ‘ 𝑖 ) ) ) )
64	62 63	syl	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑥 ) ) − 1 ) ) = ( ( 2^nd ‘ 𝑦 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑦 ) ) − 1 ) ) ) → ( 𝑥 = 𝑦 ↔ ( ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) = ( ♯ ‘ ( 1^st ‘ 𝑦 ) ) ∧ ∀ 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑥 ) ) ) ( ( 2^nd ‘ 𝑥 ) ‘ 𝑖 ) = ( ( 2^nd ‘ 𝑦 ) ‘ 𝑖 ) ) ) )
65	46 48 64	mpbir2and	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑥 ) ) − 1 ) ) = ( ( 2^nd ‘ 𝑦 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑦 ) ) − 1 ) ) ) → 𝑥 = 𝑦 )
66	65	ex	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( ( 2^nd ‘ 𝑥 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑥 ) ) − 1 ) ) = ( ( 2^nd ‘ 𝑦 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝑦 ) ) − 1 ) ) → 𝑥 = 𝑦 ) )
67	19 66	sylbid	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
68	67	ralrimivva	⊢ ( 𝐺 ∈ USPGraph → ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐶 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
69		dff13	⊢ ( 𝐹 : 𝐶 –1-1→ ( ClWWalks ‘ 𝐺 ) ↔ ( 𝐹 : 𝐶 ⟶ ( ClWWalks ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐶 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
70	3 68 69	sylanbrc	⊢ ( 𝐺 ∈ USPGraph → 𝐹 : 𝐶 –1-1→ ( ClWWalks ‘ 𝐺 ) )

Metamath Proof Explorer

Theorem clwlkclwwlkf1

Proof