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