This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐺 ) )