Step |
Hyp |
Ref |
Expression |
1 |
|
clwwlk.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
clwwlk.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 |
|
fveq2 |
⊢ ( 𝑤 = 𝑊 → ( lastS ‘ 𝑤 ) = ( lastS ‘ 𝑊 ) ) |
13 |
|
fveq1 |
⊢ ( 𝑤 = 𝑊 → ( 𝑤 ‘ 0 ) = ( 𝑊 ‘ 0 ) ) |
14 |
12 13
|
preq12d |
⊢ ( 𝑤 = 𝑊 → { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } = { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ) |
15 |
14
|
eleq1d |
⊢ ( 𝑤 = 𝑊 → ( { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ 𝐸 ↔ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) |
16 |
3 11 15
|
3anbi123d |
⊢ ( 𝑤 = 𝑊 → ( ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ 𝐸 ) ↔ ( 𝑊 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ) |
17 |
16
|
elrab |
⊢ ( 𝑊 ∈ { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ 𝐸 ) } ↔ ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ) |
18 |
1 2
|
clwwlk |
⊢ ( ClWWalks ‘ 𝐺 ) = { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ 𝐸 ) } |
19 |
18
|
eleq2i |
⊢ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ↔ 𝑊 ∈ { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ 𝐸 ) } ) |
20 |
|
3anass |
⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ) |
21 |
|
anass |
⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ↔ ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 ≠ ∅ ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ) ) |
22 |
|
3anass |
⊢ ( ( 𝑊 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ↔ ( 𝑊 ≠ ∅ ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ) |
23 |
22
|
bicomi |
⊢ ( ( 𝑊 ≠ ∅ ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ↔ ( 𝑊 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) |
24 |
23
|
anbi2i |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 ≠ ∅ ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ) ↔ ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ) |
25 |
20 21 24
|
3bitri |
⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ↔ ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) ) |
26 |
17 19 25
|
3bitr4i |
⊢ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ 𝐸 ) ) |