Step |
Hyp |
Ref |
Expression |
1 |
|
wlknwwlksnbij.t |
⊢ 𝑇 = { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 } |
2 |
|
wlknwwlksnbij.w |
⊢ 𝑊 = ( 𝑁 WWalksN 𝐺 ) |
3 |
|
wlknwwlksnbij.f |
⊢ 𝐹 = ( 𝑡 ∈ 𝑇 ↦ ( 2nd ‘ 𝑡 ) ) |
4 |
|
eqid |
⊢ ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd ‘ 𝑝 ) ) = ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd ‘ 𝑝 ) ) |
5 |
4
|
wlkswwlksf1o |
⊢ ( 𝐺 ∈ USPGraph → ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd ‘ 𝑝 ) ) : ( Walks ‘ 𝐺 ) –1-1-onto→ ( WWalks ‘ 𝐺 ) ) |
6 |
5
|
adantr |
⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd ‘ 𝑝 ) ) : ( Walks ‘ 𝐺 ) –1-1-onto→ ( WWalks ‘ 𝐺 ) ) |
7 |
|
fveqeq2 |
⊢ ( 𝑞 = ( 2nd ‘ 𝑝 ) → ( ( ♯ ‘ 𝑞 ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ ( 2nd ‘ 𝑝 ) ) = ( 𝑁 + 1 ) ) ) |
8 |
7
|
3ad2ant3 |
⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑝 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑞 = ( 2nd ‘ 𝑝 ) ) → ( ( ♯ ‘ 𝑞 ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ ( 2nd ‘ 𝑝 ) ) = ( 𝑁 + 1 ) ) ) |
9 |
|
wlkcpr |
⊢ ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↔ ( 1st ‘ 𝑝 ) ( Walks ‘ 𝐺 ) ( 2nd ‘ 𝑝 ) ) |
10 |
|
wlklenvp1 |
⊢ ( ( 1st ‘ 𝑝 ) ( Walks ‘ 𝐺 ) ( 2nd ‘ 𝑝 ) → ( ♯ ‘ ( 2nd ‘ 𝑝 ) ) = ( ( ♯ ‘ ( 1st ‘ 𝑝 ) ) + 1 ) ) |
11 |
|
eqeq1 |
⊢ ( ( ♯ ‘ ( 2nd ‘ 𝑝 ) ) = ( ( ♯ ‘ ( 1st ‘ 𝑝 ) ) + 1 ) → ( ( ♯ ‘ ( 2nd ‘ 𝑝 ) ) = ( 𝑁 + 1 ) ↔ ( ( ♯ ‘ ( 1st ‘ 𝑝 ) ) + 1 ) = ( 𝑁 + 1 ) ) ) |
12 |
|
wlkcl |
⊢ ( ( 1st ‘ 𝑝 ) ( Walks ‘ 𝐺 ) ( 2nd ‘ 𝑝 ) → ( ♯ ‘ ( 1st ‘ 𝑝 ) ) ∈ ℕ0 ) |
13 |
12
|
nn0cnd |
⊢ ( ( 1st ‘ 𝑝 ) ( Walks ‘ 𝐺 ) ( 2nd ‘ 𝑝 ) → ( ♯ ‘ ( 1st ‘ 𝑝 ) ) ∈ ℂ ) |
14 |
13
|
adantr |
⊢ ( ( ( 1st ‘ 𝑝 ) ( Walks ‘ 𝐺 ) ( 2nd ‘ 𝑝 ) ∧ ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) ) → ( ♯ ‘ ( 1st ‘ 𝑝 ) ) ∈ ℂ ) |
15 |
|
nn0cn |
⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ ) |
16 |
15
|
adantl |
⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℂ ) |
17 |
16
|
adantl |
⊢ ( ( ( 1st ‘ 𝑝 ) ( Walks ‘ 𝐺 ) ( 2nd ‘ 𝑝 ) ∧ ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) ) → 𝑁 ∈ ℂ ) |
18 |
|
1cnd |
⊢ ( ( ( 1st ‘ 𝑝 ) ( Walks ‘ 𝐺 ) ( 2nd ‘ 𝑝 ) ∧ ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) ) → 1 ∈ ℂ ) |
19 |
14 17 18
|
addcan2d |
⊢ ( ( ( 1st ‘ 𝑝 ) ( Walks ‘ 𝐺 ) ( 2nd ‘ 𝑝 ) ∧ ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) ) → ( ( ( ♯ ‘ ( 1st ‘ 𝑝 ) ) + 1 ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 ) ) |
20 |
11 19
|
sylan9bbr |
⊢ ( ( ( ( 1st ‘ 𝑝 ) ( Walks ‘ 𝐺 ) ( 2nd ‘ 𝑝 ) ∧ ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) ) ∧ ( ♯ ‘ ( 2nd ‘ 𝑝 ) ) = ( ( ♯ ‘ ( 1st ‘ 𝑝 ) ) + 1 ) ) → ( ( ♯ ‘ ( 2nd ‘ 𝑝 ) ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 ) ) |
21 |
20
|
exp31 |
⊢ ( ( 1st ‘ 𝑝 ) ( Walks ‘ 𝐺 ) ( 2nd ‘ 𝑝 ) → ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ ( 2nd ‘ 𝑝 ) ) = ( ( ♯ ‘ ( 1st ‘ 𝑝 ) ) + 1 ) → ( ( ♯ ‘ ( 2nd ‘ 𝑝 ) ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 ) ) ) ) |
22 |
10 21
|
mpid |
⊢ ( ( 1st ‘ 𝑝 ) ( Walks ‘ 𝐺 ) ( 2nd ‘ 𝑝 ) → ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ ( 2nd ‘ 𝑝 ) ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 ) ) ) |
23 |
9 22
|
sylbi |
⊢ ( 𝑝 ∈ ( Walks ‘ 𝐺 ) → ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ ( 2nd ‘ 𝑝 ) ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 ) ) ) |
24 |
23
|
impcom |
⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑝 ∈ ( Walks ‘ 𝐺 ) ) → ( ( ♯ ‘ ( 2nd ‘ 𝑝 ) ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 ) ) |
25 |
24
|
3adant3 |
⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑝 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑞 = ( 2nd ‘ 𝑝 ) ) → ( ( ♯ ‘ ( 2nd ‘ 𝑝 ) ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 ) ) |
26 |
8 25
|
bitrd |
⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑝 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑞 = ( 2nd ‘ 𝑝 ) ) → ( ( ♯ ‘ 𝑞 ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 ) ) |
27 |
4 6 26
|
f1oresrab |
⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd ‘ 𝑝 ) ) ↾ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 } ) : { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 } –1-1-onto→ { 𝑞 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑞 ) = ( 𝑁 + 1 ) } ) |
28 |
1
|
mpteq1i |
⊢ ( 𝑡 ∈ 𝑇 ↦ ( 2nd ‘ 𝑡 ) ) = ( 𝑡 ∈ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 } ↦ ( 2nd ‘ 𝑡 ) ) |
29 |
|
ssrab2 |
⊢ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 } ⊆ ( Walks ‘ 𝐺 ) |
30 |
|
resmpt |
⊢ ( { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 } ⊆ ( Walks ‘ 𝐺 ) → ( ( 𝑡 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd ‘ 𝑡 ) ) ↾ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 } ) = ( 𝑡 ∈ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 } ↦ ( 2nd ‘ 𝑡 ) ) ) |
31 |
29 30
|
ax-mp |
⊢ ( ( 𝑡 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd ‘ 𝑡 ) ) ↾ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 } ) = ( 𝑡 ∈ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 } ↦ ( 2nd ‘ 𝑡 ) ) |
32 |
|
fveq2 |
⊢ ( 𝑡 = 𝑝 → ( 2nd ‘ 𝑡 ) = ( 2nd ‘ 𝑝 ) ) |
33 |
32
|
cbvmptv |
⊢ ( 𝑡 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd ‘ 𝑡 ) ) = ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd ‘ 𝑝 ) ) |
34 |
33
|
reseq1i |
⊢ ( ( 𝑡 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd ‘ 𝑡 ) ) ↾ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 } ) = ( ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd ‘ 𝑝 ) ) ↾ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 } ) |
35 |
28 31 34
|
3eqtr2i |
⊢ ( 𝑡 ∈ 𝑇 ↦ ( 2nd ‘ 𝑡 ) ) = ( ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd ‘ 𝑝 ) ) ↾ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 } ) |
36 |
35
|
a1i |
⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → ( 𝑡 ∈ 𝑇 ↦ ( 2nd ‘ 𝑡 ) ) = ( ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd ‘ 𝑝 ) ) ↾ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 } ) ) |
37 |
3 36
|
syl5eq |
⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → 𝐹 = ( ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd ‘ 𝑝 ) ) ↾ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 } ) ) |
38 |
1
|
a1i |
⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → 𝑇 = { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 } ) |
39 |
|
wwlksn |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 WWalksN 𝐺 ) = { 𝑞 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑞 ) = ( 𝑁 + 1 ) } ) |
40 |
39
|
adantl |
⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 WWalksN 𝐺 ) = { 𝑞 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑞 ) = ( 𝑁 + 1 ) } ) |
41 |
2 40
|
syl5eq |
⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → 𝑊 = { 𝑞 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑞 ) = ( 𝑁 + 1 ) } ) |
42 |
37 38 41
|
f1oeq123d |
⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → ( 𝐹 : 𝑇 –1-1-onto→ 𝑊 ↔ ( ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd ‘ 𝑝 ) ) ↾ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 } ) : { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑝 ) ) = 𝑁 } –1-1-onto→ { 𝑞 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑞 ) = ( 𝑁 + 1 ) } ) ) |
43 |
27 42
|
mpbird |
⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → 𝐹 : 𝑇 –1-1-onto→ 𝑊 ) |