Step | Hyp | Ref
| Expression |
1 | | numclwwlk3lem2.c |
. . . . 5
β’ πΆ = (π£ β π, π β (β€β₯β2)
β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π£}) |
2 | | numclwwlk3lem2.h |
. . . . 5
β’ π» = (π£ β π, π β (β€β₯β2)
β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) β π£}) |
3 | 1, 2 | numclwwlk3lem2lem 29369 |
. . . 4
β’ ((π β π β§ π β (β€β₯β2))
β (π(ClWWalksNOnβπΊ)π) = ((ππ»π) βͺ (ππΆπ))) |
4 | 3 | adantll 713 |
. . 3
β’ (((πΊ β FinUSGraph β§ π β π) β§ π β (β€β₯β2))
β (π(ClWWalksNOnβπΊ)π) = ((ππ»π) βͺ (ππΆπ))) |
5 | 4 | fveq2d 6851 |
. 2
β’ (((πΊ β FinUSGraph β§ π β π) β§ π β (β€β₯β2))
β (β―β(π(ClWWalksNOnβπΊ)π)) = (β―β((ππ»π) βͺ (ππΆπ)))) |
6 | 2 | numclwwlkovh0 29358 |
. . . . 5
β’ ((π β π β§ π β (β€β₯β2))
β (ππ»π) = {π€ β (π(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) β π}) |
7 | 6 | adantll 713 |
. . . 4
β’ (((πΊ β FinUSGraph β§ π β π) β§ π β (β€β₯β2))
β (ππ»π) = {π€ β (π(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) β π}) |
8 | | eqid 2737 |
. . . . . . 7
β’
(VtxβπΊ) =
(VtxβπΊ) |
9 | 8 | fusgrvtxfi 28309 |
. . . . . 6
β’ (πΊ β FinUSGraph β
(VtxβπΊ) β
Fin) |
10 | 9 | ad2antrr 725 |
. . . . 5
β’ (((πΊ β FinUSGraph β§ π β π) β§ π β (β€β₯β2))
β (VtxβπΊ) β
Fin) |
11 | 8 | clwwlknonfin 29080 |
. . . . 5
β’
((VtxβπΊ)
β Fin β (π(ClWWalksNOnβπΊ)π) β Fin) |
12 | | rabfi 9220 |
. . . . 5
β’ ((π(ClWWalksNOnβπΊ)π) β Fin β {π€ β (π(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) β π} β Fin) |
13 | 10, 11, 12 | 3syl 18 |
. . . 4
β’ (((πΊ β FinUSGraph β§ π β π) β§ π β (β€β₯β2))
β {π€ β (π(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) β π} β Fin) |
14 | 7, 13 | eqeltrd 2838 |
. . 3
β’ (((πΊ β FinUSGraph β§ π β π) β§ π β (β€β₯β2))
β (ππ»π) β Fin) |
15 | 1 | 2clwwlk 29333 |
. . . . 5
β’ ((π β π β§ π β (β€β₯β2))
β (ππΆπ) = {π€ β (π(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π}) |
16 | 15 | adantll 713 |
. . . 4
β’ (((πΊ β FinUSGraph β§ π β π) β§ π β (β€β₯β2))
β (ππΆπ) = {π€ β (π(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π}) |
17 | | rabfi 9220 |
. . . . 5
β’ ((π(ClWWalksNOnβπΊ)π) β Fin β {π€ β (π(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π} β Fin) |
18 | 10, 11, 17 | 3syl 18 |
. . . 4
β’ (((πΊ β FinUSGraph β§ π β π) β§ π β (β€β₯β2))
β {π€ β (π(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π} β Fin) |
19 | 16, 18 | eqeltrd 2838 |
. . 3
β’ (((πΊ β FinUSGraph β§ π β π) β§ π β (β€β₯β2))
β (ππΆπ) β Fin) |
20 | 7, 16 | ineq12d 4178 |
. . . 4
β’ (((πΊ β FinUSGraph β§ π β π) β§ π β (β€β₯β2))
β ((ππ»π) β© (ππΆπ)) = ({π€ β (π(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) β π} β© {π€ β (π(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π})) |
21 | | inrab 4271 |
. . . . 5
β’ ({π€ β (π(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) β π} β© {π€ β (π(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π}) = {π€ β (π(ClWWalksNOnβπΊ)π) β£ ((π€β(π β 2)) β π β§ (π€β(π β 2)) = π)} |
22 | | exmid 894 |
. . . . . . . 8
β’ ((π€β(π β 2)) = π β¨ Β¬ (π€β(π β 2)) = π) |
23 | | ianor 981 |
. . . . . . . . 9
β’ (Β¬
((π€β(π β 2)) β π β§ (π€β(π β 2)) = π) β (Β¬ (π€β(π β 2)) β π β¨ Β¬ (π€β(π β 2)) = π)) |
24 | | nne 2948 |
. . . . . . . . . 10
β’ (Β¬
(π€β(π β 2)) β π β (π€β(π β 2)) = π) |
25 | 24 | orbi1i 913 |
. . . . . . . . 9
β’ ((Β¬
(π€β(π β 2)) β π β¨ Β¬ (π€β(π β 2)) = π) β ((π€β(π β 2)) = π β¨ Β¬ (π€β(π β 2)) = π)) |
26 | 23, 25 | bitri 275 |
. . . . . . . 8
β’ (Β¬
((π€β(π β 2)) β π β§ (π€β(π β 2)) = π) β ((π€β(π β 2)) = π β¨ Β¬ (π€β(π β 2)) = π)) |
27 | 22, 26 | mpbir 230 |
. . . . . . 7
β’ Β¬
((π€β(π β 2)) β π β§ (π€β(π β 2)) = π) |
28 | 27 | rgenw 3069 |
. . . . . 6
β’
βπ€ β
(π(ClWWalksNOnβπΊ)π) Β¬ ((π€β(π β 2)) β π β§ (π€β(π β 2)) = π) |
29 | | rabeq0 4349 |
. . . . . 6
β’ ({π€ β (π(ClWWalksNOnβπΊ)π) β£ ((π€β(π β 2)) β π β§ (π€β(π β 2)) = π)} = β
β βπ€ β (π(ClWWalksNOnβπΊ)π) Β¬ ((π€β(π β 2)) β π β§ (π€β(π β 2)) = π)) |
30 | 28, 29 | mpbir 230 |
. . . . 5
β’ {π€ β (π(ClWWalksNOnβπΊ)π) β£ ((π€β(π β 2)) β π β§ (π€β(π β 2)) = π)} = β
|
31 | 21, 30 | eqtri 2765 |
. . . 4
β’ ({π€ β (π(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) β π} β© {π€ β (π(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π}) = β
|
32 | 20, 31 | eqtrdi 2793 |
. . 3
β’ (((πΊ β FinUSGraph β§ π β π) β§ π β (β€β₯β2))
β ((ππ»π) β© (ππΆπ)) = β
) |
33 | | hashun 14289 |
. . 3
β’ (((ππ»π) β Fin β§ (ππΆπ) β Fin β§ ((ππ»π) β© (ππΆπ)) = β
) β (β―β((ππ»π) βͺ (ππΆπ))) = ((β―β(ππ»π)) + (β―β(ππΆπ)))) |
34 | 14, 19, 32, 33 | syl3anc 1372 |
. 2
β’ (((πΊ β FinUSGraph β§ π β π) β§ π β (β€β₯β2))
β (β―β((ππ»π) βͺ (ππΆπ))) = ((β―β(ππ»π)) + (β―β(ππΆπ)))) |
35 | 5, 34 | eqtrd 2777 |
1
β’ (((πΊ β FinUSGraph β§ π β π) β§ π β (β€β₯β2))
β (β―β(π(ClWWalksNOnβπΊ)π)) = ((β―β(ππ»π)) + (β―β(ππΆπ)))) |