Step |
Hyp |
Ref |
Expression |
1 |
|
elwwlks2s3.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
1
|
elwwlks2s3 |
⊢ ( 𝑊 ∈ ( 2 WWalksN 𝐺 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 𝑊 = 〈“ 𝑎 𝑏 𝑐 ”〉 ) |
3 |
|
fveq1 |
⊢ ( 𝑊 = 〈“ 𝑎 𝑏 𝑐 ”〉 → ( 𝑊 ‘ 1 ) = ( 〈“ 𝑎 𝑏 𝑐 ”〉 ‘ 1 ) ) |
4 |
|
s3fv1 |
⊢ ( 𝑏 ∈ 𝑉 → ( 〈“ 𝑎 𝑏 𝑐 ”〉 ‘ 1 ) = 𝑏 ) |
5 |
3 4
|
sylan9eqr |
⊢ ( ( 𝑏 ∈ 𝑉 ∧ 𝑊 = 〈“ 𝑎 𝑏 𝑐 ”〉 ) → ( 𝑊 ‘ 1 ) = 𝑏 ) |
6 |
5
|
ex |
⊢ ( 𝑏 ∈ 𝑉 → ( 𝑊 = 〈“ 𝑎 𝑏 𝑐 ”〉 → ( 𝑊 ‘ 1 ) = 𝑏 ) ) |
7 |
6
|
adantl |
⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑊 = 〈“ 𝑎 𝑏 𝑐 ”〉 → ( 𝑊 ‘ 1 ) = 𝑏 ) ) |
8 |
7
|
rexlimdvw |
⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( ∃ 𝑐 ∈ 𝑉 𝑊 = 〈“ 𝑎 𝑏 𝑐 ”〉 → ( 𝑊 ‘ 1 ) = 𝑏 ) ) |
9 |
8
|
reximdva |
⊢ ( 𝑎 ∈ 𝑉 → ( ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 𝑊 = 〈“ 𝑎 𝑏 𝑐 ”〉 → ∃ 𝑏 ∈ 𝑉 ( 𝑊 ‘ 1 ) = 𝑏 ) ) |
10 |
9
|
rexlimiv |
⊢ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 𝑊 = 〈“ 𝑎 𝑏 𝑐 ”〉 → ∃ 𝑏 ∈ 𝑉 ( 𝑊 ‘ 1 ) = 𝑏 ) |
11 |
2 10
|
syl |
⊢ ( 𝑊 ∈ ( 2 WWalksN 𝐺 ) → ∃ 𝑏 ∈ 𝑉 ( 𝑊 ‘ 1 ) = 𝑏 ) |