Metamath Proof Explorer


Theorem clwwlkfo

Description: Lemma 4 for clwwlkf1o : F is an onto function. (Contributed by Alexander van der Vekens, 29-Sep-2018) (Revised by AV, 26-Apr-2021) (Revised by AV, 1-Nov-2022)

Ref Expression
Hypotheses clwwlkf1o.d 𝐷 = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) }
clwwlkf1o.f 𝐹 = ( 𝑡𝐷 ↦ ( 𝑡 prefix 𝑁 ) )
Assertion clwwlkfo ( 𝑁 ∈ ℕ → 𝐹 : 𝐷onto→ ( 𝑁 ClWWalksN 𝐺 ) )

Proof

Step Hyp Ref Expression
1 clwwlkf1o.d 𝐷 = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( lastS ‘ 𝑤 ) = ( 𝑤 ‘ 0 ) }
2 clwwlkf1o.f 𝐹 = ( 𝑡𝐷 ↦ ( 𝑡 prefix 𝑁 ) )
3 1 2 clwwlkf ( 𝑁 ∈ ℕ → 𝐹 : 𝐷 ⟶ ( 𝑁 ClWWalksN 𝐺 ) )
4 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
5 eqid ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
6 4 5 clwwlknp ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( ( 𝑝 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑝 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑝𝑖 ) , ( 𝑝 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑝 ) , ( 𝑝 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
7 simpr ( ( ( ( 𝑝 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑝 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑝𝑖 ) , ( 𝑝 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑝 ) , ( 𝑝 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ )
8 simpl1 ( ( ( ( 𝑝 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑝 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑝𝑖 ) , ( 𝑝 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑝 ) , ( 𝑝 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝑝 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑝 ) = 𝑁 ) )
9 3simpc ( ( ( 𝑝 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑝 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑝𝑖 ) , ( 𝑝 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑝 ) , ( 𝑝 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑝𝑖 ) , ( 𝑝 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑝 ) , ( 𝑝 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
10 9 adantr ( ( ( ( 𝑝 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑝 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑝𝑖 ) , ( 𝑝 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑝 ) , ( 𝑝 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ 𝑁 ∈ ℕ ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑝𝑖 ) , ( 𝑝 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑝 ) , ( 𝑝 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
11 1 clwwlkel ( ( 𝑁 ∈ ℕ ∧ ( 𝑝 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑝 ) = 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑝𝑖 ) , ( 𝑝 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑝 ) , ( 𝑝 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝑝 ++ ⟨“ ( 𝑝 ‘ 0 ) ”⟩ ) ∈ 𝐷 )
12 7 8 10 11 syl3anc ( ( ( ( 𝑝 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑝 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑝𝑖 ) , ( 𝑝 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑝 ) , ( 𝑝 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝑝 ++ ⟨“ ( 𝑝 ‘ 0 ) ”⟩ ) ∈ 𝐷 )
13 oveq2 ( 𝑁 = ( ♯ ‘ 𝑝 ) → ( ( 𝑝 ++ ⟨“ ( 𝑝 ‘ 0 ) ”⟩ ) prefix 𝑁 ) = ( ( 𝑝 ++ ⟨“ ( 𝑝 ‘ 0 ) ”⟩ ) prefix ( ♯ ‘ 𝑝 ) ) )
14 13 eqcoms ( ( ♯ ‘ 𝑝 ) = 𝑁 → ( ( 𝑝 ++ ⟨“ ( 𝑝 ‘ 0 ) ”⟩ ) prefix 𝑁 ) = ( ( 𝑝 ++ ⟨“ ( 𝑝 ‘ 0 ) ”⟩ ) prefix ( ♯ ‘ 𝑝 ) ) )
15 14 adantl ( ( 𝑝 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑝 ) = 𝑁 ) → ( ( 𝑝 ++ ⟨“ ( 𝑝 ‘ 0 ) ”⟩ ) prefix 𝑁 ) = ( ( 𝑝 ++ ⟨“ ( 𝑝 ‘ 0 ) ”⟩ ) prefix ( ♯ ‘ 𝑝 ) ) )
16 15 3ad2ant1 ( ( ( 𝑝 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑝 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑝𝑖 ) , ( 𝑝 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑝 ) , ( 𝑝 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( 𝑝 ++ ⟨“ ( 𝑝 ‘ 0 ) ”⟩ ) prefix 𝑁 ) = ( ( 𝑝 ++ ⟨“ ( 𝑝 ‘ 0 ) ”⟩ ) prefix ( ♯ ‘ 𝑝 ) ) )
17 16 adantr ( ( ( ( 𝑝 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑝 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑝𝑖 ) , ( 𝑝 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑝 ) , ( 𝑝 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝑝 ++ ⟨“ ( 𝑝 ‘ 0 ) ”⟩ ) prefix 𝑁 ) = ( ( 𝑝 ++ ⟨“ ( 𝑝 ‘ 0 ) ”⟩ ) prefix ( ♯ ‘ 𝑝 ) ) )
18 simpll ( ( ( 𝑝 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑝 ) = 𝑁 ) ∧ 𝑁 ∈ ℕ ) → 𝑝 ∈ Word ( Vtx ‘ 𝐺 ) )
19 fstwrdne0 ( ( 𝑁 ∈ ℕ ∧ ( 𝑝 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑝 ) = 𝑁 ) ) → ( 𝑝 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) )
20 19 ancoms ( ( ( 𝑝 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑝 ) = 𝑁 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑝 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) )
21 20 s1cld ( ( ( 𝑝 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑝 ) = 𝑁 ) ∧ 𝑁 ∈ ℕ ) → ⟨“ ( 𝑝 ‘ 0 ) ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) )
22 18 21 jca ( ( ( 𝑝 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑝 ) = 𝑁 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑝 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ⟨“ ( 𝑝 ‘ 0 ) ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) ) )
23 22 3ad2antl1 ( ( ( ( 𝑝 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑝 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑝𝑖 ) , ( 𝑝 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑝 ) , ( 𝑝 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝑝 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ⟨“ ( 𝑝 ‘ 0 ) ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) ) )
24 pfxccat1 ( ( 𝑝 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ⟨“ ( 𝑝 ‘ 0 ) ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ( 𝑝 ++ ⟨“ ( 𝑝 ‘ 0 ) ”⟩ ) prefix ( ♯ ‘ 𝑝 ) ) = 𝑝 )
25 23 24 syl ( ( ( ( 𝑝 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑝 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑝𝑖 ) , ( 𝑝 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑝 ) , ( 𝑝 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝑝 ++ ⟨“ ( 𝑝 ‘ 0 ) ”⟩ ) prefix ( ♯ ‘ 𝑝 ) ) = 𝑝 )
26 17 25 eqtr2d ( ( ( ( 𝑝 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑝 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑝𝑖 ) , ( 𝑝 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑝 ) , ( 𝑝 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ 𝑁 ∈ ℕ ) → 𝑝 = ( ( 𝑝 ++ ⟨“ ( 𝑝 ‘ 0 ) ”⟩ ) prefix 𝑁 ) )
27 12 26 jca ( ( ( ( 𝑝 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑝 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑝𝑖 ) , ( 𝑝 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑝 ) , ( 𝑝 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝑝 ++ ⟨“ ( 𝑝 ‘ 0 ) ”⟩ ) ∈ 𝐷𝑝 = ( ( 𝑝 ++ ⟨“ ( 𝑝 ‘ 0 ) ”⟩ ) prefix 𝑁 ) ) )
28 27 ex ( ( ( 𝑝 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑝 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑝𝑖 ) , ( 𝑝 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑝 ) , ( 𝑝 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( 𝑁 ∈ ℕ → ( ( 𝑝 ++ ⟨“ ( 𝑝 ‘ 0 ) ”⟩ ) ∈ 𝐷𝑝 = ( ( 𝑝 ++ ⟨“ ( 𝑝 ‘ 0 ) ”⟩ ) prefix 𝑁 ) ) ) )
29 6 28 syl ( 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( 𝑁 ∈ ℕ → ( ( 𝑝 ++ ⟨“ ( 𝑝 ‘ 0 ) ”⟩ ) ∈ 𝐷𝑝 = ( ( 𝑝 ++ ⟨“ ( 𝑝 ‘ 0 ) ”⟩ ) prefix 𝑁 ) ) ) )
30 29 impcom ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ( ( 𝑝 ++ ⟨“ ( 𝑝 ‘ 0 ) ”⟩ ) ∈ 𝐷𝑝 = ( ( 𝑝 ++ ⟨“ ( 𝑝 ‘ 0 ) ”⟩ ) prefix 𝑁 ) ) )
31 oveq1 ( 𝑥 = ( 𝑝 ++ ⟨“ ( 𝑝 ‘ 0 ) ”⟩ ) → ( 𝑥 prefix 𝑁 ) = ( ( 𝑝 ++ ⟨“ ( 𝑝 ‘ 0 ) ”⟩ ) prefix 𝑁 ) )
32 31 rspceeqv ( ( ( 𝑝 ++ ⟨“ ( 𝑝 ‘ 0 ) ”⟩ ) ∈ 𝐷𝑝 = ( ( 𝑝 ++ ⟨“ ( 𝑝 ‘ 0 ) ”⟩ ) prefix 𝑁 ) ) → ∃ 𝑥𝐷 𝑝 = ( 𝑥 prefix 𝑁 ) )
33 30 32 syl ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ∃ 𝑥𝐷 𝑝 = ( 𝑥 prefix 𝑁 ) )
34 1 2 clwwlkfv ( 𝑥𝐷 → ( 𝐹𝑥 ) = ( 𝑥 prefix 𝑁 ) )
35 34 eqeq2d ( 𝑥𝐷 → ( 𝑝 = ( 𝐹𝑥 ) ↔ 𝑝 = ( 𝑥 prefix 𝑁 ) ) )
36 35 adantl ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) ∧ 𝑥𝐷 ) → ( 𝑝 = ( 𝐹𝑥 ) ↔ 𝑝 = ( 𝑥 prefix 𝑁 ) ) )
37 36 rexbidva ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ( ∃ 𝑥𝐷 𝑝 = ( 𝐹𝑥 ) ↔ ∃ 𝑥𝐷 𝑝 = ( 𝑥 prefix 𝑁 ) ) )
38 33 37 mpbird ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ∃ 𝑥𝐷 𝑝 = ( 𝐹𝑥 ) )
39 38 ralrimiva ( 𝑁 ∈ ℕ → ∀ 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∃ 𝑥𝐷 𝑝 = ( 𝐹𝑥 ) )
40 dffo3 ( 𝐹 : 𝐷onto→ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( 𝐹 : 𝐷 ⟶ ( 𝑁 ClWWalksN 𝐺 ) ∧ ∀ 𝑝 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∃ 𝑥𝐷 𝑝 = ( 𝐹𝑥 ) ) )
41 3 39 40 sylanbrc ( 𝑁 ∈ ℕ → 𝐹 : 𝐷onto→ ( 𝑁 ClWWalksN 𝐺 ) )