Step |
Hyp |
Ref |
Expression |
1 |
|
wwlksnexthasheq.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
wwlksnexthasheq.e |
⊢ 𝐸 = ( Edg ‘ 𝐺 ) |
3 |
|
simp1 |
⊢ ( ( ( 𝑥 prefix 𝑁 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) → ( 𝑥 prefix 𝑁 ) = 𝑦 ) |
4 |
3
|
a1i |
⊢ ( 𝑥 ∈ Word 𝑉 → ( ( ( 𝑥 prefix 𝑁 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) → ( 𝑥 prefix 𝑁 ) = 𝑦 ) ) |
5 |
4
|
ss2rabi |
⊢ { 𝑥 ∈ Word 𝑉 ∣ ( ( 𝑥 prefix 𝑁 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } ⊆ { 𝑥 ∈ Word 𝑉 ∣ ( 𝑥 prefix 𝑁 ) = 𝑦 } |
6 |
5
|
rgenw |
⊢ ∀ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) { 𝑥 ∈ Word 𝑉 ∣ ( ( 𝑥 prefix 𝑁 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } ⊆ { 𝑥 ∈ Word 𝑉 ∣ ( 𝑥 prefix 𝑁 ) = 𝑦 } |
7 |
|
disjwrdpfx |
⊢ Disj 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) { 𝑥 ∈ Word 𝑉 ∣ ( 𝑥 prefix 𝑁 ) = 𝑦 } |
8 |
|
disjss2 |
⊢ ( ∀ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) { 𝑥 ∈ Word 𝑉 ∣ ( ( 𝑥 prefix 𝑁 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } ⊆ { 𝑥 ∈ Word 𝑉 ∣ ( 𝑥 prefix 𝑁 ) = 𝑦 } → ( Disj 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) { 𝑥 ∈ Word 𝑉 ∣ ( 𝑥 prefix 𝑁 ) = 𝑦 } → Disj 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) { 𝑥 ∈ Word 𝑉 ∣ ( ( 𝑥 prefix 𝑁 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } ) ) |
9 |
6 7 8
|
mp2 |
⊢ Disj 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) { 𝑥 ∈ Word 𝑉 ∣ ( ( 𝑥 prefix 𝑁 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } |