Step | Hyp | Ref
| Expression |
1 | | vtxd0nedgb.d |
. . . . 5
β’ π· = (VtxDegβπΊ) |
2 | 1 | fveq1i 6893 |
. . . 4
β’ (π·βπ) = ((VtxDegβπΊ)βπ) |
3 | | vtxd0nedgb.v |
. . . . 5
β’ π = (VtxβπΊ) |
4 | | vtxd0nedgb.i |
. . . . 5
β’ πΌ = (iEdgβπΊ) |
5 | | eqid 2733 |
. . . . 5
β’ dom πΌ = dom πΌ |
6 | 3, 4, 5 | vtxdgval 28725 |
. . . 4
β’ (π β π β ((VtxDegβπΊ)βπ) = ((β―β{π β dom πΌ β£ π β (πΌβπ)}) +π
(β―β{π β
dom πΌ β£ (πΌβπ) = {π}}))) |
7 | 2, 6 | eqtrid 2785 |
. . 3
β’ (π β π β (π·βπ) = ((β―β{π β dom πΌ β£ π β (πΌβπ)}) +π
(β―β{π β
dom πΌ β£ (πΌβπ) = {π}}))) |
8 | 7 | eqeq1d 2735 |
. 2
β’ (π β π β ((π·βπ) = 0 β ((β―β{π β dom πΌ β£ π β (πΌβπ)}) +π
(β―β{π β
dom πΌ β£ (πΌβπ) = {π}})) = 0)) |
9 | 4 | fvexi 6906 |
. . . . . . 7
β’ πΌ β V |
10 | 9 | dmex 7902 |
. . . . . 6
β’ dom πΌ β V |
11 | 10 | rabex 5333 |
. . . . 5
β’ {π β dom πΌ β£ π β (πΌβπ)} β V |
12 | | hashxnn0 14299 |
. . . . 5
β’ ({π β dom πΌ β£ π β (πΌβπ)} β V β (β―β{π β dom πΌ β£ π β (πΌβπ)}) β
β0*) |
13 | 11, 12 | ax-mp 5 |
. . . 4
β’
(β―β{π
β dom πΌ β£ π β (πΌβπ)}) β
β0* |
14 | 10 | rabex 5333 |
. . . . 5
β’ {π β dom πΌ β£ (πΌβπ) = {π}} β V |
15 | | hashxnn0 14299 |
. . . . 5
β’ ({π β dom πΌ β£ (πΌβπ) = {π}} β V β (β―β{π β dom πΌ β£ (πΌβπ) = {π}}) β
β0*) |
16 | 14, 15 | ax-mp 5 |
. . . 4
β’
(β―β{π
β dom πΌ β£ (πΌβπ) = {π}}) β
β0* |
17 | 13, 16 | pm3.2i 472 |
. . 3
β’
((β―β{π
β dom πΌ β£ π β (πΌβπ)}) β β0*
β§ (β―β{π
β dom πΌ β£ (πΌβπ) = {π}}) β
β0*) |
18 | | xnn0xadd0 13226 |
. . 3
β’
(((β―β{π
β dom πΌ β£ π β (πΌβπ)}) β β0*
β§ (β―β{π
β dom πΌ β£ (πΌβπ) = {π}}) β β0*)
β (((β―β{π
β dom πΌ β£ π β (πΌβπ)}) +π
(β―β{π β
dom πΌ β£ (πΌβπ) = {π}})) = 0 β ((β―β{π β dom πΌ β£ π β (πΌβπ)}) = 0 β§ (β―β{π β dom πΌ β£ (πΌβπ) = {π}}) = 0))) |
19 | 17, 18 | mp1i 13 |
. 2
β’ (π β π β (((β―β{π β dom πΌ β£ π β (πΌβπ)}) +π
(β―β{π β
dom πΌ β£ (πΌβπ) = {π}})) = 0 β ((β―β{π β dom πΌ β£ π β (πΌβπ)}) = 0 β§ (β―β{π β dom πΌ β£ (πΌβπ) = {π}}) = 0))) |
20 | | hasheq0 14323 |
. . . . . 6
β’ ({π β dom πΌ β£ π β (πΌβπ)} β V β ((β―β{π β dom πΌ β£ π β (πΌβπ)}) = 0 β {π β dom πΌ β£ π β (πΌβπ)} = β
)) |
21 | 11, 20 | ax-mp 5 |
. . . . 5
β’
((β―β{π
β dom πΌ β£ π β (πΌβπ)}) = 0 β {π β dom πΌ β£ π β (πΌβπ)} = β
) |
22 | | hasheq0 14323 |
. . . . . 6
β’ ({π β dom πΌ β£ (πΌβπ) = {π}} β V β ((β―β{π β dom πΌ β£ (πΌβπ) = {π}}) = 0 β {π β dom πΌ β£ (πΌβπ) = {π}} = β
)) |
23 | 14, 22 | ax-mp 5 |
. . . . 5
β’
((β―β{π
β dom πΌ β£ (πΌβπ) = {π}}) = 0 β {π β dom πΌ β£ (πΌβπ) = {π}} = β
) |
24 | 21, 23 | anbi12i 628 |
. . . 4
β’
(((β―β{π
β dom πΌ β£ π β (πΌβπ)}) = 0 β§ (β―β{π β dom πΌ β£ (πΌβπ) = {π}}) = 0) β ({π β dom πΌ β£ π β (πΌβπ)} = β
β§ {π β dom πΌ β£ (πΌβπ) = {π}} = β
)) |
25 | | rabeq0 4385 |
. . . . 5
β’ ({π β dom πΌ β£ π β (πΌβπ)} = β
β βπ β dom πΌ Β¬ π β (πΌβπ)) |
26 | | rabeq0 4385 |
. . . . 5
β’ ({π β dom πΌ β£ (πΌβπ) = {π}} = β
β βπ β dom πΌ Β¬ (πΌβπ) = {π}) |
27 | 25, 26 | anbi12i 628 |
. . . 4
β’ (({π β dom πΌ β£ π β (πΌβπ)} = β
β§ {π β dom πΌ β£ (πΌβπ) = {π}} = β
) β (βπ β dom πΌ Β¬ π β (πΌβπ) β§ βπ β dom πΌ Β¬ (πΌβπ) = {π})) |
28 | | ralnex 3073 |
. . . . . . 7
β’
(βπ β
dom πΌ Β¬ (π β (πΌβπ) β¨ (πΌβπ) = {π}) β Β¬ βπ β dom πΌ(π β (πΌβπ) β¨ (πΌβπ) = {π})) |
29 | 28 | bicomi 223 |
. . . . . 6
β’ (Β¬
βπ β dom πΌ(π β (πΌβπ) β¨ (πΌβπ) = {π}) β βπ β dom πΌ Β¬ (π β (πΌβπ) β¨ (πΌβπ) = {π})) |
30 | | ioran 983 |
. . . . . . 7
β’ (Β¬
(π β (πΌβπ) β¨ (πΌβπ) = {π}) β (Β¬ π β (πΌβπ) β§ Β¬ (πΌβπ) = {π})) |
31 | 30 | ralbii 3094 |
. . . . . 6
β’
(βπ β
dom πΌ Β¬ (π β (πΌβπ) β¨ (πΌβπ) = {π}) β βπ β dom πΌ(Β¬ π β (πΌβπ) β§ Β¬ (πΌβπ) = {π})) |
32 | | r19.26 3112 |
. . . . . 6
β’
(βπ β
dom πΌ(Β¬ π β (πΌβπ) β§ Β¬ (πΌβπ) = {π}) β (βπ β dom πΌ Β¬ π β (πΌβπ) β§ βπ β dom πΌ Β¬ (πΌβπ) = {π})) |
33 | 29, 31, 32 | 3bitri 297 |
. . . . 5
β’ (Β¬
βπ β dom πΌ(π β (πΌβπ) β¨ (πΌβπ) = {π}) β (βπ β dom πΌ Β¬ π β (πΌβπ) β§ βπ β dom πΌ Β¬ (πΌβπ) = {π})) |
34 | 33 | bicomi 223 |
. . . 4
β’
((βπ β
dom πΌ Β¬ π β (πΌβπ) β§ βπ β dom πΌ Β¬ (πΌβπ) = {π}) β Β¬ βπ β dom πΌ(π β (πΌβπ) β¨ (πΌβπ) = {π})) |
35 | 24, 27, 34 | 3bitri 297 |
. . 3
β’
(((β―β{π
β dom πΌ β£ π β (πΌβπ)}) = 0 β§ (β―β{π β dom πΌ β£ (πΌβπ) = {π}}) = 0) β Β¬ βπ β dom πΌ(π β (πΌβπ) β¨ (πΌβπ) = {π})) |
36 | | orcom 869 |
. . . . . 6
β’ ((π β (πΌβπ) β¨ (πΌβπ) = {π}) β ((πΌβπ) = {π} β¨ π β (πΌβπ))) |
37 | | snidg 4663 |
. . . . . . . 8
β’ (π β π β π β {π}) |
38 | | eleq2 2823 |
. . . . . . . 8
β’ ((πΌβπ) = {π} β (π β (πΌβπ) β π β {π})) |
39 | 37, 38 | syl5ibrcom 246 |
. . . . . . 7
β’ (π β π β ((πΌβπ) = {π} β π β (πΌβπ))) |
40 | | pm4.72 949 |
. . . . . . 7
β’ (((πΌβπ) = {π} β π β (πΌβπ)) β (π β (πΌβπ) β ((πΌβπ) = {π} β¨ π β (πΌβπ)))) |
41 | 39, 40 | sylib 217 |
. . . . . 6
β’ (π β π β (π β (πΌβπ) β ((πΌβπ) = {π} β¨ π β (πΌβπ)))) |
42 | 36, 41 | bitr4id 290 |
. . . . 5
β’ (π β π β ((π β (πΌβπ) β¨ (πΌβπ) = {π}) β π β (πΌβπ))) |
43 | 42 | rexbidv 3179 |
. . . 4
β’ (π β π β (βπ β dom πΌ(π β (πΌβπ) β¨ (πΌβπ) = {π}) β βπ β dom πΌ π β (πΌβπ))) |
44 | 43 | notbid 318 |
. . 3
β’ (π β π β (Β¬ βπ β dom πΌ(π β (πΌβπ) β¨ (πΌβπ) = {π}) β Β¬ βπ β dom πΌ π β (πΌβπ))) |
45 | 35, 44 | bitrid 283 |
. 2
β’ (π β π β (((β―β{π β dom πΌ β£ π β (πΌβπ)}) = 0 β§ (β―β{π β dom πΌ β£ (πΌβπ) = {π}}) = 0) β Β¬ βπ β dom πΌ π β (πΌβπ))) |
46 | 8, 19, 45 | 3bitrd 305 |
1
β’ (π β π β ((π·βπ) = 0 β Β¬ βπ β dom πΌ π β (πΌβπ))) |