Metamath Proof Explorer


Theorem clwlkclwwlken

Description: The set of the nonempty closed walks and the set of closed walks as word are equinumerous in a simple pseudograph. (Contributed by AV, 25-May-2022) (Proof shortened by AV, 4-Nov-2022)

Ref Expression
Assertion clwlkclwwlken G USHGraph w ClWalks G | 1 1 st w ClWWalks G

Proof

Step Hyp Ref Expression
1 fvex ClWalks G V
2 1 rabex w ClWalks G | 1 1 st w V
3 fvex ClWWalks G V
4 2fveq3 w = u 1 st w = 1 st u
5 4 breq2d w = u 1 1 st w 1 1 st u
6 5 cbvrabv w ClWalks G | 1 1 st w = u ClWalks G | 1 1 st u
7 fveq2 d = c 2 nd d = 2 nd c
8 2fveq3 d = c 2 nd d = 2 nd c
9 8 oveq1d d = c 2 nd d 1 = 2 nd c 1
10 7 9 oveq12d d = c 2 nd d prefix 2 nd d 1 = 2 nd c prefix 2 nd c 1
11 10 cbvmptv d w ClWalks G | 1 1 st w 2 nd d prefix 2 nd d 1 = c w ClWalks G | 1 1 st w 2 nd c prefix 2 nd c 1
12 6 11 clwlkclwwlkf1o G USHGraph d w ClWalks G | 1 1 st w 2 nd d prefix 2 nd d 1 : w ClWalks G | 1 1 st w 1-1 onto ClWWalks G
13 f1oen2g w ClWalks G | 1 1 st w V ClWWalks G V d w ClWalks G | 1 1 st w 2 nd d prefix 2 nd d 1 : w ClWalks G | 1 1 st w 1-1 onto ClWWalks G w ClWalks G | 1 1 st w ClWWalks G
14 2 3 12 13 mp3an12i G USHGraph w ClWalks G | 1 1 st w ClWWalks G