Step |
Hyp |
Ref |
Expression |
1 |
|
wwlks.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
wwlks.e |
⊢ 𝐸 = ( Edg ‘ 𝐺 ) |
3 |
|
df-wwlks |
⊢ WWalks = ( 𝑔 ∈ V ↦ { 𝑤 ∈ Word ( Vtx ‘ 𝑔 ) ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝑔 ) ) } ) |
4 |
|
fveq2 |
⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) ) |
5 |
4 1
|
eqtr4di |
⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = 𝑉 ) |
6 |
|
wrdeq |
⊢ ( ( Vtx ‘ 𝑔 ) = 𝑉 → Word ( Vtx ‘ 𝑔 ) = Word 𝑉 ) |
7 |
5 6
|
syl |
⊢ ( 𝑔 = 𝐺 → Word ( Vtx ‘ 𝑔 ) = Word 𝑉 ) |
8 |
|
fveq2 |
⊢ ( 𝑔 = 𝐺 → ( Edg ‘ 𝑔 ) = ( Edg ‘ 𝐺 ) ) |
9 |
8 2
|
eqtr4di |
⊢ ( 𝑔 = 𝐺 → ( Edg ‘ 𝑔 ) = 𝐸 ) |
10 |
9
|
eleq2d |
⊢ ( 𝑔 = 𝐺 → ( { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝑔 ) ↔ { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) |
11 |
10
|
ralbidv |
⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝑔 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) |
12 |
11
|
anbi2d |
⊢ ( 𝑔 = 𝐺 → ( ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝑔 ) ) ↔ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) ) |
13 |
7 12
|
rabeqbidv |
⊢ ( 𝑔 = 𝐺 → { 𝑤 ∈ Word ( Vtx ‘ 𝑔 ) ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝑔 ) ) } = { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) } ) |
14 |
|
id |
⊢ ( 𝐺 ∈ V → 𝐺 ∈ V ) |
15 |
1
|
fvexi |
⊢ 𝑉 ∈ V |
16 |
15
|
a1i |
⊢ ( 𝐺 ∈ V → 𝑉 ∈ V ) |
17 |
|
wrdexg |
⊢ ( 𝑉 ∈ V → Word 𝑉 ∈ V ) |
18 |
|
rabexg |
⊢ ( Word 𝑉 ∈ V → { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) } ∈ V ) |
19 |
16 17 18
|
3syl |
⊢ ( 𝐺 ∈ V → { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) } ∈ V ) |
20 |
3 13 14 19
|
fvmptd3 |
⊢ ( 𝐺 ∈ V → ( WWalks ‘ 𝐺 ) = { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) } ) |
21 |
|
fvprc |
⊢ ( ¬ 𝐺 ∈ V → ( WWalks ‘ 𝐺 ) = ∅ ) |
22 |
|
fvprc |
⊢ ( ¬ 𝐺 ∈ V → ( Vtx ‘ 𝐺 ) = ∅ ) |
23 |
1 22
|
syl5eq |
⊢ ( ¬ 𝐺 ∈ V → 𝑉 = ∅ ) |
24 |
|
wrdeq |
⊢ ( 𝑉 = ∅ → Word 𝑉 = Word ∅ ) |
25 |
23 24
|
syl |
⊢ ( ¬ 𝐺 ∈ V → Word 𝑉 = Word ∅ ) |
26 |
25
|
eleq2d |
⊢ ( ¬ 𝐺 ∈ V → ( 𝑤 ∈ Word 𝑉 ↔ 𝑤 ∈ Word ∅ ) ) |
27 |
|
0wrd0 |
⊢ ( 𝑤 ∈ Word ∅ ↔ 𝑤 = ∅ ) |
28 |
26 27
|
bitrdi |
⊢ ( ¬ 𝐺 ∈ V → ( 𝑤 ∈ Word 𝑉 ↔ 𝑤 = ∅ ) ) |
29 |
|
nne |
⊢ ( ¬ 𝑤 ≠ ∅ ↔ 𝑤 = ∅ ) |
30 |
29
|
biimpri |
⊢ ( 𝑤 = ∅ → ¬ 𝑤 ≠ ∅ ) |
31 |
30
|
intnanrd |
⊢ ( 𝑤 = ∅ → ¬ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) |
32 |
28 31
|
syl6bi |
⊢ ( ¬ 𝐺 ∈ V → ( 𝑤 ∈ Word 𝑉 → ¬ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) ) |
33 |
32
|
ralrimiv |
⊢ ( ¬ 𝐺 ∈ V → ∀ 𝑤 ∈ Word 𝑉 ¬ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) |
34 |
|
rabeq0 |
⊢ ( { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) } = ∅ ↔ ∀ 𝑤 ∈ Word 𝑉 ¬ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) ) |
35 |
33 34
|
sylibr |
⊢ ( ¬ 𝐺 ∈ V → { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) } = ∅ ) |
36 |
21 35
|
eqtr4d |
⊢ ( ¬ 𝐺 ∈ V → ( WWalks ‘ 𝐺 ) = { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) } ) |
37 |
20 36
|
pm2.61i |
⊢ ( WWalks ‘ 𝐺 ) = { 𝑤 ∈ Word 𝑉 ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) } |