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