Step |
Hyp |
Ref |
Expression |
1 |
|
wwlksnextprop.x |
⊢ 𝑋 = ( ( 𝑁 + 1 ) WWalksN 𝐺 ) |
2 |
|
wwlksnextprop.e |
⊢ 𝐸 = ( Edg ‘ 𝐺 ) |
3 |
|
wwlksnextprop.y |
⊢ 𝑌 = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } |
4 |
|
wwlksnfi |
⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → ( 𝑁 WWalksN 𝐺 ) ∈ Fin ) |
5 |
|
ssrab2 |
⊢ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ⊆ ( 𝑁 WWalksN 𝐺 ) |
6 |
|
ssfi |
⊢ ( ( ( 𝑁 WWalksN 𝐺 ) ∈ Fin ∧ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ⊆ ( 𝑁 WWalksN 𝐺 ) ) → { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ∈ Fin ) |
7 |
4 5 6
|
sylancl |
⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ∈ Fin ) |
8 |
3 7
|
eqeltrid |
⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → 𝑌 ∈ Fin ) |
9 |
|
wwlksnfi |
⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∈ Fin ) |
10 |
1 9
|
eqeltrid |
⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → 𝑋 ∈ Fin ) |
11 |
|
rabfi |
⊢ ( 𝑋 ∈ Fin → { 𝑥 ∈ 𝑋 ∣ ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } ∈ Fin ) |
12 |
10 11
|
syl |
⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → { 𝑥 ∈ 𝑋 ∣ ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } ∈ Fin ) |
13 |
12
|
adantr |
⊢ ( ( ( Vtx ‘ 𝐺 ) ∈ Fin ∧ 𝑦 ∈ 𝑌 ) → { 𝑥 ∈ 𝑋 ∣ ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } ∈ Fin ) |
14 |
1 2 3
|
disjxwwlkn |
⊢ Disj 𝑦 ∈ 𝑌 { 𝑥 ∈ 𝑋 ∣ ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } |
15 |
14
|
a1i |
⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → Disj 𝑦 ∈ 𝑌 { 𝑥 ∈ 𝑋 ∣ ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } ) |
16 |
8 13 15
|
hashrabrex |
⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → ( ♯ ‘ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑌 ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } ) = Σ 𝑦 ∈ 𝑌 ( ♯ ‘ { 𝑥 ∈ 𝑋 ∣ ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } ) ) |