Proof of Theorem av-numclwwlkovf2
Step | Hyp | Ref
| Expression |
1 | | simpr 476 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ 𝑉) |
2 | | 2nn 11062 |
. . 3
⊢ 2 ∈
ℕ |
3 | | av-numclwwlkovf.f |
. . . 4
⊢ 𝐹 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑣}) |
4 | 3 | av-numclwwlkovf 41511 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 2 ∈ ℕ) → (𝑋𝐹2) = {𝑤 ∈ (2 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑋}) |
5 | 1, 2, 4 | sylancl 693 |
. 2
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → (𝑋𝐹2) = {𝑤 ∈ (2 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑋}) |
6 | | clwwlksn2 41217 |
. . . . . 6
⊢ (𝑤 ∈ (2 ClWWalkSN 𝐺) ↔ ((#‘𝑤) = 2 ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))) |
7 | 6 | anbi1i 727 |
. . . . 5
⊢ ((𝑤 ∈ (2 ClWWalkSN 𝐺) ∧ (𝑤‘0) = 𝑋) ↔ (((#‘𝑤) = 2 ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)) ∧ (𝑤‘0) = 𝑋)) |
8 | 7 | a1i 11 |
. . . 4
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → ((𝑤 ∈ (2 ClWWalkSN 𝐺) ∧ (𝑤‘0) = 𝑋) ↔ (((#‘𝑤) = 2 ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)) ∧ (𝑤‘0) = 𝑋))) |
9 | | anass 679 |
. . . . 5
⊢ (((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 2 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝐸)) ∧ (𝑤‘0) = 𝑋) ↔ (𝑤 ∈ Word 𝑉 ∧ (((#‘𝑤) = 2 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝐸) ∧ (𝑤‘0) = 𝑋))) |
10 | | df-3an 1033 |
. . . . . . . 8
⊢
(((#‘𝑤) = 2
∧ 𝑤 ∈ Word
(Vtx‘𝐺) ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)) ↔ (((#‘𝑤) = 2 ∧ 𝑤 ∈ Word (Vtx‘𝐺)) ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))) |
11 | | ancom 465 |
. . . . . . . . . 10
⊢
(((#‘𝑤) = 2
∧ 𝑤 ∈ Word
(Vtx‘𝐺)) ↔
(𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) =
2)) |
12 | | av-numclwwlkffin.v |
. . . . . . . . . . . . . 14
⊢ 𝑉 = (Vtx‘𝐺) |
13 | 12 | eqcomi 2619 |
. . . . . . . . . . . . 13
⊢
(Vtx‘𝐺) =
𝑉 |
14 | 13 | wrdeqi 13183 |
. . . . . . . . . . . 12
⊢ Word
(Vtx‘𝐺) = Word 𝑉 |
15 | 14 | eleq2i 2680 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ Word (Vtx‘𝐺) ↔ 𝑤 ∈ Word 𝑉) |
16 | 15 | anbi1i 727 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 2) ↔ (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 2)) |
17 | 11, 16 | bitri 263 |
. . . . . . . . 9
⊢
(((#‘𝑤) = 2
∧ 𝑤 ∈ Word
(Vtx‘𝐺)) ↔
(𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 2)) |
18 | | av-numclwwlkovfel2.e |
. . . . . . . . . . 11
⊢ 𝐸 = (Edg‘𝐺) |
19 | 18 | eqcomi 2619 |
. . . . . . . . . 10
⊢
(Edg‘𝐺) =
𝐸 |
20 | 19 | eleq2i 2680 |
. . . . . . . . 9
⊢ ({(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺) ↔ {(𝑤‘0), (𝑤‘1)} ∈ 𝐸) |
21 | 17, 20 | anbi12i 729 |
. . . . . . . 8
⊢
((((#‘𝑤) = 2
∧ 𝑤 ∈ Word
(Vtx‘𝐺)) ∧
{(𝑤‘0), (𝑤‘1)} ∈
(Edg‘𝐺)) ↔
((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 2) ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝐸)) |
22 | 10, 21 | bitri 263 |
. . . . . . 7
⊢
(((#‘𝑤) = 2
∧ 𝑤 ∈ Word
(Vtx‘𝐺) ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)) ↔ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 2) ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝐸)) |
23 | | anass 679 |
. . . . . . 7
⊢ (((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 2) ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝐸) ↔ (𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 2 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝐸))) |
24 | 22, 23 | bitri 263 |
. . . . . 6
⊢
(((#‘𝑤) = 2
∧ 𝑤 ∈ Word
(Vtx‘𝐺) ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)) ↔ (𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 2 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝐸))) |
25 | 24 | anbi1i 727 |
. . . . 5
⊢
((((#‘𝑤) = 2
∧ 𝑤 ∈ Word
(Vtx‘𝐺) ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)) ∧ (𝑤‘0) = 𝑋) ↔ ((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 2 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝐸)) ∧ (𝑤‘0) = 𝑋)) |
26 | | df-3an 1033 |
. . . . . 6
⊢
(((#‘𝑤) = 2
∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝐸 ∧ (𝑤‘0) = 𝑋) ↔ (((#‘𝑤) = 2 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝐸) ∧ (𝑤‘0) = 𝑋)) |
27 | 26 | anbi2i 726 |
. . . . 5
⊢ ((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 2 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝐸 ∧ (𝑤‘0) = 𝑋)) ↔ (𝑤 ∈ Word 𝑉 ∧ (((#‘𝑤) = 2 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝐸) ∧ (𝑤‘0) = 𝑋))) |
28 | 9, 25, 27 | 3bitr4i 291 |
. . . 4
⊢
((((#‘𝑤) = 2
∧ 𝑤 ∈ Word
(Vtx‘𝐺) ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)) ∧ (𝑤‘0) = 𝑋) ↔ (𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 2 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝐸 ∧ (𝑤‘0) = 𝑋))) |
29 | 8, 28 | syl6bb 275 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → ((𝑤 ∈ (2 ClWWalkSN 𝐺) ∧ (𝑤‘0) = 𝑋) ↔ (𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 2 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝐸 ∧ (𝑤‘0) = 𝑋)))) |
30 | 29 | rabbidva2 3162 |
. 2
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → {𝑤 ∈ (2 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑋} = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝐸 ∧ (𝑤‘0) = 𝑋)}) |
31 | 5, 30 | eqtrd 2644 |
1
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → (𝑋𝐹2) = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝐸 ∧ (𝑤‘0) = 𝑋)}) |