Step | Hyp | Ref
| Expression |
1 | | eliun 5001 |
. . 3
β’ (π¦ β βͺ π₯ β π (π₯(ClWWalksNOnβπΊ)π) β βπ₯ β π π¦ β (π₯(ClWWalksNOnβπΊ)π)) |
2 | | isclwwlknon 29382 |
. . . . 5
β’ (π¦ β (π₯(ClWWalksNOnβπΊ)π) β (π¦ β (π ClWWalksN πΊ) β§ (π¦β0) = π₯)) |
3 | 2 | rexbii 3094 |
. . . 4
β’
(βπ₯ β
π π¦ β (π₯(ClWWalksNOnβπΊ)π) β βπ₯ β π (π¦ β (π ClWWalksN πΊ) β§ (π¦β0) = π₯)) |
4 | | simpl 483 |
. . . . . 6
β’ ((π¦ β (π ClWWalksN πΊ) β§ (π¦β0) = π₯) β π¦ β (π ClWWalksN πΊ)) |
5 | 4 | rexlimivw 3151 |
. . . . 5
β’
(βπ₯ β
π (π¦ β (π ClWWalksN πΊ) β§ (π¦β0) = π₯) β π¦ β (π ClWWalksN πΊ)) |
6 | | clwwlknun.v |
. . . . . . . . 9
β’ π = (VtxβπΊ) |
7 | | eqid 2732 |
. . . . . . . . 9
β’
(EdgβπΊ) =
(EdgβπΊ) |
8 | 6, 7 | clwwlknp 29328 |
. . . . . . . 8
β’ (π¦ β (π ClWWalksN πΊ) β ((π¦ β Word π β§ (β―βπ¦) = π) β§ βπ β (0..^(π β 1)){(π¦βπ), (π¦β(π + 1))} β (EdgβπΊ) β§ {(lastSβπ¦), (π¦β0)} β (EdgβπΊ))) |
9 | 8 | anim2i 617 |
. . . . . . 7
β’ ((πΊ β USGraph β§ π¦ β (π ClWWalksN πΊ)) β (πΊ β USGraph β§ ((π¦ β Word π β§ (β―βπ¦) = π) β§ βπ β (0..^(π β 1)){(π¦βπ), (π¦β(π + 1))} β (EdgβπΊ) β§ {(lastSβπ¦), (π¦β0)} β (EdgβπΊ)))) |
10 | 7, 6 | usgrpredgv 28492 |
. . . . . . . . . . . . 13
β’ ((πΊ β USGraph β§
{(lastSβπ¦), (π¦β0)} β
(EdgβπΊ)) β
((lastSβπ¦) β
π β§ (π¦β0) β π)) |
11 | 10 | ex 413 |
. . . . . . . . . . . 12
β’ (πΊ β USGraph β
({(lastSβπ¦), (π¦β0)} β
(EdgβπΊ) β
((lastSβπ¦) β
π β§ (π¦β0) β π))) |
12 | | simpr 485 |
. . . . . . . . . . . 12
β’
(((lastSβπ¦)
β π β§ (π¦β0) β π) β (π¦β0) β π) |
13 | 11, 12 | syl6com 37 |
. . . . . . . . . . 11
β’
({(lastSβπ¦),
(π¦β0)} β
(EdgβπΊ) β (πΊ β USGraph β (π¦β0) β π)) |
14 | 13 | 3ad2ant3 1135 |
. . . . . . . . . 10
β’ (((π¦ β Word π β§ (β―βπ¦) = π) β§ βπ β (0..^(π β 1)){(π¦βπ), (π¦β(π + 1))} β (EdgβπΊ) β§ {(lastSβπ¦), (π¦β0)} β (EdgβπΊ)) β (πΊ β USGraph β (π¦β0) β π)) |
15 | 14 | impcom 408 |
. . . . . . . . 9
β’ ((πΊ β USGraph β§ ((π¦ β Word π β§ (β―βπ¦) = π) β§ βπ β (0..^(π β 1)){(π¦βπ), (π¦β(π + 1))} β (EdgβπΊ) β§ {(lastSβπ¦), (π¦β0)} β (EdgβπΊ))) β (π¦β0) β π) |
16 | | simpr 485 |
. . . . . . . . . . . 12
β’ (((πΊ β USGraph β§ ((π¦ β Word π β§ (β―βπ¦) = π) β§ βπ β (0..^(π β 1)){(π¦βπ), (π¦β(π + 1))} β (EdgβπΊ) β§ {(lastSβπ¦), (π¦β0)} β (EdgβπΊ))) β§ π₯ = (π¦β0)) β π₯ = (π¦β0)) |
17 | 16 | eqcomd 2738 |
. . . . . . . . . . 11
β’ (((πΊ β USGraph β§ ((π¦ β Word π β§ (β―βπ¦) = π) β§ βπ β (0..^(π β 1)){(π¦βπ), (π¦β(π + 1))} β (EdgβπΊ) β§ {(lastSβπ¦), (π¦β0)} β (EdgβπΊ))) β§ π₯ = (π¦β0)) β (π¦β0) = π₯) |
18 | 17 | biantrud 532 |
. . . . . . . . . 10
β’ (((πΊ β USGraph β§ ((π¦ β Word π β§ (β―βπ¦) = π) β§ βπ β (0..^(π β 1)){(π¦βπ), (π¦β(π + 1))} β (EdgβπΊ) β§ {(lastSβπ¦), (π¦β0)} β (EdgβπΊ))) β§ π₯ = (π¦β0)) β (π¦ β (π ClWWalksN πΊ) β (π¦ β (π ClWWalksN πΊ) β§ (π¦β0) = π₯))) |
19 | 18 | bicomd 222 |
. . . . . . . . 9
β’ (((πΊ β USGraph β§ ((π¦ β Word π β§ (β―βπ¦) = π) β§ βπ β (0..^(π β 1)){(π¦βπ), (π¦β(π + 1))} β (EdgβπΊ) β§ {(lastSβπ¦), (π¦β0)} β (EdgβπΊ))) β§ π₯ = (π¦β0)) β ((π¦ β (π ClWWalksN πΊ) β§ (π¦β0) = π₯) β π¦ β (π ClWWalksN πΊ))) |
20 | 15, 19 | rspcedv 3605 |
. . . . . . . 8
β’ ((πΊ β USGraph β§ ((π¦ β Word π β§ (β―βπ¦) = π) β§ βπ β (0..^(π β 1)){(π¦βπ), (π¦β(π + 1))} β (EdgβπΊ) β§ {(lastSβπ¦), (π¦β0)} β (EdgβπΊ))) β (π¦ β (π ClWWalksN πΊ) β βπ₯ β π (π¦ β (π ClWWalksN πΊ) β§ (π¦β0) = π₯))) |
21 | 20 | adantld 491 |
. . . . . . 7
β’ ((πΊ β USGraph β§ ((π¦ β Word π β§ (β―βπ¦) = π) β§ βπ β (0..^(π β 1)){(π¦βπ), (π¦β(π + 1))} β (EdgβπΊ) β§ {(lastSβπ¦), (π¦β0)} β (EdgβπΊ))) β ((πΊ β USGraph β§ π¦ β (π ClWWalksN πΊ)) β βπ₯ β π (π¦ β (π ClWWalksN πΊ) β§ (π¦β0) = π₯))) |
22 | 9, 21 | mpcom 38 |
. . . . . 6
β’ ((πΊ β USGraph β§ π¦ β (π ClWWalksN πΊ)) β βπ₯ β π (π¦ β (π ClWWalksN πΊ) β§ (π¦β0) = π₯)) |
23 | 22 | ex 413 |
. . . . 5
β’ (πΊ β USGraph β (π¦ β (π ClWWalksN πΊ) β βπ₯ β π (π¦ β (π ClWWalksN πΊ) β§ (π¦β0) = π₯))) |
24 | 5, 23 | impbid2 225 |
. . . 4
β’ (πΊ β USGraph β
(βπ₯ β π (π¦ β (π ClWWalksN πΊ) β§ (π¦β0) = π₯) β π¦ β (π ClWWalksN πΊ))) |
25 | 3, 24 | bitrid 282 |
. . 3
β’ (πΊ β USGraph β
(βπ₯ β π π¦ β (π₯(ClWWalksNOnβπΊ)π) β π¦ β (π ClWWalksN πΊ))) |
26 | 1, 25 | bitr2id 283 |
. 2
β’ (πΊ β USGraph β (π¦ β (π ClWWalksN πΊ) β π¦ β βͺ
π₯ β π (π₯(ClWWalksNOnβπΊ)π))) |
27 | 26 | eqrdv 2730 |
1
β’ (πΊ β USGraph β (π ClWWalksN πΊ) = βͺ
π₯ β π (π₯(ClWWalksNOnβπΊ)π)) |