Metamath Proof Explorer

Theorem numclwwlk1lem2fo

Description: T is an onto function. (Contributed by Alexander van der Vekens, 20-Sep-2018) (Revised by AV, 29-May-2021) (Proof shortened by AV, 13-Feb-2022) (Revised by AV, 31-Oct-2022)

Ref Expression
Hypotheses extwwlkfab.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
extwwlkfab.c ⊢ 𝐶 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } )
extwwlkfab.f ⊢ 𝐹 = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) )
numclwwlk.t ⊢ 𝑇 = ( 𝑢 ∈ ( 𝑋 𝐶 𝑁 ) ↦ ⟨ ( 𝑢 prefix ( 𝑁 − 2 ) ) , ( 𝑢 ‘ ( 𝑁 − 1 ) ) ⟩ )
Assertion numclwwlk1lem2fo ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → 𝑇 : ( 𝑋 𝐶 𝑁 ) –onto→ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 extwwlkfab.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 extwwlkfab.c ⊢ 𝐶 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } )
3 extwwlkfab.f ⊢ 𝐹 = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) )
4 numclwwlk.t ⊢ 𝑇 = ( 𝑢 ∈ ( 𝑋 𝐶 𝑁 ) ↦ ⟨ ( 𝑢 prefix ( 𝑁 − 2 ) ) , ( 𝑢 ‘ ( 𝑁 − 1 ) ) ⟩ )
5 1 2 3 4 numclwwlk1lem2f ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → 𝑇 : ( 𝑋 𝐶 𝑁 ) ⟶ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) )
6 elxp ⊢ ( 𝑝 ∈ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) ↔ ∃ 𝑎 ∃ 𝑏 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ) )
7 1 2 3 numclwwlk1lem2foa ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) → ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ∈ ( 𝑋 𝐶 𝑁 ) ) )
8 7 com12 ⊢ ( ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) → ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ∈ ( 𝑋 𝐶 𝑁 ) ) )
9 8 adantl ⊢ ( ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ) → ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ∈ ( 𝑋 𝐶 𝑁 ) ) )
10 9 imp ⊢ ( ( ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ) ∧ ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ∈ ( 𝑋 𝐶 𝑁 ) )
11 simpl ⊢ ( ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ∈ ( 𝑋 𝐶 𝑁 ) ∧ ( ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ) ∧ ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ) → ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ∈ ( 𝑋 𝐶 𝑁 ) )
12 fveq2 ⊢ ( 𝑥 = ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) → ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ) )
13 12 eqeq2d ⊢ ( 𝑥 = ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) → ( 𝑝 = ( 𝑇 ‘ 𝑥 ) ↔ 𝑝 = ( 𝑇 ‘ ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ) ) )
14 1 2 3 4 numclwwlk1lem2fv ⊢ ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ∈ ( 𝑋 𝐶 𝑁 ) → ( 𝑇 ‘ ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ) = ⟨ ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) prefix ( 𝑁 − 2 ) ) , ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ‘ ( 𝑁 − 1 ) ) ⟩ )
15 14 adantr ⊢ ( ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ∈ ( 𝑋 𝐶 𝑁 ) ∧ ( ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ) ∧ ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ) → ( 𝑇 ‘ ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ) = ⟨ ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) prefix ( 𝑁 − 2 ) ) , ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ‘ ( 𝑁 − 1 ) ) ⟩ )
16 15 eqeq2d ⊢ ( ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ∈ ( 𝑋 𝐶 𝑁 ) ∧ ( ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ) ∧ ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ) → ( 𝑝 = ( 𝑇 ‘ ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ) ↔ 𝑝 = ⟨ ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) prefix ( 𝑁 − 2 ) ) , ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ‘ ( 𝑁 − 1 ) ) ⟩ ) )
17 13 16 sylan9bbr ⊢ ( ( ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ∈ ( 𝑋 𝐶 𝑁 ) ∧ ( ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ) ∧ ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ) ∧ 𝑥 = ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ) → ( 𝑝 = ( 𝑇 ‘ 𝑥 ) ↔ 𝑝 = ⟨ ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) prefix ( 𝑁 − 2 ) ) , ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ‘ ( 𝑁 − 1 ) ) ⟩ ) )
18 simprll ⊢ ( ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ∈ ( 𝑋 𝐶 𝑁 ) ∧ ( ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ) ∧ ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ) → 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ )
19 1 nbgrisvtx ⊢ ( 𝑏 ∈ ( 𝐺 NeighbVtx 𝑋 ) → 𝑏 ∈ 𝑉 )
20 3 eleq2i ⊢ ( 𝑎 ∈ 𝐹 ↔ 𝑎 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) )
21 uz3m2nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 − 2 ) ∈ ℕ )
22 21 nnne0d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 − 2 ) ≠ 0 )
23 22 3ad2ant3 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑁 − 2 ) ≠ 0 )
24 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
25 1 24 clwwlknonel ⊢ ( ( 𝑁 − 2 ) ≠ 0 → ( 𝑎 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ↔ ( ( 𝑎 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑎 ) − 1 ) ) { ( 𝑎 ‘ 𝑖 ) , ( 𝑎 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑎 ) , ( 𝑎 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ) )
26 23 25 syl ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑎 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ↔ ( ( 𝑎 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑎 ) − 1 ) ) { ( 𝑎 ‘ 𝑖 ) , ( 𝑎 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑎 ) , ( 𝑎 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ) )
27 20 26 syl5bb ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑎 ∈ 𝐹 ↔ ( ( 𝑎 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑎 ) − 1 ) ) { ( 𝑎 ‘ 𝑖 ) , ( 𝑎 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑎 ) , ( 𝑎 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ) )
28 df-3an ⊢ ( ( ( 𝑎 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑎 ) − 1 ) ) { ( 𝑎 ‘ 𝑖 ) , ( 𝑎 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑎 ) , ( 𝑎 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ↔ ( ( ( 𝑎 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑎 ) − 1 ) ) { ( 𝑎 ‘ 𝑖 ) , ( 𝑎 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑎 ) , ( 𝑎 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) )
29 27 28 bitrdi ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑎 ∈ 𝐹 ↔ ( ( ( 𝑎 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑎 ) − 1 ) ) { ( 𝑎 ‘ 𝑖 ) , ( 𝑎 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑎 ) , ( 𝑎 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) ) )
30 simplll ⊢ ( ( ( ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ∧ 𝑏 ∈ 𝑉 ) → 𝑎 ∈ Word 𝑉 )
31 s1cl ⊢ ( 𝑋 ∈ 𝑉 → ⟨“ 𝑋 ”⟩ ∈ Word 𝑉 )
32 31 adantr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ⟨“ 𝑋 ”⟩ ∈ Word 𝑉 )
33 32 adantl ⊢ ( ( ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ⟨“ 𝑋 ”⟩ ∈ Word 𝑉 )
34 33 adantr ⊢ ( ( ( ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ∧ 𝑏 ∈ 𝑉 ) → ⟨“ 𝑋 ”⟩ ∈ Word 𝑉 )
35 s1cl ⊢ ( 𝑏 ∈ 𝑉 → ⟨“ 𝑏 ”⟩ ∈ Word 𝑉 )
36 35 adantl ⊢ ( ( ( ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ∧ 𝑏 ∈ 𝑉 ) → ⟨“ 𝑏 ”⟩ ∈ Word 𝑉 )
37 ccatass ⊢ ( ( 𝑎 ∈ Word 𝑉 ∧ ⟨“ 𝑋 ”⟩ ∈ Word 𝑉 ∧ ⟨“ 𝑏 ”⟩ ∈ Word 𝑉 ) → ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) = ( 𝑎 ++ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑏 ”⟩ ) ) )
38 37 oveq1d ⊢ ( ( 𝑎 ∈ Word 𝑉 ∧ ⟨“ 𝑋 ”⟩ ∈ Word 𝑉 ∧ ⟨“ 𝑏 ”⟩ ∈ Word 𝑉 ) → ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) prefix ( 𝑁 − 2 ) ) = ( ( 𝑎 ++ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑏 ”⟩ ) ) prefix ( 𝑁 − 2 ) ) )
39 30 34 36 38 syl3anc ⊢ ( ( ( ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ∧ 𝑏 ∈ 𝑉 ) → ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) prefix ( 𝑁 − 2 ) ) = ( ( 𝑎 ++ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑏 ”⟩ ) ) prefix ( 𝑁 − 2 ) ) )
40 ccatcl ⊢ ( ( ⟨“ 𝑋 ”⟩ ∈ Word 𝑉 ∧ ⟨“ 𝑏 ”⟩ ∈ Word 𝑉 ) → ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑏 ”⟩ ) ∈ Word 𝑉 )
41 33 35 40 syl2an ⊢ ( ( ( ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ∧ 𝑏 ∈ 𝑉 ) → ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑏 ”⟩ ) ∈ Word 𝑉 )
42 simpr ⊢ ( ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) → ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) )
43 42 eqcomd ⊢ ( ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) → ( 𝑁 − 2 ) = ( ♯ ‘ 𝑎 ) )
44 43 adantr ⊢ ( ( ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( 𝑁 − 2 ) = ( ♯ ‘ 𝑎 ) )
45 44 adantr ⊢ ( ( ( ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ∧ 𝑏 ∈ 𝑉 ) → ( 𝑁 − 2 ) = ( ♯ ‘ 𝑎 ) )
46 pfxccatid ⊢ ( ( 𝑎 ∈ Word 𝑉 ∧ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑏 ”⟩ ) ∈ Word 𝑉 ∧ ( 𝑁 − 2 ) = ( ♯ ‘ 𝑎 ) ) → ( ( 𝑎 ++ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑏 ”⟩ ) ) prefix ( 𝑁 − 2 ) ) = 𝑎 )
47 30 41 45 46 syl3anc ⊢ ( ( ( ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ∧ 𝑏 ∈ 𝑉 ) → ( ( 𝑎 ++ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑏 ”⟩ ) ) prefix ( 𝑁 − 2 ) ) = 𝑎 )
48 39 47 eqtr2d ⊢ ( ( ( ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ∧ 𝑏 ∈ 𝑉 ) → 𝑎 = ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) prefix ( 𝑁 − 2 ) ) )
49 1e2m1 ⊢ 1 = ( 2 − 1 )
50 49 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 1 = ( 2 − 1 ) )
51 50 oveq2d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 − 1 ) = ( 𝑁 − ( 2 − 1 ) ) )
52 eluzelcn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℂ )
53 2cnd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 2 ∈ ℂ )
54 1cnd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 1 ∈ ℂ )
55 52 53 54 subsubd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 − ( 2 − 1 ) ) = ( ( 𝑁 − 2 ) + 1 ) )
56 51 55 eqtrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 − 1 ) = ( ( 𝑁 − 2 ) + 1 ) )
57 56 adantl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑁 − 1 ) = ( ( 𝑁 − 2 ) + 1 ) )
58 57 adantl ⊢ ( ( ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( 𝑁 − 1 ) = ( ( 𝑁 − 2 ) + 1 ) )
59 58 adantr ⊢ ( ( ( ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ∧ 𝑏 ∈ 𝑉 ) → ( 𝑁 − 1 ) = ( ( 𝑁 − 2 ) + 1 ) )
60 59 fveq2d ⊢ ( ( ( ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ∧ 𝑏 ∈ 𝑉 ) → ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ‘ ( 𝑁 − 1 ) ) = ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ‘ ( ( 𝑁 − 2 ) + 1 ) ) )
61 simpll ⊢ ( ( ( ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ∧ 𝑏 ∈ 𝑉 ) → ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) )
62 simprl ⊢ ( ( ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → 𝑋 ∈ 𝑉 )
63 62 anim1i ⊢ ( ( ( ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ∧ 𝑏 ∈ 𝑉 ) → ( 𝑋 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) )
64 ccatw2s1p2 ⊢ ( ( ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ‘ ( ( 𝑁 − 2 ) + 1 ) ) = 𝑏 )
65 61 63 64 syl2anc ⊢ ( ( ( ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ∧ 𝑏 ∈ 𝑉 ) → ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ‘ ( ( 𝑁 − 2 ) + 1 ) ) = 𝑏 )
66 60 65 eqtr2d ⊢ ( ( ( ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ∧ 𝑏 ∈ 𝑉 ) → 𝑏 = ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ‘ ( 𝑁 − 1 ) ) )
67 48 66 opeq12d ⊢ ( ( ( ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ∧ 𝑏 ∈ 𝑉 ) → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) prefix ( 𝑁 − 2 ) ) , ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ‘ ( 𝑁 − 1 ) ) ⟩ )
68 67 exp31 ⊢ ( ( 𝑎 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑏 ∈ 𝑉 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) prefix ( 𝑁 − 2 ) ) , ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ‘ ( 𝑁 − 1 ) ) ⟩ ) ) )
69 68 3ad2antl1 ⊢ ( ( ( 𝑎 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑎 ) − 1 ) ) { ( 𝑎 ‘ 𝑖 ) , ( 𝑎 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑎 ) , ( 𝑎 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑏 ∈ 𝑉 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) prefix ( 𝑁 − 2 ) ) , ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ‘ ( 𝑁 − 1 ) ) ⟩ ) ) )
70 69 adantr ⊢ ( ( ( ( 𝑎 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑎 ) − 1 ) ) { ( 𝑎 ‘ 𝑖 ) , ( 𝑎 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑎 ) , ( 𝑎 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑏 ∈ 𝑉 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) prefix ( 𝑁 − 2 ) ) , ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ‘ ( 𝑁 − 1 ) ) ⟩ ) ) )
71 70 com12 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( ( ( 𝑎 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑎 ) − 1 ) ) { ( 𝑎 ‘ 𝑖 ) , ( 𝑎 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑎 ) , ( 𝑎 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) → ( 𝑏 ∈ 𝑉 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) prefix ( 𝑁 − 2 ) ) , ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ‘ ( 𝑁 − 1 ) ) ⟩ ) ) )
72 71 3adant1 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( ( ( 𝑎 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑎 ) − 1 ) ) { ( 𝑎 ‘ 𝑖 ) , ( 𝑎 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑎 ) , ( 𝑎 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) → ( 𝑏 ∈ 𝑉 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) prefix ( 𝑁 − 2 ) ) , ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ‘ ( 𝑁 − 1 ) ) ⟩ ) ) )
73 29 72 sylbid ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑎 ∈ 𝐹 → ( 𝑏 ∈ 𝑉 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) prefix ( 𝑁 − 2 ) ) , ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ‘ ( 𝑁 − 1 ) ) ⟩ ) ) )
74 73 com23 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑏 ∈ 𝑉 → ( 𝑎 ∈ 𝐹 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) prefix ( 𝑁 − 2 ) ) , ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ‘ ( 𝑁 − 1 ) ) ⟩ ) ) )
75 19 74 syl5 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑏 ∈ ( 𝐺 NeighbVtx 𝑋 ) → ( 𝑎 ∈ 𝐹 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) prefix ( 𝑁 − 2 ) ) , ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ‘ ( 𝑁 − 1 ) ) ⟩ ) ) )
76 75 com13 ⊢ ( 𝑎 ∈ 𝐹 → ( 𝑏 ∈ ( 𝐺 NeighbVtx 𝑋 ) → ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) prefix ( 𝑁 − 2 ) ) , ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ‘ ( 𝑁 − 1 ) ) ⟩ ) ) )
77 76 imp ⊢ ( ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) → ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) prefix ( 𝑁 − 2 ) ) , ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ‘ ( 𝑁 − 1 ) ) ⟩ ) )
78 77 adantl ⊢ ( ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ) → ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) prefix ( 𝑁 − 2 ) ) , ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ‘ ( 𝑁 − 1 ) ) ⟩ ) )
79 78 imp ⊢ ( ( ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ) ∧ ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) prefix ( 𝑁 − 2 ) ) , ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ‘ ( 𝑁 − 1 ) ) ⟩ )
80 79 adantl ⊢ ( ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ∈ ( 𝑋 𝐶 𝑁 ) ∧ ( ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ) ∧ ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ) → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) prefix ( 𝑁 − 2 ) ) , ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ‘ ( 𝑁 − 1 ) ) ⟩ )
81 18 80 eqtrd ⊢ ( ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ∈ ( 𝑋 𝐶 𝑁 ) ∧ ( ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ) ∧ ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ) → 𝑝 = ⟨ ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) prefix ( 𝑁 − 2 ) ) , ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ‘ ( 𝑁 − 1 ) ) ⟩ )
82 11 17 81 rspcedvd ⊢ ( ( ( ( 𝑎 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑏 ”⟩ ) ∈ ( 𝑋 𝐶 𝑁 ) ∧ ( ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ) ∧ ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) ) → ∃ 𝑥 ∈ ( 𝑋 𝐶 𝑁 ) 𝑝 = ( 𝑇 ‘ 𝑥 ) )
83 10 82 mpancom ⊢ ( ( ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ) ∧ ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ∃ 𝑥 ∈ ( 𝑋 𝐶 𝑁 ) 𝑝 = ( 𝑇 ‘ 𝑥 ) )
84 83 ex ⊢ ( ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ) → ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ∃ 𝑥 ∈ ( 𝑋 𝐶 𝑁 ) 𝑝 = ( 𝑇 ‘ 𝑥 ) ) )
85 84 exlimivv ⊢ ( ∃ 𝑎 ∃ 𝑏 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ) → ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ∃ 𝑥 ∈ ( 𝑋 𝐶 𝑁 ) 𝑝 = ( 𝑇 ‘ 𝑥 ) ) )
86 6 85 sylbi ⊢ ( 𝑝 ∈ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) → ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ∃ 𝑥 ∈ ( 𝑋 𝐶 𝑁 ) 𝑝 = ( 𝑇 ‘ 𝑥 ) ) )
87 86 impcom ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ 𝑝 ∈ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) ) → ∃ 𝑥 ∈ ( 𝑋 𝐶 𝑁 ) 𝑝 = ( 𝑇 ‘ 𝑥 ) )
88 87 ralrimiva ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ∀ 𝑝 ∈ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) ∃ 𝑥 ∈ ( 𝑋 𝐶 𝑁 ) 𝑝 = ( 𝑇 ‘ 𝑥 ) )
89 dffo3 ⊢ ( 𝑇 : ( 𝑋 𝐶 𝑁 ) –onto→ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) ↔ ( 𝑇 : ( 𝑋 𝐶 𝑁 ) ⟶ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) ∧ ∀ 𝑝 ∈ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) ∃ 𝑥 ∈ ( 𝑋 𝐶 𝑁 ) 𝑝 = ( 𝑇 ‘ 𝑥 ) ) )
90 5 88 89 sylanbrc ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → 𝑇 : ( 𝑋 𝐶 𝑁 ) –onto→ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) )