Metamath Proof Explorer


Theorem clwwlkvbij

Description: There is a bijection between the set of closed walks of a fixed length N on a fixed vertex X represented by walks (as word) and the set of closed walks (as words) of the fixed length N on the fixed vertex X . The difference between these two representations is that in the first case the fixed vertex is repeated at the end of the word, and in the second case it is not. (Contributed by Alexander van der Vekens, 29-Sep-2018) (Revised by AV, 26-Apr-2021) (Revised by AV, 7-Jul-2022) (Proof shortened by AV, 2-Nov-2022)

Ref Expression
Assertion clwwlkvbij ( ( 𝑋𝑉𝑁 ∈ ℕ ) → ∃ 𝑓 𝑓 : { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )

Proof

Step Hyp Ref Expression
1 ovex ( 𝑁 WWalksN 𝐺 ) ∈ V
2 1 mptrabex ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ↦ ( 𝑤 prefix 𝑁 ) ) ∈ V
3 2 resex ( ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ↦ ( 𝑤 prefix 𝑁 ) ) ↾ { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) ∈ V
4 eqid ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ↦ ( 𝑤 prefix 𝑁 ) ) = ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ↦ ( 𝑤 prefix 𝑁 ) )
5 eqid { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } = { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) }
6 5 4 clwwlkf1o ( 𝑁 ∈ ℕ → ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ↦ ( 𝑤 prefix 𝑁 ) ) : { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } –1-1-onto→ ( 𝑁 ClWWalksN 𝐺 ) )
7 fveq1 ( 𝑦 = ( 𝑤 prefix 𝑁 ) → ( 𝑦 ‘ 0 ) = ( ( 𝑤 prefix 𝑁 ) ‘ 0 ) )
8 7 eqeq1d ( 𝑦 = ( 𝑤 prefix 𝑁 ) → ( ( 𝑦 ‘ 0 ) = 𝑋 ↔ ( ( 𝑤 prefix 𝑁 ) ‘ 0 ) = 𝑋 ) )
9 8 3ad2ant3 ( ( 𝑁 ∈ ℕ ∧ 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∧ 𝑦 = ( 𝑤 prefix 𝑁 ) ) → ( ( 𝑦 ‘ 0 ) = 𝑋 ↔ ( ( 𝑤 prefix 𝑁 ) ‘ 0 ) = 𝑋 ) )
10 fveq2 ( 𝑥 = 𝑤 → ( lastS ‘ 𝑥 ) = ( lastS ‘ 𝑤 ) )
11 fveq1 ( 𝑥 = 𝑤 → ( 𝑥 ‘ 0 ) = ( 𝑤 ‘ 0 ) )
12 10 11 eqeq12d ( 𝑥 = 𝑤 → ( ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) ↔ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ) )
13 12 elrab ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ↔ ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ) )
14 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
15 eqid ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
16 14 15 wwlknp ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
17 simpll ( ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) )
18 nnz ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
19 uzid ( 𝑁 ∈ ℤ → 𝑁 ∈ ( ℤ𝑁 ) )
20 peano2uz ( 𝑁 ∈ ( ℤ𝑁 ) → ( 𝑁 + 1 ) ∈ ( ℤ𝑁 ) )
21 18 19 20 3syl ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ( ℤ𝑁 ) )
22 elfz1end ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( 1 ... 𝑁 ) )
23 22 biimpi ( 𝑁 ∈ ℕ → 𝑁 ∈ ( 1 ... 𝑁 ) )
24 fzss2 ( ( 𝑁 + 1 ) ∈ ( ℤ𝑁 ) → ( 1 ... 𝑁 ) ⊆ ( 1 ... ( 𝑁 + 1 ) ) )
25 24 sselda ( ( ( 𝑁 + 1 ) ∈ ( ℤ𝑁 ) ∧ 𝑁 ∈ ( 1 ... 𝑁 ) ) → 𝑁 ∈ ( 1 ... ( 𝑁 + 1 ) ) )
26 21 23 25 syl2anc ( 𝑁 ∈ ℕ → 𝑁 ∈ ( 1 ... ( 𝑁 + 1 ) ) )
27 26 adantl ( ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ( 1 ... ( 𝑁 + 1 ) ) )
28 oveq2 ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) → ( 1 ... ( ♯ ‘ 𝑤 ) ) = ( 1 ... ( 𝑁 + 1 ) ) )
29 28 eleq2d ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) → ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ↔ 𝑁 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) )
30 29 adantl ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) → ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ↔ 𝑁 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) )
31 30 adantr ( ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ↔ 𝑁 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) )
32 27 31 mpbird ( ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) )
33 17 32 jca ( ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ) )
34 33 ex ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) → ( 𝑁 ∈ ℕ → ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ) ) )
35 34 3adant3 ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑤𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( 𝑁 ∈ ℕ → ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ) ) )
36 16 35 syl ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑁 ∈ ℕ → ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ) ) )
37 36 adantr ( ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ) → ( 𝑁 ∈ ℕ → ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ) ) )
38 13 37 sylbi ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } → ( 𝑁 ∈ ℕ → ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ) ) )
39 38 impcom ( ( 𝑁 ∈ ℕ ∧ 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ) → ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ) )
40 pfxfv0 ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ) → ( ( 𝑤 prefix 𝑁 ) ‘ 0 ) = ( 𝑤 ‘ 0 ) )
41 39 40 syl ( ( 𝑁 ∈ ℕ ∧ 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ) → ( ( 𝑤 prefix 𝑁 ) ‘ 0 ) = ( 𝑤 ‘ 0 ) )
42 41 eqeq1d ( ( 𝑁 ∈ ℕ ∧ 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ) → ( ( ( 𝑤 prefix 𝑁 ) ‘ 0 ) = 𝑋 ↔ ( 𝑤 ‘ 0 ) = 𝑋 ) )
43 42 3adant3 ( ( 𝑁 ∈ ℕ ∧ 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∧ 𝑦 = ( 𝑤 prefix 𝑁 ) ) → ( ( ( 𝑤 prefix 𝑁 ) ‘ 0 ) = 𝑋 ↔ ( 𝑤 ‘ 0 ) = 𝑋 ) )
44 9 43 bitrd ( ( 𝑁 ∈ ℕ ∧ 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∧ 𝑦 = ( 𝑤 prefix 𝑁 ) ) → ( ( 𝑦 ‘ 0 ) = 𝑋 ↔ ( 𝑤 ‘ 0 ) = 𝑋 ) )
45 4 6 44 f1oresrab ( 𝑁 ∈ ℕ → ( ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ↦ ( 𝑤 prefix 𝑁 ) ) ↾ { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) : { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } –1-1-onto→ { 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑦 ‘ 0 ) = 𝑋 } )
46 45 adantl ( ( 𝑋𝑉𝑁 ∈ ℕ ) → ( ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ↦ ( 𝑤 prefix 𝑁 ) ) ↾ { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) : { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } –1-1-onto→ { 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑦 ‘ 0 ) = 𝑋 } )
47 clwwlknon ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) = { 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑦 ‘ 0 ) = 𝑋 }
48 47 a1i ( ( 𝑋𝑉𝑁 ∈ ℕ ) → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) = { 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑦 ‘ 0 ) = 𝑋 } )
49 48 f1oeq3d ( ( 𝑋𝑉𝑁 ∈ ℕ ) → ( ( ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ↦ ( 𝑤 prefix 𝑁 ) ) ↾ { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) : { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ↔ ( ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ↦ ( 𝑤 prefix 𝑁 ) ) ↾ { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) : { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } –1-1-onto→ { 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑦 ‘ 0 ) = 𝑋 } ) )
50 46 49 mpbird ( ( 𝑋𝑉𝑁 ∈ ℕ ) → ( ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ↦ ( 𝑤 prefix 𝑁 ) ) ↾ { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) : { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )
51 f1oeq1 ( 𝑓 = ( ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ↦ ( 𝑤 prefix 𝑁 ) ) ↾ { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) → ( 𝑓 : { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ↔ ( ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ↦ ( 𝑤 prefix 𝑁 ) ) ↾ { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) : { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) )
52 51 spcegv ( ( ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ↦ ( 𝑤 prefix 𝑁 ) ) ↾ { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) ∈ V → ( ( ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ↦ ( 𝑤 prefix 𝑁 ) ) ↾ { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ) : { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) → ∃ 𝑓 𝑓 : { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) )
53 3 50 52 mpsyl ( ( 𝑋𝑉𝑁 ∈ ℕ ) → ∃ 𝑓 𝑓 : { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )
54 df-rab { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } = { 𝑤 ∣ ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ) }
55 anass ( ( ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ↔ ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ) )
56 55 bicomi ( ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ) ↔ ( ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) )
57 56 abbii { 𝑤 ∣ ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ) } = { 𝑤 ∣ ( ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) }
58 13 bicomi ( ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ) ↔ 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } )
59 58 anbi1i ( ( ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ↔ ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) )
60 59 abbii { 𝑤 ∣ ( ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } = { 𝑤 ∣ ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) }
61 df-rab { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } = { 𝑤 ∣ ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) }
62 60 61 eqtr4i { 𝑤 ∣ ( ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } = { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 }
63 54 57 62 3eqtri { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } = { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 }
64 f1oeq2 ( { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } = { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } → ( 𝑓 : { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ↔ 𝑓 : { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) )
65 63 64 mp1i ( ( 𝑋𝑉𝑁 ∈ ℕ ) → ( 𝑓 : { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ↔ 𝑓 : { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) )
66 65 exbidv ( ( 𝑋𝑉𝑁 ∈ ℕ ) → ( ∃ 𝑓 𝑓 : { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ↔ ∃ 𝑓 𝑓 : { 𝑤 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑥 ) = ( 𝑥 ‘ 0 ) } ∣ ( 𝑤 ‘ 0 ) = 𝑋 } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) )
67 53 66 mpbird ( ( 𝑋𝑉𝑁 ∈ ℕ ) → ∃ 𝑓 𝑓 : { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } –1-1-onto→ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )