Step |
Hyp |
Ref |
Expression |
1 |
|
ewlksfval.i |
⊢ 𝐼 = ( iEdg ‘ 𝐺 ) |
2 |
1
|
ewlksfval |
⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ) → ( 𝐺 EdgWalks 𝑆 ) = { 𝑓 ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) } ) |
3 |
2
|
3adant3 |
⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ∧ 𝐹 ∈ 𝑈 ) → ( 𝐺 EdgWalks 𝑆 ) = { 𝑓 ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) } ) |
4 |
3
|
eleq2d |
⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ∧ 𝐹 ∈ 𝑈 ) → ( 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) ↔ 𝐹 ∈ { 𝑓 ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) } ) ) |
5 |
|
eleq1 |
⊢ ( 𝑓 = 𝐹 → ( 𝑓 ∈ Word dom 𝐼 ↔ 𝐹 ∈ Word dom 𝐼 ) ) |
6 |
|
fveq2 |
⊢ ( 𝑓 = 𝐹 → ( ♯ ‘ 𝑓 ) = ( ♯ ‘ 𝐹 ) ) |
7 |
6
|
oveq2d |
⊢ ( 𝑓 = 𝐹 → ( 1 ..^ ( ♯ ‘ 𝑓 ) ) = ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) |
8 |
|
fveq1 |
⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ ( 𝑘 − 1 ) ) = ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) |
9 |
8
|
fveq2d |
⊢ ( 𝑓 = 𝐹 → ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) = ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) |
10 |
|
fveq1 |
⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) ) |
11 |
10
|
fveq2d |
⊢ ( 𝑓 = 𝐹 → ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) |
12 |
9 11
|
ineq12d |
⊢ ( 𝑓 = 𝐹 → ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) = ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) |
13 |
12
|
fveq2d |
⊢ ( 𝑓 = 𝐹 → ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) = ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) |
14 |
13
|
breq2d |
⊢ ( 𝑓 = 𝐹 → ( 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ↔ 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) |
15 |
7 14
|
raleqbidv |
⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ↔ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) |
16 |
5 15
|
anbi12d |
⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) ) |
17 |
16
|
elabg |
⊢ ( 𝐹 ∈ 𝑈 → ( 𝐹 ∈ { 𝑓 ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) } ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) ) |
18 |
17
|
3ad2ant3 |
⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ∧ 𝐹 ∈ 𝑈 ) → ( 𝐹 ∈ { 𝑓 ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) } ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) ) |
19 |
4 18
|
bitrd |
⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ∧ 𝐹 ∈ 𝑈 ) → ( 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) ) |