Theorem clwlknf1oclwwlknOLD 27410

Description: Obsolete version of clwlknf1oclwwlkn 27408 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 5-Jul-2018.) (Revised by AV, 3-May-2021.) (Revised by AV, 26-May-2022.) (New usage is discouraged.) (Proof modification is discouraged.)

Hypotheses

Ref	Expression
clwlknf1oclwwlknOLD.a	⊢ 𝐴 = (1st ‘𝑐)
clwlknf1oclwwlknOLD.b	⊢ 𝐵 = (2nd ‘𝑐)
clwlknf1oclwwlknOLD.c	⊢ 𝐶 = {𝑤 ∈ (ClWalks‘𝐺) ∣ (♯‘(1st ‘𝑤)) = 𝑁}
clwlknf1oclwwlknOLD.f	⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr ⟨0, (♯‘𝐴)⟩))

Assertion

Ref	Expression
clwlknf1oclwwlknOLD	⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → 𝐹:𝐶–1-1-onto→(𝑁 ClWWalksN 𝐺))

Distinct variable groups:   𝐶,𝑐   𝐺,𝑐,𝑤   𝑤,𝑁,𝑐

Allowed substitution hints:   𝐴(𝑤,𝑐)   𝐵(𝑤,𝑐)   𝐶(𝑤)   𝐹(𝑤,𝑐)

Proof of Theorem clwlknf1oclwwlknOLD

Dummy variables 𝑑 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2797	. . 3 ⊢ (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} ↦ ((2nd ‘𝑐) substr ⟨0, ((♯‘(2nd ‘𝑐)) − 1)⟩)) = (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} ↦ ((2nd ‘𝑐) substr ⟨0, ((♯‘(2nd ‘𝑐)) − 1)⟩))
2		2fveq3 6414	. . . . . . . 8 ⊢ (𝑠 = 𝑤 → (♯‘(1st ‘𝑠)) = (♯‘(1st ‘𝑤)))
3	2	breq2d 4853	. . . . . . 7 ⊢ (𝑠 = 𝑤 → (1 ≤ (♯‘(1st ‘𝑠)) ↔ 1 ≤ (♯‘(1st ‘𝑤))))
4	3	cbvrabv 3381	. . . . . 6 ⊢ {𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑠))} = {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))}
5		fveq2 6409	. . . . . . . 8 ⊢ (𝑑 = 𝑐 → (2nd ‘𝑑) = (2nd ‘𝑐))
6		2fveq3 6414	. . . . . . . . . 10 ⊢ (𝑑 = 𝑐 → (♯‘(2nd ‘𝑑)) = (♯‘(2nd ‘𝑐)))
7	6	oveq1d 6891	. . . . . . . . 9 ⊢ (𝑑 = 𝑐 → ((♯‘(2nd ‘𝑑)) − 1) = ((♯‘(2nd ‘𝑐)) − 1))
8	7	opeq2d 4598	. . . . . . . 8 ⊢ (𝑑 = 𝑐 → ⟨0, ((♯‘(2nd ‘𝑑)) − 1)⟩ = ⟨0, ((♯‘(2nd ‘𝑐)) − 1)⟩)
9	5, 8	oveq12d 6894	. . . . . . 7 ⊢ (𝑑 = 𝑐 → ((2nd ‘𝑑) substr ⟨0, ((♯‘(2nd ‘𝑑)) − 1)⟩) = ((2nd ‘𝑐) substr ⟨0, ((♯‘(2nd ‘𝑐)) − 1)⟩))
10	9	cbvmptv 4941	. . . . . 6 ⊢ (𝑑 ∈ {𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑠))} ↦ ((2nd ‘𝑑) substr ⟨0, ((♯‘(2nd ‘𝑑)) − 1)⟩)) = (𝑐 ∈ {𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑠))} ↦ ((2nd ‘𝑐) substr ⟨0, ((♯‘(2nd ‘𝑐)) − 1)⟩))
11	4, 10	clwlkclwwlkf1oOLD 27300	. . . . 5 ⊢ (𝐺 ∈ USPGraph → (𝑑 ∈ {𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑠))} ↦ ((2nd ‘𝑑) substr ⟨0, ((♯‘(2nd ‘𝑑)) − 1)⟩)):{𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑠))}–1-1-onto→(ClWWalks‘𝐺))
12	11	adantr 473	. . . 4 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → (𝑑 ∈ {𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑠))} ↦ ((2nd ‘𝑑) substr ⟨0, ((♯‘(2nd ‘𝑑)) − 1)⟩)):{𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑠))}–1-1-onto→(ClWWalks‘𝐺))
13		2fveq3 6414	. . . . . . . . . 10 ⊢ (𝑤 = 𝑠 → (♯‘(1st ‘𝑤)) = (♯‘(1st ‘𝑠)))
14	13	breq2d 4853	. . . . . . . . 9 ⊢ (𝑤 = 𝑠 → (1 ≤ (♯‘(1st ‘𝑤)) ↔ 1 ≤ (♯‘(1st ‘𝑠))))
15	14	cbvrabv 3381	. . . . . . . 8 ⊢ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} = {𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑠))}
16	15	mpteq1i 4930	. . . . . . 7 ⊢ (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} ↦ ((2nd ‘𝑐) substr ⟨0, ((♯‘(2nd ‘𝑐)) − 1)⟩)) = (𝑐 ∈ {𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑠))} ↦ ((2nd ‘𝑐) substr ⟨0, ((♯‘(2nd ‘𝑐)) − 1)⟩))
17		fveq2 6409	. . . . . . . . 9 ⊢ (𝑐 = 𝑑 → (2nd ‘𝑐) = (2nd ‘𝑑))
18		2fveq3 6414	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑑 → (♯‘(2nd ‘𝑐)) = (♯‘(2nd ‘𝑑)))
19	18	oveq1d 6891	. . . . . . . . . 10 ⊢ (𝑐 = 𝑑 → ((♯‘(2nd ‘𝑐)) − 1) = ((♯‘(2nd ‘𝑑)) − 1))
20	19	opeq2d 4598	. . . . . . . . 9 ⊢ (𝑐 = 𝑑 → ⟨0, ((♯‘(2nd ‘𝑐)) − 1)⟩ = ⟨0, ((♯‘(2nd ‘𝑑)) − 1)⟩)
21	17, 20	oveq12d 6894	. . . . . . . 8 ⊢ (𝑐 = 𝑑 → ((2nd ‘𝑐) substr ⟨0, ((♯‘(2nd ‘𝑐)) − 1)⟩) = ((2nd ‘𝑑) substr ⟨0, ((♯‘(2nd ‘𝑑)) − 1)⟩))
22	21	cbvmptv 4941	. . . . . . 7 ⊢ (𝑐 ∈ {𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑠))} ↦ ((2nd ‘𝑐) substr ⟨0, ((♯‘(2nd ‘𝑐)) − 1)⟩)) = (𝑑 ∈ {𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑠))} ↦ ((2nd ‘𝑑) substr ⟨0, ((♯‘(2nd ‘𝑑)) − 1)⟩))
23	16, 22	eqtri 2819	. . . . . 6 ⊢ (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} ↦ ((2nd ‘𝑐) substr ⟨0, ((♯‘(2nd ‘𝑐)) − 1)⟩)) = (𝑑 ∈ {𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑠))} ↦ ((2nd ‘𝑑) substr ⟨0, ((♯‘(2nd ‘𝑑)) − 1)⟩))
24	23	a1i 11	. . . . 5 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} ↦ ((2nd ‘𝑐) substr ⟨0, ((♯‘(2nd ‘𝑐)) − 1)⟩)) = (𝑑 ∈ {𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑠))} ↦ ((2nd ‘𝑑) substr ⟨0, ((♯‘(2nd ‘𝑑)) − 1)⟩)))
25	4	eqcomi 2806	. . . . . 6 ⊢ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} = {𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑠))}
26	25	a1i 11	. . . . 5 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} = {𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑠))})
27		eqidd 2798	. . . . 5 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → (ClWWalks‘𝐺) = (ClWWalks‘𝐺))
28	24, 26, 27	f1oeq123d 6349	. . . 4 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → ((𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} ↦ ((2nd ‘𝑐) substr ⟨0, ((♯‘(2nd ‘𝑐)) − 1)⟩)):{𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))}–1-1-onto→(ClWWalks‘𝐺) ↔ (𝑑 ∈ {𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑠))} ↦ ((2nd ‘𝑑) substr ⟨0, ((♯‘(2nd ‘𝑑)) − 1)⟩)):{𝑠 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑠))}–1-1-onto→(ClWWalks‘𝐺)))
29	12, 28	mpbird 249	. . 3 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} ↦ ((2nd ‘𝑐) substr ⟨0, ((♯‘(2nd ‘𝑐)) − 1)⟩)):{𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))}–1-1-onto→(ClWWalks‘𝐺))
30		fveq2 6409	. . . . . 6 ⊢ (𝑠 = ((2nd ‘𝑐) substr ⟨0, ((♯‘(2nd ‘𝑐)) − 1)⟩) → (♯‘𝑠) = (♯‘((2nd ‘𝑐) substr ⟨0, ((♯‘(2nd ‘𝑐)) − 1)⟩)))
31	30	3ad2ant3 1166	. . . . 5 ⊢ (((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) ∧ 𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} ∧ 𝑠 = ((2nd ‘𝑐) substr ⟨0, ((♯‘(2nd ‘𝑐)) − 1)⟩)) → (♯‘𝑠) = (♯‘((2nd ‘𝑐) substr ⟨0, ((♯‘(2nd ‘𝑐)) − 1)⟩)))
32		2fveq3 6414	. . . . . . . . 9 ⊢ (𝑤 = 𝑐 → (♯‘(1st ‘𝑤)) = (♯‘(1st ‘𝑐)))
33	32	breq2d 4853	. . . . . . . 8 ⊢ (𝑤 = 𝑐 → (1 ≤ (♯‘(1st ‘𝑤)) ↔ 1 ≤ (♯‘(1st ‘𝑐))))
34	33	elrab 3554	. . . . . . 7 ⊢ (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} ↔ (𝑐 ∈ (ClWalks‘𝐺) ∧ 1 ≤ (♯‘(1st ‘𝑐))))
35		clwlknf1oclwwlknlem1OLD 27405	. . . . . . 7 ⊢ ((𝑐 ∈ (ClWalks‘𝐺) ∧ 1 ≤ (♯‘(1st ‘𝑐))) → (♯‘((2nd ‘𝑐) substr ⟨0, ((♯‘(2nd ‘𝑐)) − 1)⟩)) = (♯‘(1st ‘𝑐)))
36	34, 35	sylbi 209	. . . . . 6 ⊢ (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} → (♯‘((2nd ‘𝑐) substr ⟨0, ((♯‘(2nd ‘𝑐)) − 1)⟩)) = (♯‘(1st ‘𝑐)))
37	36	3ad2ant2 1165	. . . . 5 ⊢ (((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) ∧ 𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} ∧ 𝑠 = ((2nd ‘𝑐) substr ⟨0, ((♯‘(2nd ‘𝑐)) − 1)⟩)) → (♯‘((2nd ‘𝑐) substr ⟨0, ((♯‘(2nd ‘𝑐)) − 1)⟩)) = (♯‘(1st ‘𝑐)))
38	31, 37	eqtrd 2831	. . . 4 ⊢ (((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) ∧ 𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} ∧ 𝑠 = ((2nd ‘𝑐) substr ⟨0, ((♯‘(2nd ‘𝑐)) − 1)⟩)) → (♯‘𝑠) = (♯‘(1st ‘𝑐)))
39	38	eqeq1d 2799	. . 3 ⊢ (((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) ∧ 𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} ∧ 𝑠 = ((2nd ‘𝑐) substr ⟨0, ((♯‘(2nd ‘𝑐)) − 1)⟩)) → ((♯‘𝑠) = 𝑁 ↔ (♯‘(1st ‘𝑐)) = 𝑁))
40	1, 29, 39	f1oresrab 6619	. 2 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → ((𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} ↦ ((2nd ‘𝑐) substr ⟨0, ((♯‘(2nd ‘𝑐)) − 1)⟩)) ↾ {𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} ∣ (♯‘(1st ‘𝑐)) = 𝑁}):{𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} ∣ (♯‘(1st ‘𝑐)) = 𝑁}–1-1-onto→{𝑠 ∈ (ClWWalks‘𝐺) ∣ (♯‘𝑠) = 𝑁})
41		clwlknf1oclwwlknOLD.a	. . . . 5 ⊢ 𝐴 = (1st ‘𝑐)
42		clwlknf1oclwwlknOLD.b	. . . . 5 ⊢ 𝐵 = (2nd ‘𝑐)
43		clwlknf1oclwwlknOLD.c	. . . . 5 ⊢ 𝐶 = {𝑤 ∈ (ClWalks‘𝐺) ∣ (♯‘(1st ‘𝑤)) = 𝑁}
44		clwlknf1oclwwlknOLD.f	. . . . 5 ⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr ⟨0, (♯‘𝐴)⟩))
45	41, 42, 43, 44	clwlknf1oclwwlknlem3OLD 27409	. . . 4 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → 𝐹 = ((𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} ↦ (𝐵 substr ⟨0, (♯‘𝐴)⟩)) ↾ 𝐶))
46	42	a1i 11	. . . . . . 7 ⊢ (((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) ∧ 𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))}) → 𝐵 = (2nd ‘𝑐))
47		clwlkwlk 27021	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ (ClWalks‘𝐺) → 𝑐 ∈ (Walks‘𝐺))
48		wlkcpr 26870	. . . . . . . . . . . . 13 ⊢ (𝑐 ∈ (Walks‘𝐺) ↔ (1st ‘𝑐)(Walks‘𝐺)(2nd ‘𝑐))
49	41	fveq2i 6412	. . . . . . . . . . . . . 14 ⊢ (♯‘𝐴) = (♯‘(1st ‘𝑐))
50		wlklenvm1 26863	. . . . . . . . . . . . . 14 ⊢ ((1st ‘𝑐)(Walks‘𝐺)(2nd ‘𝑐) → (♯‘(1st ‘𝑐)) = ((♯‘(2nd ‘𝑐)) − 1))
51	49, 50	syl5eq 2843	. . . . . . . . . . . . 13 ⊢ ((1st ‘𝑐)(Walks‘𝐺)(2nd ‘𝑐) → (♯‘𝐴) = ((♯‘(2nd ‘𝑐)) − 1))
52	48, 51	sylbi 209	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ (Walks‘𝐺) → (♯‘𝐴) = ((♯‘(2nd ‘𝑐)) − 1))
53	47, 52	syl 17	. . . . . . . . . . 11 ⊢ (𝑐 ∈ (ClWalks‘𝐺) → (♯‘𝐴) = ((♯‘(2nd ‘𝑐)) − 1))
54	53	adantr 473	. . . . . . . . . 10 ⊢ ((𝑐 ∈ (ClWalks‘𝐺) ∧ 1 ≤ (♯‘(1st ‘𝑐))) → (♯‘𝐴) = ((♯‘(2nd ‘𝑐)) − 1))
55	34, 54	sylbi 209	. . . . . . . . 9 ⊢ (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} → (♯‘𝐴) = ((♯‘(2nd ‘𝑐)) − 1))
56	55	adantl 474	. . . . . . . 8 ⊢ (((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) ∧ 𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))}) → (♯‘𝐴) = ((♯‘(2nd ‘𝑐)) − 1))
57	56	opeq2d 4598	. . . . . . 7 ⊢ (((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) ∧ 𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))}) → ⟨0, (♯‘𝐴)⟩ = ⟨0, ((♯‘(2nd ‘𝑐)) − 1)⟩)
58	46, 57	oveq12d 6894	. . . . . 6 ⊢ (((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) ∧ 𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))}) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) = ((2nd ‘𝑐) substr ⟨0, ((♯‘(2nd ‘𝑐)) − 1)⟩))
59	58	mpteq2dva 4935	. . . . 5 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} ↦ (𝐵 substr ⟨0, (♯‘𝐴)⟩)) = (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} ↦ ((2nd ‘𝑐) substr ⟨0, ((♯‘(2nd ‘𝑐)) − 1)⟩)))
60	32	eqeq1d 2799	. . . . . . . 8 ⊢ (𝑤 = 𝑐 → ((♯‘(1st ‘𝑤)) = 𝑁 ↔ (♯‘(1st ‘𝑐)) = 𝑁))
61	60	cbvrabv 3381	. . . . . . 7 ⊢ {𝑤 ∈ (ClWalks‘𝐺) ∣ (♯‘(1st ‘𝑤)) = 𝑁} = {𝑐 ∈ (ClWalks‘𝐺) ∣ (♯‘(1st ‘𝑐)) = 𝑁}
62		nnge1 11340	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → 1 ≤ 𝑁)
63		breq2 4845	. . . . . . . . . . . 12 ⊢ ((♯‘(1st ‘𝑐)) = 𝑁 → (1 ≤ (♯‘(1st ‘𝑐)) ↔ 1 ≤ 𝑁))
64	62, 63	syl5ibrcom 239	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → ((♯‘(1st ‘𝑐)) = 𝑁 → 1 ≤ (♯‘(1st ‘𝑐))))
65	64	adantl 474	. . . . . . . . . 10 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → ((♯‘(1st ‘𝑐)) = 𝑁 → 1 ≤ (♯‘(1st ‘𝑐))))
66	65	adantr 473	. . . . . . . . 9 ⊢ (((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) ∧ 𝑐 ∈ (ClWalks‘𝐺)) → ((♯‘(1st ‘𝑐)) = 𝑁 → 1 ≤ (♯‘(1st ‘𝑐))))
67	66	pm4.71rd 559	. . . . . . . 8 ⊢ (((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) ∧ 𝑐 ∈ (ClWalks‘𝐺)) → ((♯‘(1st ‘𝑐)) = 𝑁 ↔ (1 ≤ (♯‘(1st ‘𝑐)) ∧ (♯‘(1st ‘𝑐)) = 𝑁)))
68	67	rabbidva 3370	. . . . . . 7 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → {𝑐 ∈ (ClWalks‘𝐺) ∣ (♯‘(1st ‘𝑐)) = 𝑁} = {𝑐 ∈ (ClWalks‘𝐺) ∣ (1 ≤ (♯‘(1st ‘𝑐)) ∧ (♯‘(1st ‘𝑐)) = 𝑁)})
69	61, 68	syl5eq 2843	. . . . . 6 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → {𝑤 ∈ (ClWalks‘𝐺) ∣ (♯‘(1st ‘𝑤)) = 𝑁} = {𝑐 ∈ (ClWalks‘𝐺) ∣ (1 ≤ (♯‘(1st ‘𝑐)) ∧ (♯‘(1st ‘𝑐)) = 𝑁)})
70	34	anbi1i 618	. . . . . . . 8 ⊢ ((𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} ∧ (♯‘(1st ‘𝑐)) = 𝑁) ↔ ((𝑐 ∈ (ClWalks‘𝐺) ∧ 1 ≤ (♯‘(1st ‘𝑐))) ∧ (♯‘(1st ‘𝑐)) = 𝑁))
71		anass 461	. . . . . . . 8 ⊢ (((𝑐 ∈ (ClWalks‘𝐺) ∧ 1 ≤ (♯‘(1st ‘𝑐))) ∧ (♯‘(1st ‘𝑐)) = 𝑁) ↔ (𝑐 ∈ (ClWalks‘𝐺) ∧ (1 ≤ (♯‘(1st ‘𝑐)) ∧ (♯‘(1st ‘𝑐)) = 𝑁)))
72	70, 71	bitri 267	. . . . . . 7 ⊢ ((𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} ∧ (♯‘(1st ‘𝑐)) = 𝑁) ↔ (𝑐 ∈ (ClWalks‘𝐺) ∧ (1 ≤ (♯‘(1st ‘𝑐)) ∧ (♯‘(1st ‘𝑐)) = 𝑁)))
73	72	rabbia2 3369	. . . . . 6 ⊢ {𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} ∣ (♯‘(1st ‘𝑐)) = 𝑁} = {𝑐 ∈ (ClWalks‘𝐺) ∣ (1 ≤ (♯‘(1st ‘𝑐)) ∧ (♯‘(1st ‘𝑐)) = 𝑁)}
74	69, 43, 73	3eqtr4g 2856	. . . . 5 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → 𝐶 = {𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} ∣ (♯‘(1st ‘𝑐)) = 𝑁})
75	59, 74	reseq12d 5599	. . . 4 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → ((𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} ↦ (𝐵 substr ⟨0, (♯‘𝐴)⟩)) ↾ 𝐶) = ((𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} ↦ ((2nd ‘𝑐) substr ⟨0, ((♯‘(2nd ‘𝑐)) − 1)⟩)) ↾ {𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} ∣ (♯‘(1st ‘𝑐)) = 𝑁}))
76	45, 75	eqtrd 2831	. . 3 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → 𝐹 = ((𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} ↦ ((2nd ‘𝑐) substr ⟨0, ((♯‘(2nd ‘𝑐)) − 1)⟩)) ↾ {𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} ∣ (♯‘(1st ‘𝑐)) = 𝑁}))
77		clwlknf1oclwwlknlem2 27406	. . . . 5 ⊢ (𝑁 ∈ ℕ → {𝑤 ∈ (ClWalks‘𝐺) ∣ (♯‘(1st ‘𝑤)) = 𝑁} = {𝑐 ∈ (ClWalks‘𝐺) ∣ (1 ≤ (♯‘(1st ‘𝑐)) ∧ (♯‘(1st ‘𝑐)) = 𝑁)})
78	77	adantl 474	. . . 4 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → {𝑤 ∈ (ClWalks‘𝐺) ∣ (♯‘(1st ‘𝑤)) = 𝑁} = {𝑐 ∈ (ClWalks‘𝐺) ∣ (1 ≤ (♯‘(1st ‘𝑐)) ∧ (♯‘(1st ‘𝑐)) = 𝑁)})
79	78, 43, 73	3eqtr4g 2856	. . 3 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → 𝐶 = {𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} ∣ (♯‘(1st ‘𝑐)) = 𝑁})
80		clwwlkn 27322	. . . 4 ⊢ (𝑁 ClWWalksN 𝐺) = {𝑠 ∈ (ClWWalks‘𝐺) ∣ (♯‘𝑠) = 𝑁}
81	80	a1i 11	. . 3 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → (𝑁 ClWWalksN 𝐺) = {𝑠 ∈ (ClWWalks‘𝐺) ∣ (♯‘𝑠) = 𝑁})
82	76, 79, 81	f1oeq123d 6349	. 2 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → (𝐹:𝐶–1-1-onto→(𝑁 ClWWalksN 𝐺) ↔ ((𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} ↦ ((2nd ‘𝑐) substr ⟨0, ((♯‘(2nd ‘𝑐)) − 1)⟩)) ↾ {𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} ∣ (♯‘(1st ‘𝑐)) = 𝑁}):{𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} ∣ (♯‘(1st ‘𝑐)) = 𝑁}–1-1-onto→{𝑠 ∈ (ClWWalks‘𝐺) ∣ (♯‘𝑠) = 𝑁}))
83	40, 82	mpbird 249	1 ⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → 𝐹:𝐶–1-1-onto→(𝑁 ClWWalksN 𝐺))

Syntax hints:   → wi 4   ∧ wa 385   ∧ w3a 1108   = wceq 1653   ∈ wcel 2157  {crab 3091  ⟨cop 4372   class class class wbr 4841   ↦ cmpt 4920   ↾ cres 5312  –1-1-onto→wf1o 6098  ‘cfv 6099  (class class class)co 6876  1^st c1st 7397  2^nd c2nd 7398  0cc0 10222  1c1 10223   ≤ cle 10362   − cmin 10554  ℕcn 11310  ♯chash 13366   substr csubstr 13661  USPGraphcuspgr 26376  Walkscwlks 26838  ClWalkscclwlks 27016  ClWWalkscclwwlk 27266   ClWWalksN cclwwlkn 27318

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2354  ax-ext 2775  ax-rep 4962  ax-sep 4973  ax-nul 4981  ax-pow 5033  ax-pr 5095  ax-un 7181  ax-cnex 10278  ax-resscn 10279  ax-1cn 10280  ax-icn 10281  ax-addcl 10282  ax-addrcl 10283  ax-mulcl 10284  ax-mulrcl 10285  ax-mulcom 10286  ax-addass 10287  ax-mulass 10288  ax-distr 10289  ax-i2m1 10290  ax-1ne0 10291  ax-1rid 10292  ax-rnegex 10293  ax-rrecex 10294  ax-cnre 10295  ax-pre-lttri 10296  ax-pre-lttrn 10297  ax-pre-ltadd 10298  ax-pre-mulgt0 10299

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-ifp 1087  df-3or 1109  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2590  df-eu 2607  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-ne 2970  df-nel 3073  df-ral 3092  df-rex 3093  df-reu 3094  df-rmo 3095  df-rab 3096  df-v 3385  df-sbc 3632  df-csb 3727  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-pss 3783  df-nul 4114  df-if 4276  df-pw 4349  df-sn 4367  df-pr 4369  df-tp 4371  df-op 4373  df-uni 4627  df-int 4666  df-iun 4710  df-br 4842  df-opab 4904  df-mpt 4921  df-tr 4944  df-id 5218  df-eprel 5223  df-po 5231  df-so 5232  df-fr 5269  df-we 5271  df-xp 5316  df-rel 5317  df-cnv 5318  df-co 5319  df-dm 5320  df-rn 5321  df-res 5322  df-ima 5323  df-pred 5896  df-ord 5942  df-on 5943  df-lim 5944  df-suc 5945  df-iota 6062  df-fun 6101  df-fn 6102  df-f 6103  df-f1 6104  df-fo 6105  df-f1o 6106  df-fv 6107  df-riota 6837  df-ov 6879  df-oprab 6880  df-mpt2 6881  df-om 7298  df-1st 7399  df-2nd 7400  df-wrecs 7643  df-recs 7705  df-rdg 7743  df-1o 7797  df-2o 7798  df-oadd 7801  df-er 7980  df-map 8095  df-pm 8096  df-en 8194  df-dom 8195  df-sdom 8196  df-fin 8197  df-card 9049  df-cda 9276  df-pnf 10363  df-mnf 10364  df-xr 10365  df-ltxr 10366  df-le 10367  df-sub 10556  df-neg 10557  df-nn 11311  df-2 11372  df-n0 11577  df-xnn0 11649  df-z 11663  df-uz 11927  df-rp 12071  df-fz 12577  df-fzo 12717  df-hash 13367  df-word 13531  df-lsw 13579  df-concat 13587  df-s1 13612  df-substr 13662  df-pfx 13711  df-edg 26275  df-uhgr 26285  df-upgr 26309  df-uspgr 26378  df-wlks 26841  df-clwlks 27017  df-clwwlk 27267  df-clwwlkn 27320

This theorem is referenced by:  clwlkssizeeqOLD  27412  clwwlknonclwlknonf1oOLD  27723