Step |
Hyp |
Ref |
Expression |
1 |
|
wwlks.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
wwlks.e |
⊢ 𝐸 = ( Edg ‘ 𝐺 ) |
3 |
|
neeq1 |
⊢ ( 𝑤 = 𝑊 → ( 𝑤 ≠ ∅ ↔ 𝑊 ≠ ∅ ) ) |
4 |
|
fveq2 |
⊢ ( 𝑤 = 𝑊 → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑊 ) ) |
5 |
4
|
oveq1d |
⊢ ( 𝑤 = 𝑊 → ( ( ♯ ‘ 𝑤 ) − 1 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) ) |
6 |
5
|
oveq2d |
⊢ ( 𝑤 = 𝑊 → ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) = ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) |
7 |
|
fveq1 |
⊢ ( 𝑤 = 𝑊 → ( 𝑤 ‘ 𝑖 ) = ( 𝑊 ‘ 𝑖 ) ) |
8 |
|
fveq1 |
⊢ ( 𝑤 = 𝑊 → ( 𝑤 ‘ ( 𝑖 + 1 ) ) = ( 𝑊 ‘ ( 𝑖 + 1 ) ) ) |
9 |
7 8
|
preq12d |
⊢ ( 𝑤 = 𝑊 → { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } = { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ) |
10 |
9
|
eleq1d |
⊢ ( 𝑤 = 𝑊 → ( { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ↔ { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) |
11 |
6 10
|
raleqbidv |
⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) |
12 |
3 11
|
anbi12d |
⊢ ( 𝑤 = 𝑊 → ( ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ↔ ( 𝑊 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) ) |
13 |
12
|
elrab |
⊢ ( 𝑊 ∈ { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) } ↔ ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) ) |
14 |
1 2
|
wwlks |
⊢ ( WWalks ‘ 𝐺 ) = { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) } |
15 |
14
|
eleq2i |
⊢ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ↔ 𝑊 ∈ { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) } ) |
16 |
|
3anan12 |
⊢ ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ↔ ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) ) |
17 |
13 15 16
|
3bitr4i |
⊢ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ↔ ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) |