Metamath Proof Explorer

Theorem clwlknf1oclwwlkn

Description: There is a one-to-one onto function between the set of closed walks as words of length N and the set of closed walks of length N in a simple pseudograph. (Contributed by Alexander van der Vekens, 5-Jul-2018) (Revised by AV, 3-May-2021) (Revised by AV, 1-Nov-2022)

Ref Expression
Hypotheses clwlknf1oclwwlkn.a ⊢A=1st⁡c
clwlknf1oclwwlkn.b ⊢B=2nd⁡c
clwlknf1oclwwlkn.c ⊢C=w∈ClWalks⁡G|1st⁡w=N
clwlknf1oclwwlkn.f ⊢F=c∈C⟼BprefixA
Assertion clwlknf1oclwwlkn ⊢G∈USHGraph∧N∈ℕ→F:C⟶1-1 ontoNClWWalksNG

Proof

Step Hyp Ref Expression
1 clwlknf1oclwwlkn.a ⊢A=1st⁡c
2 clwlknf1oclwwlkn.b ⊢B=2nd⁡c
3 clwlknf1oclwwlkn.c ⊢C=w∈ClWalks⁡G|1st⁡w=N
4 clwlknf1oclwwlkn.f ⊢F=c∈C⟼BprefixA
5 eqid ⊢c∈w∈ClWalks⁡G|1≤1st⁡w⟼2nd⁡cprefix2nd⁡c−1=c∈w∈ClWalks⁡G|1≤1st⁡w⟼2nd⁡cprefix2nd⁡c−1
6 2fveq3 ⊢s=w→1st⁡s=1st⁡w
7 6 breq2d ⊢s=w→1≤1st⁡s↔1≤1st⁡w
8 7 cbvrabv ⊢s∈ClWalks⁡G|1≤1st⁡s=w∈ClWalks⁡G|1≤1st⁡w
9 fveq2 ⊢d=c→2nd⁡d=2nd⁡c
10 2fveq3 ⊢d=c→2nd⁡d=2nd⁡c
11 10 oveq1d ⊢d=c→2nd⁡d−1=2nd⁡c−1
12 9 11 oveq12d ⊢d=c→2nd⁡dprefix2nd⁡d−1=2nd⁡cprefix2nd⁡c−1
13 12 cbvmptv ⊢d∈s∈ClWalks⁡G|1≤1st⁡s⟼2nd⁡dprefix2nd⁡d−1=c∈s∈ClWalks⁡G|1≤1st⁡s⟼2nd⁡cprefix2nd⁡c−1
14 8 13 clwlkclwwlkf1o ⊢G∈USHGraph→d∈s∈ClWalks⁡G|1≤1st⁡s⟼2nd⁡dprefix2nd⁡d−1:s∈ClWalks⁡G|1≤1st⁡s⟶1-1 ontoClWWalks⁡G
15 14 adantr ⊢G∈USHGraph∧N∈ℕ→d∈s∈ClWalks⁡G|1≤1st⁡s⟼2nd⁡dprefix2nd⁡d−1:s∈ClWalks⁡G|1≤1st⁡s⟶1-1 ontoClWWalks⁡G
16 2fveq3 ⊢w=s→1st⁡w=1st⁡s
17 16 breq2d ⊢w=s→1≤1st⁡w↔1≤1st⁡s
18 17 cbvrabv ⊢w∈ClWalks⁡G|1≤1st⁡w=s∈ClWalks⁡G|1≤1st⁡s
19 18 mpteq1i ⊢c∈w∈ClWalks⁡G|1≤1st⁡w⟼2nd⁡cprefix2nd⁡c−1=c∈s∈ClWalks⁡G|1≤1st⁡s⟼2nd⁡cprefix2nd⁡c−1
20 fveq2 ⊢c=d→2nd⁡c=2nd⁡d
21 2fveq3 ⊢c=d→2nd⁡c=2nd⁡d
22 21 oveq1d ⊢c=d→2nd⁡c−1=2nd⁡d−1
23 20 22 oveq12d ⊢c=d→2nd⁡cprefix2nd⁡c−1=2nd⁡dprefix2nd⁡d−1
24 23 cbvmptv ⊢c∈s∈ClWalks⁡G|1≤1st⁡s⟼2nd⁡cprefix2nd⁡c−1=d∈s∈ClWalks⁡G|1≤1st⁡s⟼2nd⁡dprefix2nd⁡d−1
25 19 24 eqtri ⊢c∈w∈ClWalks⁡G|1≤1st⁡w⟼2nd⁡cprefix2nd⁡c−1=d∈s∈ClWalks⁡G|1≤1st⁡s⟼2nd⁡dprefix2nd⁡d−1
26 25 a1i ⊢G∈USHGraph∧N∈ℕ→c∈w∈ClWalks⁡G|1≤1st⁡w⟼2nd⁡cprefix2nd⁡c−1=d∈s∈ClWalks⁡G|1≤1st⁡s⟼2nd⁡dprefix2nd⁡d−1
27 8 eqcomi ⊢w∈ClWalks⁡G|1≤1st⁡w=s∈ClWalks⁡G|1≤1st⁡s
28 27 a1i ⊢G∈USHGraph∧N∈ℕ→w∈ClWalks⁡G|1≤1st⁡w=s∈ClWalks⁡G|1≤1st⁡s
29 eqidd ⊢G∈USHGraph∧N∈ℕ→ClWWalks⁡G=ClWWalks⁡G
30 26 28 29 f1oeq123d ⊢G∈USHGraph∧N∈ℕ→c∈w∈ClWalks⁡G|1≤1st⁡w⟼2nd⁡cprefix2nd⁡c−1:w∈ClWalks⁡G|1≤1st⁡w⟶1-1 ontoClWWalks⁡G↔d∈s∈ClWalks⁡G|1≤1st⁡s⟼2nd⁡dprefix2nd⁡d−1:s∈ClWalks⁡G|1≤1st⁡s⟶1-1 ontoClWWalks⁡G
31 15 30 mpbird ⊢G∈USHGraph∧N∈ℕ→c∈w∈ClWalks⁡G|1≤1st⁡w⟼2nd⁡cprefix2nd⁡c−1:w∈ClWalks⁡G|1≤1st⁡w⟶1-1 ontoClWWalks⁡G
32 fveq2 ⊢s=2nd⁡cprefix2nd⁡c−1→s=2nd⁡cprefix2nd⁡c−1
33 32 3ad2ant3 ⊢G∈USHGraph∧N∈ℕ∧c∈w∈ClWalks⁡G|1≤1st⁡w∧s=2nd⁡cprefix2nd⁡c−1→s=2nd⁡cprefix2nd⁡c−1
34 2fveq3 ⊢w=c→1st⁡w=1st⁡c
35 34 breq2d ⊢w=c→1≤1st⁡w↔1≤1st⁡c
36 35 elrab ⊢c∈w∈ClWalks⁡G|1≤1st⁡w↔c∈ClWalks⁡G∧1≤1st⁡c
37 clwlknf1oclwwlknlem1 ⊢c∈ClWalks⁡G∧1≤1st⁡c→2nd⁡cprefix2nd⁡c−1=1st⁡c
38 36 37 sylbi ⊢c∈w∈ClWalks⁡G|1≤1st⁡w→2nd⁡cprefix2nd⁡c−1=1st⁡c
39 38 3ad2ant2 ⊢G∈USHGraph∧N∈ℕ∧c∈w∈ClWalks⁡G|1≤1st⁡w∧s=2nd⁡cprefix2nd⁡c−1→2nd⁡cprefix2nd⁡c−1=1st⁡c
40 33 39 eqtrd ⊢G∈USHGraph∧N∈ℕ∧c∈w∈ClWalks⁡G|1≤1st⁡w∧s=2nd⁡cprefix2nd⁡c−1→s=1st⁡c
41 40 eqeq1d ⊢G∈USHGraph∧N∈ℕ∧c∈w∈ClWalks⁡G|1≤1st⁡w∧s=2nd⁡cprefix2nd⁡c−1→s=N↔1st⁡c=N
42 5 31 41 f1oresrab ⊢G∈USHGraph∧N∈ℕ→c∈w∈ClWalks⁡G|1≤1st⁡w⟼2nd⁡cprefix2nd⁡c−1↾c∈w∈ClWalks⁡G|1≤1st⁡w|1st⁡c=N:c∈w∈ClWalks⁡G|1≤1st⁡w|1st⁡c=N⟶1-1 ontos∈ClWWalks⁡G|s=N
43 1 2 3 4 clwlknf1oclwwlknlem3 ⊢G∈USHGraph∧N∈ℕ→F=c∈w∈ClWalks⁡G|1≤1st⁡w⟼BprefixA↾C
44 2 a1i ⊢G∈USHGraph∧N∈ℕ∧c∈w∈ClWalks⁡G|1≤1st⁡w→B=2nd⁡c
45 clwlkwlk ⊢c∈ClWalks⁡G→c∈Walks⁡G
46 wlkcpr ⊢c∈Walks⁡G↔1st⁡cWalks⁡G2nd⁡c
47 1 fveq2i ⊢A=1st⁡c
48 wlklenvm1 ⊢1st⁡cWalks⁡G2nd⁡c→1st⁡c=2nd⁡c−1
49 47 48 eqtrid ⊢1st⁡cWalks⁡G2nd⁡c→A=2nd⁡c−1
50 46 49 sylbi ⊢c∈Walks⁡G→A=2nd⁡c−1
51 45 50 syl ⊢c∈ClWalks⁡G→A=2nd⁡c−1
52 51 adantr ⊢c∈ClWalks⁡G∧1≤1st⁡c→A=2nd⁡c−1
53 36 52 sylbi ⊢c∈w∈ClWalks⁡G|1≤1st⁡w→A=2nd⁡c−1
54 53 adantl ⊢G∈USHGraph∧N∈ℕ∧c∈w∈ClWalks⁡G|1≤1st⁡w→A=2nd⁡c−1
55 44 54 oveq12d ⊢G∈USHGraph∧N∈ℕ∧c∈w∈ClWalks⁡G|1≤1st⁡w→BprefixA=2nd⁡cprefix2nd⁡c−1
56 55 mpteq2dva ⊢G∈USHGraph∧N∈ℕ→c∈w∈ClWalks⁡G|1≤1st⁡w⟼BprefixA=c∈w∈ClWalks⁡G|1≤1st⁡w⟼2nd⁡cprefix2nd⁡c−1
57 34 eqeq1d ⊢w=c→1st⁡w=N↔1st⁡c=N
58 57 cbvrabv ⊢w∈ClWalks⁡G|1st⁡w=N=c∈ClWalks⁡G|1st⁡c=N
59 nnge1 ⊢N∈ℕ→1≤N
60 breq2 ⊢1st⁡c=N→1≤1st⁡c↔1≤N
61 59 60 syl5ibrcom ⊢N∈ℕ→1st⁡c=N→1≤1st⁡c
62 61 adantl ⊢G∈USHGraph∧N∈ℕ→1st⁡c=N→1≤1st⁡c
63 62 adantr ⊢G∈USHGraph∧N∈ℕ∧c∈ClWalks⁡G→1st⁡c=N→1≤1st⁡c
64 63 pm4.71rd ⊢G∈USHGraph∧N∈ℕ∧c∈ClWalks⁡G→1st⁡c=N↔1≤1st⁡c∧1st⁡c=N
65 64 rabbidva ⊢G∈USHGraph∧N∈ℕ→c∈ClWalks⁡G|1st⁡c=N=c∈ClWalks⁡G|1≤1st⁡c∧1st⁡c=N
66 58 65 eqtrid ⊢G∈USHGraph∧N∈ℕ→w∈ClWalks⁡G|1st⁡w=N=c∈ClWalks⁡G|1≤1st⁡c∧1st⁡c=N
67 36 anbi1i ⊢c∈w∈ClWalks⁡G|1≤1st⁡w∧1st⁡c=N↔c∈ClWalks⁡G∧1≤1st⁡c∧1st⁡c=N
68 anass ⊢c∈ClWalks⁡G∧1≤1st⁡c∧1st⁡c=N↔c∈ClWalks⁡G∧1≤1st⁡c∧1st⁡c=N
69 67 68 bitri ⊢c∈w∈ClWalks⁡G|1≤1st⁡w∧1st⁡c=N↔c∈ClWalks⁡G∧1≤1st⁡c∧1st⁡c=N
70 69 rabbia2 ⊢c∈w∈ClWalks⁡G|1≤1st⁡w|1st⁡c=N=c∈ClWalks⁡G|1≤1st⁡c∧1st⁡c=N
71 66 3 70 3eqtr4g ⊢G∈USHGraph∧N∈ℕ→C=c∈w∈ClWalks⁡G|1≤1st⁡w|1st⁡c=N
72 56 71 reseq12d ⊢G∈USHGraph∧N∈ℕ→c∈w∈ClWalks⁡G|1≤1st⁡w⟼BprefixA↾C=c∈w∈ClWalks⁡G|1≤1st⁡w⟼2nd⁡cprefix2nd⁡c−1↾c∈w∈ClWalks⁡G|1≤1st⁡w|1st⁡c=N
73 43 72 eqtrd ⊢G∈USHGraph∧N∈ℕ→F=c∈w∈ClWalks⁡G|1≤1st⁡w⟼2nd⁡cprefix2nd⁡c−1↾c∈w∈ClWalks⁡G|1≤1st⁡w|1st⁡c=N
74 clwlknf1oclwwlknlem2 ⊢N∈ℕ→w∈ClWalks⁡G|1st⁡w=N=c∈ClWalks⁡G|1≤1st⁡c∧1st⁡c=N
75 74 adantl ⊢G∈USHGraph∧N∈ℕ→w∈ClWalks⁡G|1st⁡w=N=c∈ClWalks⁡G|1≤1st⁡c∧1st⁡c=N
76 75 3 70 3eqtr4g ⊢G∈USHGraph∧N∈ℕ→C=c∈w∈ClWalks⁡G|1≤1st⁡w|1st⁡c=N
77 clwwlkn ⊢NClWWalksNG=s∈ClWWalks⁡G|s=N
78 77 a1i ⊢G∈USHGraph∧N∈ℕ→NClWWalksNG=s∈ClWWalks⁡G|s=N
79 73 76 78 f1oeq123d ⊢G∈USHGraph∧N∈ℕ→F:C⟶1-1 ontoNClWWalksNG↔c∈w∈ClWalks⁡G|1≤1st⁡w⟼2nd⁡cprefix2nd⁡c−1↾c∈w∈ClWalks⁡G|1≤1st⁡w|1st⁡c=N:c∈w∈ClWalks⁡G|1≤1st⁡w|1st⁡c=N⟶1-1 ontos∈ClWWalks⁡G|s=N
80 42 79 mpbird ⊢G∈USHGraph∧N∈ℕ→F:C⟶1-1 ontoNClWWalksNG