| Step | Hyp | Ref
| Expression |
|---|
| 1 | | vdn0conngrv2.v |
. . . 4
β’ π = (VtxβπΊ) |
| 2 | | eqid 2727 |
. . . 4
β’
(iEdgβπΊ) =
(iEdgβπΊ) |
| 3 | | eqid 2727 |
. . . 4
β’ dom
(iEdgβπΊ) = dom
(iEdgβπΊ) |
| 4 | | eqid 2727 |
. . . 4
β’
(VtxDegβπΊ) =
(VtxDegβπΊ) |
| 5 | 1, 2, 3, 4 | vtxdumgrval 29287 |
. . 3
β’ ((πΊ β UMGraph β§ π β π) β ((VtxDegβπΊ)βπ) = (β―β{π₯ β dom (iEdgβπΊ) β£ π β ((iEdgβπΊ)βπ₯)})) |
| 6 | 5 | ad2ant2lr 747 |
. 2
β’ (((πΊ β ConnGraph β§ πΊ β UMGraph) β§ (π β π β§ 1 < (β―βπ))) β ((VtxDegβπΊ)βπ) = (β―β{π₯ β dom (iEdgβπΊ) β£ π β ((iEdgβπΊ)βπ₯)})) |
| 7 | | umgruhgr 28904 |
. . . . . . . 8
β’ (πΊ β UMGraph β πΊ β
UHGraph) |
| 8 | 2 | uhgrfun 28866 |
. . . . . . . 8
β’ (πΊ β UHGraph β Fun
(iEdgβπΊ)) |
| 9 | | funfn 6577 |
. . . . . . . . 9
β’ (Fun
(iEdgβπΊ) β
(iEdgβπΊ) Fn dom
(iEdgβπΊ)) |
| 10 | 9 | biimpi 215 |
. . . . . . . 8
β’ (Fun
(iEdgβπΊ) β
(iEdgβπΊ) Fn dom
(iEdgβπΊ)) |
| 11 | 7, 8, 10 | 3syl 18 |
. . . . . . 7
β’ (πΊ β UMGraph β
(iEdgβπΊ) Fn dom
(iEdgβπΊ)) |
| 12 | 11 | adantl 481 |
. . . . . 6
β’ ((πΊ β ConnGraph β§ πΊ β UMGraph) β
(iEdgβπΊ) Fn dom
(iEdgβπΊ)) |
| 13 | 12 | adantr 480 |
. . . . 5
β’ (((πΊ β ConnGraph β§ πΊ β UMGraph) β§ (π β π β§ 1 < (β―βπ))) β (iEdgβπΊ) Fn dom (iEdgβπΊ)) |
| 14 | | simpl 482 |
. . . . . . 7
β’ ((πΊ β ConnGraph β§ πΊ β UMGraph) β πΊ β
ConnGraph) |
| 15 | 14 | adantr 480 |
. . . . . 6
β’ (((πΊ β ConnGraph β§ πΊ β UMGraph) β§ (π β π β§ 1 < (β―βπ))) β πΊ β ConnGraph) |
| 16 | | simpl 482 |
. . . . . . 7
β’ ((π β π β§ 1 < (β―βπ)) β π β π) |
| 17 | 16 | adantl 481 |
. . . . . 6
β’ (((πΊ β ConnGraph β§ πΊ β UMGraph) β§ (π β π β§ 1 < (β―βπ))) β π β π) |
| 18 | | simprr 772 |
. . . . . 6
β’ (((πΊ β ConnGraph β§ πΊ β UMGraph) β§ (π β π β§ 1 < (β―βπ))) β 1 <
(β―βπ)) |
| 19 | 1, 2 | conngrv2edg 29992 |
. . . . . 6
β’ ((πΊ β ConnGraph β§ π β π β§ 1 < (β―βπ)) β βπ β ran (iEdgβπΊ)π β π) |
| 20 | 15, 17, 18, 19 | syl3anc 1369 |
. . . . 5
β’ (((πΊ β ConnGraph β§ πΊ β UMGraph) β§ (π β π β§ 1 < (β―βπ))) β βπ β ran (iEdgβπΊ)π β π) |
| 21 | | eleq2 2817 |
. . . . . . 7
β’ (π = ((iEdgβπΊ)βπ₯) β (π β π β π β ((iEdgβπΊ)βπ₯))) |
| 22 | 21 | rexrn 7091 |
. . . . . 6
β’
((iEdgβπΊ) Fn
dom (iEdgβπΊ) β
(βπ β ran
(iEdgβπΊ)π β π β βπ₯ β dom (iEdgβπΊ)π β ((iEdgβπΊ)βπ₯))) |
| 23 | 22 | biimpd 228 |
. . . . 5
β’
((iEdgβπΊ) Fn
dom (iEdgβπΊ) β
(βπ β ran
(iEdgβπΊ)π β π β βπ₯ β dom (iEdgβπΊ)π β ((iEdgβπΊ)βπ₯))) |
| 24 | 13, 20, 23 | sylc 65 |
. . . 4
β’ (((πΊ β ConnGraph β§ πΊ β UMGraph) β§ (π β π β§ 1 < (β―βπ))) β βπ₯ β dom (iEdgβπΊ)π β ((iEdgβπΊ)βπ₯)) |
| 25 | | dfrex2 3068 |
. . . 4
β’
(βπ₯ β dom
(iEdgβπΊ)π β ((iEdgβπΊ)βπ₯) β Β¬ βπ₯ β dom (iEdgβπΊ) Β¬ π β ((iEdgβπΊ)βπ₯)) |
| 26 | 24, 25 | sylib 217 |
. . 3
β’ (((πΊ β ConnGraph β§ πΊ β UMGraph) β§ (π β π β§ 1 < (β―βπ))) β Β¬ βπ₯ β dom (iEdgβπΊ) Β¬ π β ((iEdgβπΊ)βπ₯)) |
| 27 | | fvex 6904 |
. . . . . . . 8
β’
(iEdgβπΊ)
β V |
| 28 | 27 | dmex 7911 |
. . . . . . 7
β’ dom
(iEdgβπΊ) β
V |
| 29 | 28 | a1i 11 |
. . . . . 6
β’ (((πΊ β ConnGraph β§ πΊ β UMGraph) β§ (π β π β§ 1 < (β―βπ))) β dom (iEdgβπΊ) β V) |
| 30 | | rabexg 5327 |
. . . . . 6
β’ (dom
(iEdgβπΊ) β V
β {π₯ β dom
(iEdgβπΊ) β£
π β ((iEdgβπΊ)βπ₯)} β V) |
| 31 | | hasheq0 14346 |
. . . . . 6
β’ ({π₯ β dom (iEdgβπΊ) β£ π β ((iEdgβπΊ)βπ₯)} β V β ((β―β{π₯ β dom (iEdgβπΊ) β£ π β ((iEdgβπΊ)βπ₯)}) = 0 β {π₯ β dom (iEdgβπΊ) β£ π β ((iEdgβπΊ)βπ₯)} = β
)) |
| 32 | 29, 30, 31 | 3syl 18 |
. . . . 5
β’ (((πΊ β ConnGraph β§ πΊ β UMGraph) β§ (π β π β§ 1 < (β―βπ))) β
((β―β{π₯ β
dom (iEdgβπΊ) β£
π β ((iEdgβπΊ)βπ₯)}) = 0 β {π₯ β dom (iEdgβπΊ) β£ π β ((iEdgβπΊ)βπ₯)} = β
)) |
| 33 | | rabeq0 4380 |
. . . . 5
β’ ({π₯ β dom (iEdgβπΊ) β£ π β ((iEdgβπΊ)βπ₯)} = β
β βπ₯ β dom (iEdgβπΊ) Β¬ π β ((iEdgβπΊ)βπ₯)) |
| 34 | 32, 33 | bitrdi 287 |
. . . 4
β’ (((πΊ β ConnGraph β§ πΊ β UMGraph) β§ (π β π β§ 1 < (β―βπ))) β
((β―β{π₯ β
dom (iEdgβπΊ) β£
π β ((iEdgβπΊ)βπ₯)}) = 0 β βπ₯ β dom (iEdgβπΊ) Β¬ π β ((iEdgβπΊ)βπ₯))) |
| 35 | 34 | necon3abid 2972 |
. . 3
β’ (((πΊ β ConnGraph β§ πΊ β UMGraph) β§ (π β π β§ 1 < (β―βπ))) β
((β―β{π₯ β
dom (iEdgβπΊ) β£
π β ((iEdgβπΊ)βπ₯)}) β 0 β Β¬ βπ₯ β dom (iEdgβπΊ) Β¬ π β ((iEdgβπΊ)βπ₯))) |
| 36 | 26, 35 | mpbird 257 |
. 2
β’ (((πΊ β ConnGraph β§ πΊ β UMGraph) β§ (π β π β§ 1 < (β―βπ))) β (β―β{π₯ β dom (iEdgβπΊ) β£ π β ((iEdgβπΊ)βπ₯)}) β 0) |
| 37 | 6, 36 | eqnetrd 3003 |
1
β’ (((πΊ β ConnGraph β§ πΊ β UMGraph) β§ (π β π β§ 1 < (β―βπ))) β ((VtxDegβπΊ)βπ) β 0) |
