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 ⊢ D = w ∈ N WWalksN G | lastS ⁡ w = w ⁡ 0
clwwlkf1o.f ⊢ F = t ∈ D ⟼ t prefix N
Assertion clwwlkfo ⊢ N ∈ ℕ → F : D ⟶ onto N ClWWalksN G

Proof

Step Hyp Ref Expression
1 clwwlkf1o.d ⊢ D = w ∈ N WWalksN G | lastS ⁡ w = w ⁡ 0
2 clwwlkf1o.f ⊢ F = t ∈ D ⟼ t prefix N
3 1 2 clwwlkf ⊢ N ∈ ℕ → F : D ⟶ N ClWWalksN G
4 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
5 eqid ⊢ Edg ⁡ G = Edg ⁡ G
6 4 5 clwwlknp ⊢ p ∈ N ClWWalksN G → p ∈ Word Vtx ⁡ G ∧ p = N ∧ ∀ i ∈ 0 ..^ N − 1 p ⁡ i p ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ p p ⁡ 0 ∈ Edg ⁡ G
7 simpr ⊢ p ∈ Word Vtx ⁡ G ∧ p = N ∧ ∀ i ∈ 0 ..^ N − 1 p ⁡ i p ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ p p ⁡ 0 ∈ Edg ⁡ G ∧ N ∈ ℕ → N ∈ ℕ
8 simpl1 ⊢ p ∈ Word Vtx ⁡ G ∧ p = N ∧ ∀ i ∈ 0 ..^ N − 1 p ⁡ i p ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ p p ⁡ 0 ∈ Edg ⁡ G ∧ N ∈ ℕ → p ∈ Word Vtx ⁡ G ∧ p = N
9 3simpc ⊢ p ∈ Word Vtx ⁡ G ∧ p = N ∧ ∀ i ∈ 0 ..^ N − 1 p ⁡ i p ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ p p ⁡ 0 ∈ Edg ⁡ G → ∀ i ∈ 0 ..^ N − 1 p ⁡ i p ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ p p ⁡ 0 ∈ Edg ⁡ G
10 9 adantr ⊢ p ∈ Word Vtx ⁡ G ∧ p = N ∧ ∀ i ∈ 0 ..^ N − 1 p ⁡ i p ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ p p ⁡ 0 ∈ Edg ⁡ G ∧ N ∈ ℕ → ∀ i ∈ 0 ..^ N − 1 p ⁡ i p ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ p p ⁡ 0 ∈ Edg ⁡ G
11 1 clwwlkel ⊢ N ∈ ℕ ∧ p ∈ Word Vtx ⁡ G ∧ p = N ∧ ∀ i ∈ 0 ..^ N − 1 p ⁡ i p ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ p p ⁡ 0 ∈ Edg ⁡ G → p ++ ⟨“ p ⁡ 0 ”⟩ ∈ D
12 7 8 10 11 syl3anc ⊢ p ∈ Word Vtx ⁡ G ∧ p = N ∧ ∀ i ∈ 0 ..^ N − 1 p ⁡ i p ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ p p ⁡ 0 ∈ Edg ⁡ G ∧ N ∈ ℕ → p ++ ⟨“ p ⁡ 0 ”⟩ ∈ D
13 oveq2 ⊢ N = p → p ++ ⟨“ p ⁡ 0 ”⟩ prefix N = p ++ ⟨“ p ⁡ 0 ”⟩ prefix p
14 13 eqcoms ⊢ p = N → p ++ ⟨“ p ⁡ 0 ”⟩ prefix N = p ++ ⟨“ p ⁡ 0 ”⟩ prefix p
15 14 adantl ⊢ p ∈ Word Vtx ⁡ G ∧ p = N → p ++ ⟨“ p ⁡ 0 ”⟩ prefix N = p ++ ⟨“ p ⁡ 0 ”⟩ prefix p
16 15 3ad2ant1 ⊢ p ∈ Word Vtx ⁡ G ∧ p = N ∧ ∀ i ∈ 0 ..^ N − 1 p ⁡ i p ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ p p ⁡ 0 ∈ Edg ⁡ G → p ++ ⟨“ p ⁡ 0 ”⟩ prefix N = p ++ ⟨“ p ⁡ 0 ”⟩ prefix p
17 16 adantr ⊢ p ∈ Word Vtx ⁡ G ∧ p = N ∧ ∀ i ∈ 0 ..^ N − 1 p ⁡ i p ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ p p ⁡ 0 ∈ Edg ⁡ G ∧ N ∈ ℕ → p ++ ⟨“ p ⁡ 0 ”⟩ prefix N = p ++ ⟨“ p ⁡ 0 ”⟩ prefix p
18 simpll ⊢ p ∈ Word Vtx ⁡ G ∧ p = N ∧ N ∈ ℕ → p ∈ Word Vtx ⁡ G
19 fstwrdne0 ⊢ N ∈ ℕ ∧ p ∈ Word Vtx ⁡ G ∧ p = N → p ⁡ 0 ∈ Vtx ⁡ G
20 19 ancoms ⊢ p ∈ Word Vtx ⁡ G ∧ p = N ∧ N ∈ ℕ → p ⁡ 0 ∈ Vtx ⁡ G
21 20 s1cld ⊢ p ∈ Word Vtx ⁡ G ∧ p = N ∧ N ∈ ℕ → ⟨“ p ⁡ 0 ”⟩ ∈ Word Vtx ⁡ G
22 18 21 jca ⊢ p ∈ Word Vtx ⁡ G ∧ p = N ∧ N ∈ ℕ → p ∈ Word Vtx ⁡ G ∧ ⟨“ p ⁡ 0 ”⟩ ∈ Word Vtx ⁡ G
23 22 3ad2antl1 ⊢ p ∈ Word Vtx ⁡ G ∧ p = N ∧ ∀ i ∈ 0 ..^ N − 1 p ⁡ i p ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ p p ⁡ 0 ∈ Edg ⁡ G ∧ N ∈ ℕ → p ∈ Word Vtx ⁡ G ∧ ⟨“ p ⁡ 0 ”⟩ ∈ Word Vtx ⁡ G
24 pfxccat1 ⊢ p ∈ Word Vtx ⁡ G ∧ ⟨“ p ⁡ 0 ”⟩ ∈ Word Vtx ⁡ G → p ++ ⟨“ p ⁡ 0 ”⟩ prefix p = p
25 23 24 syl ⊢ p ∈ Word Vtx ⁡ G ∧ p = N ∧ ∀ i ∈ 0 ..^ N − 1 p ⁡ i p ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ p p ⁡ 0 ∈ Edg ⁡ G ∧ N ∈ ℕ → p ++ ⟨“ p ⁡ 0 ”⟩ prefix p = p
26 17 25 eqtr2d ⊢ p ∈ Word Vtx ⁡ G ∧ p = N ∧ ∀ i ∈ 0 ..^ N − 1 p ⁡ i p ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ p p ⁡ 0 ∈ Edg ⁡ G ∧ N ∈ ℕ → p = p ++ ⟨“ p ⁡ 0 ”⟩ prefix N
27 12 26 jca ⊢ p ∈ Word Vtx ⁡ G ∧ p = N ∧ ∀ i ∈ 0 ..^ N − 1 p ⁡ i p ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ p p ⁡ 0 ∈ Edg ⁡ G ∧ N ∈ ℕ → p ++ ⟨“ p ⁡ 0 ”⟩ ∈ D ∧ p = p ++ ⟨“ p ⁡ 0 ”⟩ prefix N
28 27 ex ⊢ p ∈ Word Vtx ⁡ G ∧ p = N ∧ ∀ i ∈ 0 ..^ N − 1 p ⁡ i p ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ p p ⁡ 0 ∈ Edg ⁡ G → N ∈ ℕ → p ++ ⟨“ p ⁡ 0 ”⟩ ∈ D ∧ p = p ++ ⟨“ p ⁡ 0 ”⟩ prefix N
29 6 28 syl ⊢ p ∈ N ClWWalksN G → N ∈ ℕ → p ++ ⟨“ p ⁡ 0 ”⟩ ∈ D ∧ p = p ++ ⟨“ p ⁡ 0 ”⟩ prefix N
30 29 impcom ⊢ N ∈ ℕ ∧ p ∈ N ClWWalksN G → p ++ ⟨“ p ⁡ 0 ”⟩ ∈ D ∧ p = p ++ ⟨“ p ⁡ 0 ”⟩ prefix N
31 oveq1 ⊢ x = p ++ ⟨“ p ⁡ 0 ”⟩ → x prefix N = p ++ ⟨“ p ⁡ 0 ”⟩ prefix N
32 31 rspceeqv ⊢ p ++ ⟨“ p ⁡ 0 ”⟩ ∈ D ∧ p = p ++ ⟨“ p ⁡ 0 ”⟩ prefix N → ∃ x ∈ D p = x prefix N
33 30 32 syl ⊢ N ∈ ℕ ∧ p ∈ N ClWWalksN G → ∃ x ∈ D p = x prefix N
34 1 2 clwwlkfv ⊢ x ∈ D → F ⁡ x = x prefix N
35 34 eqeq2d ⊢ x ∈ D → p = F ⁡ x ↔ p = x prefix N
36 35 adantl ⊢ N ∈ ℕ ∧ p ∈ N ClWWalksN G ∧ x ∈ D → p = F ⁡ x ↔ p = x prefix N
37 36 rexbidva ⊢ N ∈ ℕ ∧ p ∈ N ClWWalksN G → ∃ x ∈ D p = F ⁡ x ↔ ∃ x ∈ D p = x prefix N
38 33 37 mpbird ⊢ N ∈ ℕ ∧ p ∈ N ClWWalksN G → ∃ x ∈ D p = F ⁡ x
39 38 ralrimiva ⊢ N ∈ ℕ → ∀ p ∈ N ClWWalksN G ∃ x ∈ D p = F ⁡ x
40 dffo3 ⊢ F : D ⟶ onto N ClWWalksN G ↔ F : D ⟶ N ClWWalksN G ∧ ∀ p ∈ N ClWWalksN G ∃ x ∈ D p = F ⁡ x
41 3 39 40 sylanbrc ⊢ N ∈ ℕ → F : D ⟶ onto N ClWWalksN G