Step |
Hyp |
Ref |
Expression |
1 |
|
wwlksnextprop.x |
⊢ 𝑋 = ( ( 𝑁 + 1 ) WWalksN 𝐺 ) |
2 |
|
wwlksnextprop.e |
⊢ 𝐸 = ( Edg ‘ 𝐺 ) |
3 |
|
wwlksnextprop.y |
⊢ 𝑌 = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } |
4 |
|
simp1 |
⊢ ( ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) → ( 𝑥 prefix 𝑀 ) = 𝑦 ) |
5 |
4
|
rgenw |
⊢ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) → ( 𝑥 prefix 𝑀 ) = 𝑦 ) |
6 |
|
ss2rab |
⊢ ( { 𝑥 ∈ 𝑋 ∣ ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } ⊆ { 𝑥 ∈ 𝑋 ∣ ( 𝑥 prefix 𝑀 ) = 𝑦 } ↔ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) → ( 𝑥 prefix 𝑀 ) = 𝑦 ) ) |
7 |
5 6
|
mpbir |
⊢ { 𝑥 ∈ 𝑋 ∣ ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } ⊆ { 𝑥 ∈ 𝑋 ∣ ( 𝑥 prefix 𝑀 ) = 𝑦 } |
8 |
|
wwlkssswwlksn |
⊢ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ⊆ ( WWalks ‘ 𝐺 ) |
9 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
10 |
9
|
wwlkssswrd |
⊢ ( WWalks ‘ 𝐺 ) ⊆ Word ( Vtx ‘ 𝐺 ) |
11 |
8 10
|
sstri |
⊢ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ⊆ Word ( Vtx ‘ 𝐺 ) |
12 |
1 11
|
eqsstri |
⊢ 𝑋 ⊆ Word ( Vtx ‘ 𝐺 ) |
13 |
|
rabss2 |
⊢ ( 𝑋 ⊆ Word ( Vtx ‘ 𝐺 ) → { 𝑥 ∈ 𝑋 ∣ ( 𝑥 prefix 𝑀 ) = 𝑦 } ⊆ { 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( 𝑥 prefix 𝑀 ) = 𝑦 } ) |
14 |
12 13
|
ax-mp |
⊢ { 𝑥 ∈ 𝑋 ∣ ( 𝑥 prefix 𝑀 ) = 𝑦 } ⊆ { 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( 𝑥 prefix 𝑀 ) = 𝑦 } |
15 |
7 14
|
sstri |
⊢ { 𝑥 ∈ 𝑋 ∣ ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } ⊆ { 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( 𝑥 prefix 𝑀 ) = 𝑦 } |
16 |
15
|
rgenw |
⊢ ∀ 𝑦 ∈ 𝑌 { 𝑥 ∈ 𝑋 ∣ ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } ⊆ { 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( 𝑥 prefix 𝑀 ) = 𝑦 } |
17 |
|
disjwrdpfx |
⊢ Disj 𝑦 ∈ 𝑌 { 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( 𝑥 prefix 𝑀 ) = 𝑦 } |
18 |
|
disjss2 |
⊢ ( ∀ 𝑦 ∈ 𝑌 { 𝑥 ∈ 𝑋 ∣ ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } ⊆ { 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( 𝑥 prefix 𝑀 ) = 𝑦 } → ( Disj 𝑦 ∈ 𝑌 { 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( 𝑥 prefix 𝑀 ) = 𝑦 } → Disj 𝑦 ∈ 𝑌 { 𝑥 ∈ 𝑋 ∣ ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } ) ) |
19 |
16 17 18
|
mp2 |
⊢ Disj 𝑦 ∈ 𝑌 { 𝑥 ∈ 𝑋 ∣ ( ( 𝑥 prefix 𝑀 ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } |