Metamath Proof Explorer

Theorem numclwlk2lem2f1o

Description: R is a 1-1 onto function. (Contributed by Alexander van der Vekens, 6-Oct-2018) (Revised by AV, 21-Jan-2022) (Proof shortened by AV, 17-Mar-2022) (Revised by AV, 1-Nov-2022)

Ref Expression
Hypotheses numclwwlk.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
numclwwlk.q ⊢ 𝑄 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ℕ ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑣 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑣 ) } )
numclwwlk.h ⊢ 𝐻 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) ≠ 𝑣 } )
numclwwlk.r ⊢ 𝑅 = ( 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ↦ ( 𝑥 prefix ( 𝑁 + 1 ) ) )
Assertion numclwlk2lem2f1o ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → 𝑅 : ( 𝑋 𝐻 ( 𝑁 + 2 ) ) –1-1-onto→ ( 𝑋 𝑄 𝑁 ) )

Proof

Step Hyp Ref Expression
1 numclwwlk.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 numclwwlk.q ⊢ 𝑄 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ℕ ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑣 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑣 ) } )
3 numclwwlk.h ⊢ 𝐻 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) ≠ 𝑣 } )
4 numclwwlk.r ⊢ 𝑅 = ( 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ↦ ( 𝑥 prefix ( 𝑁 + 1 ) ) )
5 eleq1w ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ↔ 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) )
6 fveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝑅 ‘ 𝑦 ) = ( 𝑅 ‘ 𝑥 ) )
7 oveq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 prefix ( 𝑁 + 1 ) ) = ( 𝑥 prefix ( 𝑁 + 1 ) ) )
8 6 7 eqeq12d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑅 ‘ 𝑦 ) = ( 𝑦 prefix ( 𝑁 + 1 ) ) ↔ ( 𝑅 ‘ 𝑥 ) = ( 𝑥 prefix ( 𝑁 + 1 ) ) ) )
9 5 8 imbi12d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) → ( 𝑅 ‘ 𝑦 ) = ( 𝑦 prefix ( 𝑁 + 1 ) ) ) ↔ ( 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) → ( 𝑅 ‘ 𝑥 ) = ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ) )
10 9 imbi2d ⊢ ( 𝑦 = 𝑥 → ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑦 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) → ( 𝑅 ‘ 𝑦 ) = ( 𝑦 prefix ( 𝑁 + 1 ) ) ) ) ↔ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) → ( 𝑅 ‘ 𝑥 ) = ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ) ) )
11 1 2 3 4 numclwlk2lem2fv ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑦 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) → ( 𝑅 ‘ 𝑦 ) = ( 𝑦 prefix ( 𝑁 + 1 ) ) ) )
12 10 11 chvarvv ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) → ( 𝑅 ‘ 𝑥 ) = ( 𝑥 prefix ( 𝑁 + 1 ) ) ) )
13 12 3adant1 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) → ( 𝑅 ‘ 𝑥 ) = ( 𝑥 prefix ( 𝑁 + 1 ) ) ) )
14 13 imp ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) → ( 𝑅 ‘ 𝑥 ) = ( 𝑥 prefix ( 𝑁 + 1 ) ) )
15 1 2 3 4 numclwlk2lem2f ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → 𝑅 : ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ⟶ ( 𝑋 𝑄 𝑁 ) )
16 15 ffvelrnda ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) → ( 𝑅 ‘ 𝑥 ) ∈ ( 𝑋 𝑄 𝑁 ) )
17 14 16 eqeltrrd ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) → ( 𝑥 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑋 𝑄 𝑁 ) )
18 17 ralrimiva ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ∀ 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ( 𝑥 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑋 𝑄 𝑁 ) )
19 1 2 3 numclwwlk2lem1 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑢 ∈ ( 𝑋 𝑄 𝑁 ) → ∃! 𝑣 ∈ 𝑉 ( 𝑢 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) )
20 19 imp ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ 𝑢 ∈ ( 𝑋 𝑄 𝑁 ) ) → ∃! 𝑣 ∈ 𝑉 ( 𝑢 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) )
21 1 2 numclwwlkovq ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑋 𝑄 𝑁 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) } )
22 21 eleq2d ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑢 ∈ ( 𝑋 𝑄 𝑁 ) ↔ 𝑢 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) } ) )
23 22 3adant1 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑢 ∈ ( 𝑋 𝑄 𝑁 ) ↔ 𝑢 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) } ) )
24 fveq1 ⊢ ( 𝑤 = 𝑢 → ( 𝑤 ‘ 0 ) = ( 𝑢 ‘ 0 ) )
25 24 eqeq1d ⊢ ( 𝑤 = 𝑢 → ( ( 𝑤 ‘ 0 ) = 𝑋 ↔ ( 𝑢 ‘ 0 ) = 𝑋 ) )
26 fveq2 ⊢ ( 𝑤 = 𝑢 → ( lastS ‘ 𝑤 ) = ( lastS ‘ 𝑢 ) )
27 26 neeq1d ⊢ ( 𝑤 = 𝑢 → ( ( lastS ‘ 𝑤 ) ≠ 𝑋 ↔ ( lastS ‘ 𝑢 ) ≠ 𝑋 ) )
28 25 27 anbi12d ⊢ ( 𝑤 = 𝑢 → ( ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) ↔ ( ( 𝑢 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑢 ) ≠ 𝑋 ) ) )
29 28 elrab ⊢ ( 𝑢 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑋 ) } ↔ ( 𝑢 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑢 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑢 ) ≠ 𝑋 ) ) )
30 23 29 bitrdi ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑢 ∈ ( 𝑋 𝑄 𝑁 ) ↔ ( 𝑢 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑢 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑢 ) ≠ 𝑋 ) ) ) )
31 wwlknbp1 ⊢ ( 𝑢 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑁 ∈ ℕ0 ∧ 𝑢 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) ) )
32 3simpc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑢 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) ) → ( 𝑢 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) ) )
33 31 32 syl ⊢ ( 𝑢 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑢 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) ) )
34 1 wrdeqi ⊢ Word 𝑉 = Word ( Vtx ‘ 𝐺 )
35 34 eleq2i ⊢ ( 𝑢 ∈ Word 𝑉 ↔ 𝑢 ∈ Word ( Vtx ‘ 𝐺 ) )
36 35 anbi1i ⊢ ( ( 𝑢 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) ) ↔ ( 𝑢 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) ) )
37 33 36 sylibr ⊢ ( 𝑢 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑢 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) ) )
38 simpll ⊢ ( ( ( 𝑢 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → 𝑢 ∈ Word 𝑉 )
39 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
40 2nn ⊢ 2 ∈ ℕ
41 40 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℕ )
42 41 nnzd ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℤ )
43 nn0pzuz ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 2 ∈ ℤ ) → ( 𝑁 + 2 ) ∈ ( ℤ≥ ‘ 2 ) )
44 39 42 43 syl2anc ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 2 ) ∈ ( ℤ≥ ‘ 2 ) )
45 3 numclwwlkovh ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 + 2 ) ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑋 𝐻 ( 𝑁 + 2 ) ) = { 𝑤 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ) } )
46 44 45 sylan2 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑋 𝐻 ( 𝑁 + 2 ) ) = { 𝑤 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ) } )
47 46 eleq2d ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ↔ 𝑥 ∈ { 𝑤 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ) } ) )
48 fveq1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 ‘ 0 ) = ( 𝑥 ‘ 0 ) )
49 48 eqeq1d ⊢ ( 𝑤 = 𝑥 → ( ( 𝑤 ‘ 0 ) = 𝑋 ↔ ( 𝑥 ‘ 0 ) = 𝑋 ) )
50 fveq1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 ‘ ( ( 𝑁 + 2 ) − 2 ) ) = ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) )
51 50 48 neeq12d ⊢ ( 𝑤 = 𝑥 → ( ( 𝑤 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ↔ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) )
52 49 51 anbi12d ⊢ ( 𝑤 = 𝑥 → ( ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ) ↔ ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) ) )
53 52 elrab ⊢ ( 𝑥 ∈ { 𝑤 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑋 ∧ ( 𝑤 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑤 ‘ 0 ) ) } ↔ ( 𝑥 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∧ ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) ) )
54 47 53 bitrdi ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ↔ ( 𝑥 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∧ ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) ) ) )
55 54 3adant1 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ↔ ( 𝑥 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∧ ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) ) ) )
56 55 adantl ⊢ ( ( ( 𝑢 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ↔ ( 𝑥 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∧ ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) ) ) )
57 1 clwwlknbp ⊢ ( 𝑥 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) → ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ) )
58 lencl ⊢ ( 𝑢 ∈ Word 𝑉 → ( ♯ ‘ 𝑢 ) ∈ ℕ0 )
59 simprr ⊢ ( ( ( ( ( ♯ ‘ 𝑢 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) ) ∧ 𝑁 ∈ ℕ ) ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) ) → 𝑥 ∈ Word 𝑉 )
60 df-2 ⊢ 2 = ( 1 + 1 )
61 60 a1i ⊢ ( 𝑁 ∈ ℕ → 2 = ( 1 + 1 ) )
62 61 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 2 ) = ( 𝑁 + ( 1 + 1 ) ) )
63 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
64 1cnd ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℂ )
65 63 64 64 addassd ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 + 1 ) + 1 ) = ( 𝑁 + ( 1 + 1 ) ) )
66 62 65 eqtr4d ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 2 ) = ( ( 𝑁 + 1 ) + 1 ) )
67 66 adantl ⊢ ( ( ( ( ♯ ‘ 𝑢 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 + 2 ) = ( ( 𝑁 + 1 ) + 1 ) )
68 67 eqeq2d ⊢ ( ( ( ( ♯ ‘ 𝑢 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ↔ ( ♯ ‘ 𝑥 ) = ( ( 𝑁 + 1 ) + 1 ) ) )
69 68 biimpcd ⊢ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) → ( ( ( ( ♯ ‘ 𝑢 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ 𝑥 ) = ( ( 𝑁 + 1 ) + 1 ) ) )
70 69 adantr ⊢ ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) → ( ( ( ( ♯ ‘ 𝑢 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ 𝑥 ) = ( ( 𝑁 + 1 ) + 1 ) ) )
71 70 impcom ⊢ ( ( ( ( ( ♯ ‘ 𝑢 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) ) ∧ 𝑁 ∈ ℕ ) ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) ) → ( ♯ ‘ 𝑥 ) = ( ( 𝑁 + 1 ) + 1 ) )
72 oveq1 ⊢ ( ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) → ( ( ♯ ‘ 𝑢 ) + 1 ) = ( ( 𝑁 + 1 ) + 1 ) )
73 72 ad3antlr ⊢ ( ( ( ( ( ♯ ‘ 𝑢 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) ) ∧ 𝑁 ∈ ℕ ) ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) ) → ( ( ♯ ‘ 𝑢 ) + 1 ) = ( ( 𝑁 + 1 ) + 1 ) )
74 71 73 eqtr4d ⊢ ( ( ( ( ( ♯ ‘ 𝑢 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) ) ∧ 𝑁 ∈ ℕ ) ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) ) → ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑢 ) + 1 ) )
75 59 74 jca ⊢ ( ( ( ( ( ♯ ‘ 𝑢 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) ) ∧ 𝑁 ∈ ℕ ) ∧ ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) ) → ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑢 ) + 1 ) ) )
76 75 exp31 ⊢ ( ( ( ♯ ‘ 𝑢 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) ) → ( 𝑁 ∈ ℕ → ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) → ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑢 ) + 1 ) ) ) ) )
77 58 76 sylan ⊢ ( ( 𝑢 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) ) → ( 𝑁 ∈ ℕ → ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) → ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑢 ) + 1 ) ) ) ) )
78 77 com12 ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑢 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) ) → ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) → ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑢 ) + 1 ) ) ) ) )
79 78 3ad2ant3 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( 𝑢 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) ) → ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) → ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑢 ) + 1 ) ) ) ) )
80 79 impcom ⊢ ( ( ( 𝑢 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) → ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑢 ) + 1 ) ) ) )
81 80 com12 ⊢ ( ( ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ∧ 𝑥 ∈ Word 𝑉 ) → ( ( ( 𝑢 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑢 ) + 1 ) ) ) )
82 81 ancoms ⊢ ( ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( 𝑁 + 2 ) ) → ( ( ( 𝑢 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑢 ) + 1 ) ) ) )
83 57 82 syl ⊢ ( 𝑥 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) → ( ( ( 𝑢 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑢 ) + 1 ) ) ) )
84 83 adantr ⊢ ( ( 𝑥 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∧ ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) ) → ( ( ( 𝑢 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑢 ) + 1 ) ) ) )
85 84 com12 ⊢ ( ( ( 𝑢 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( ( 𝑥 ∈ ( ( 𝑁 + 2 ) ClWWalksN 𝐺 ) ∧ ( ( 𝑥 ‘ 0 ) = 𝑋 ∧ ( 𝑥 ‘ ( ( 𝑁 + 2 ) − 2 ) ) ≠ ( 𝑥 ‘ 0 ) ) ) → ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑢 ) + 1 ) ) ) )
86 56 85 sylbid ⊢ ( ( ( 𝑢 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) → ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑢 ) + 1 ) ) ) )
87 86 ralrimiv ⊢ ( ( ( 𝑢 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ∀ 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑢 ) + 1 ) ) )
88 38 87 jca ⊢ ( ( ( 𝑢 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( 𝑢 ∈ Word 𝑉 ∧ ∀ 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑢 ) + 1 ) ) ) )
89 88 ex ⊢ ( ( 𝑢 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) ) → ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑢 ∈ Word 𝑉 ∧ ∀ 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑢 ) + 1 ) ) ) ) )
90 37 89 syl ⊢ ( 𝑢 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑢 ∈ Word 𝑉 ∧ ∀ 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑢 ) + 1 ) ) ) ) )
91 90 adantr ⊢ ( ( 𝑢 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑢 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑢 ) ≠ 𝑋 ) ) → ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑢 ∈ Word 𝑉 ∧ ∀ 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑢 ) + 1 ) ) ) ) )
92 91 imp ⊢ ( ( ( 𝑢 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑢 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑢 ) ≠ 𝑋 ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( 𝑢 ∈ Word 𝑉 ∧ ∀ 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑢 ) + 1 ) ) ) )
93 nfcv ⊢ Ⅎ 𝑣 𝑋
94 nfmpo1 ⊢ Ⅎ 𝑣 ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) ≠ 𝑣 } )
95 3 94 nfcxfr ⊢ Ⅎ 𝑣 𝐻
96 nfcv ⊢ Ⅎ 𝑣 ( 𝑁 + 2 )
97 93 95 96 nfov ⊢ Ⅎ 𝑣 ( 𝑋 𝐻 ( 𝑁 + 2 ) )
98 97 reuccatpfxs1 ⊢ ( ( 𝑢 ∈ Word 𝑉 ∧ ∀ 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑢 ) + 1 ) ) ) → ( ∃! 𝑣 ∈ 𝑉 ( 𝑢 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) → ∃! 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) 𝑢 = ( 𝑥 prefix ( ♯ ‘ 𝑢 ) ) ) )
99 92 98 syl ⊢ ( ( ( 𝑢 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑢 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑢 ) ≠ 𝑋 ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) → ( ∃! 𝑣 ∈ 𝑉 ( 𝑢 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) → ∃! 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) 𝑢 = ( 𝑥 prefix ( ♯ ‘ 𝑢 ) ) ) )
100 99 imp ⊢ ( ( ( ( 𝑢 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑢 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑢 ) ≠ 𝑋 ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) ∧ ∃! 𝑣 ∈ 𝑉 ( 𝑢 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) → ∃! 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) 𝑢 = ( 𝑥 prefix ( ♯ ‘ 𝑢 ) ) )
101 31 simp3d ⊢ ( 𝑢 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ♯ ‘ 𝑢 ) = ( 𝑁 + 1 ) )
102 101 eqcomd ⊢ ( 𝑢 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑁 + 1 ) = ( ♯ ‘ 𝑢 ) )
103 102 ad4antr ⊢ ( ( ( ( ( 𝑢 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑢 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑢 ) ≠ 𝑋 ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) ∧ ∃! 𝑣 ∈ 𝑉 ( 𝑢 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) ∧ 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) → ( 𝑁 + 1 ) = ( ♯ ‘ 𝑢 ) )
104 103 oveq2d ⊢ ( ( ( ( ( 𝑢 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑢 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑢 ) ≠ 𝑋 ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) ∧ ∃! 𝑣 ∈ 𝑉 ( 𝑢 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) ∧ 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) → ( 𝑥 prefix ( 𝑁 + 1 ) ) = ( 𝑥 prefix ( ♯ ‘ 𝑢 ) ) )
105 104 eqeq2d ⊢ ( ( ( ( ( 𝑢 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑢 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑢 ) ≠ 𝑋 ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) ∧ ∃! 𝑣 ∈ 𝑉 ( 𝑢 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) ∧ 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) → ( 𝑢 = ( 𝑥 prefix ( 𝑁 + 1 ) ) ↔ 𝑢 = ( 𝑥 prefix ( ♯ ‘ 𝑢 ) ) ) )
106 105 reubidva ⊢ ( ( ( ( 𝑢 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑢 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑢 ) ≠ 𝑋 ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) ∧ ∃! 𝑣 ∈ 𝑉 ( 𝑢 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) → ( ∃! 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) 𝑢 = ( 𝑥 prefix ( 𝑁 + 1 ) ) ↔ ∃! 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) 𝑢 = ( 𝑥 prefix ( ♯ ‘ 𝑢 ) ) ) )
107 100 106 mpbird ⊢ ( ( ( ( 𝑢 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑢 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑢 ) ≠ 𝑋 ) ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ) ∧ ∃! 𝑣 ∈ 𝑉 ( 𝑢 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) → ∃! 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) 𝑢 = ( 𝑥 prefix ( 𝑁 + 1 ) ) )
108 107 exp31 ⊢ ( ( 𝑢 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑢 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑢 ) ≠ 𝑋 ) ) → ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ∃! 𝑣 ∈ 𝑉 ( 𝑢 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) → ∃! 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) 𝑢 = ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ) )
109 108 com12 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( 𝑢 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑢 ‘ 0 ) = 𝑋 ∧ ( lastS ‘ 𝑢 ) ≠ 𝑋 ) ) → ( ∃! 𝑣 ∈ 𝑉 ( 𝑢 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) → ∃! 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) 𝑢 = ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ) )
110 30 109 sylbid ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑢 ∈ ( 𝑋 𝑄 𝑁 ) → ( ∃! 𝑣 ∈ 𝑉 ( 𝑢 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) → ∃! 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) 𝑢 = ( 𝑥 prefix ( 𝑁 + 1 ) ) ) ) )
111 110 imp ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ 𝑢 ∈ ( 𝑋 𝑄 𝑁 ) ) → ( ∃! 𝑣 ∈ 𝑉 ( 𝑢 ++ ⟨“ 𝑣 ”⟩ ) ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) → ∃! 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) 𝑢 = ( 𝑥 prefix ( 𝑁 + 1 ) ) ) )
112 20 111 mpd ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ 𝑢 ∈ ( 𝑋 𝑄 𝑁 ) ) → ∃! 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) 𝑢 = ( 𝑥 prefix ( 𝑁 + 1 ) ) )
113 112 ralrimiva ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ∀ 𝑢 ∈ ( 𝑋 𝑄 𝑁 ) ∃! 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) 𝑢 = ( 𝑥 prefix ( 𝑁 + 1 ) ) )
114 4 f1ompt ⊢ ( 𝑅 : ( 𝑋 𝐻 ( 𝑁 + 2 ) ) –1-1-onto→ ( 𝑋 𝑄 𝑁 ) ↔ ( ∀ 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ( 𝑥 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑋 𝑄 𝑁 ) ∧ ∀ 𝑢 ∈ ( 𝑋 𝑄 𝑁 ) ∃! 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) 𝑢 = ( 𝑥 prefix ( 𝑁 + 1 ) ) ) )
115 18 113 114 sylanbrc ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → 𝑅 : ( 𝑋 𝐻 ( 𝑁 + 2 ) ) –1-1-onto→ ( 𝑋 𝑄 𝑁 ) )