Step | Hyp | Ref
| Expression |
1 | | lfuhgr1v0e.i |
. . . . . 6
β’ πΌ = (iEdgβπΊ) |
2 | 1 | a1i 11 |
. . . . 5
β’ ((πΊ β UHGraph β§
(β―βπ) = 1)
β πΌ =
(iEdgβπΊ)) |
3 | 1 | dmeqi 5861 |
. . . . . 6
β’ dom πΌ = dom (iEdgβπΊ) |
4 | 3 | a1i 11 |
. . . . 5
β’ ((πΊ β UHGraph β§
(β―βπ) = 1)
β dom πΌ = dom
(iEdgβπΊ)) |
5 | | lfuhgr1v0e.e |
. . . . . 6
β’ πΈ = {π₯ β π« π β£ 2 β€ (β―βπ₯)} |
6 | | lfuhgr1v0e.v |
. . . . . . . . . 10
β’ π = (VtxβπΊ) |
7 | 6 | fvexi 6857 |
. . . . . . . . 9
β’ π β V |
8 | | hash1snb 14325 |
. . . . . . . . 9
β’ (π β V β
((β―βπ) = 1
β βπ£ π = {π£})) |
9 | 7, 8 | ax-mp 5 |
. . . . . . . 8
β’
((β―βπ) =
1 β βπ£ π = {π£}) |
10 | | pweq 4575 |
. . . . . . . . . . . 12
β’ (π = {π£} β π« π = π« {π£}) |
11 | 10 | rabeqdv 3421 |
. . . . . . . . . . 11
β’ (π = {π£} β {π₯ β π« π β£ 2 β€ (β―βπ₯)} = {π₯ β π« {π£} β£ 2 β€ (β―βπ₯)}) |
12 | | 2pos 12261 |
. . . . . . . . . . . . . . 15
β’ 0 <
2 |
13 | | 0re 11162 |
. . . . . . . . . . . . . . . 16
β’ 0 β
β |
14 | | 2re 12232 |
. . . . . . . . . . . . . . . 16
β’ 2 β
β |
15 | 13, 14 | ltnlei 11281 |
. . . . . . . . . . . . . . 15
β’ (0 < 2
β Β¬ 2 β€ 0) |
16 | 12, 15 | mpbi 229 |
. . . . . . . . . . . . . 14
β’ Β¬ 2
β€ 0 |
17 | | 1lt2 12329 |
. . . . . . . . . . . . . . 15
β’ 1 <
2 |
18 | | 1re 11160 |
. . . . . . . . . . . . . . . 16
β’ 1 β
β |
19 | 18, 14 | ltnlei 11281 |
. . . . . . . . . . . . . . 15
β’ (1 < 2
β Β¬ 2 β€ 1) |
20 | 17, 19 | mpbi 229 |
. . . . . . . . . . . . . 14
β’ Β¬ 2
β€ 1 |
21 | | 0ex 5265 |
. . . . . . . . . . . . . . 15
β’ β
β V |
22 | | vsnex 5387 |
. . . . . . . . . . . . . . 15
β’ {π£} β V |
23 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = β
β
(β―βπ₯) =
(β―ββ
)) |
24 | | hash0 14273 |
. . . . . . . . . . . . . . . . . 18
β’
(β―ββ
) = 0 |
25 | 23, 24 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = β
β
(β―βπ₯) =
0) |
26 | 25 | breq2d 5118 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = β
β (2 β€
(β―βπ₯) β 2
β€ 0)) |
27 | 26 | notbid 318 |
. . . . . . . . . . . . . . 15
β’ (π₯ = β
β (Β¬ 2 β€
(β―βπ₯) β
Β¬ 2 β€ 0)) |
28 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = {π£} β (β―βπ₯) = (β―β{π£})) |
29 | | hashsng 14275 |
. . . . . . . . . . . . . . . . . . 19
β’ (π£ β V β
(β―β{π£}) =
1) |
30 | 29 | elv 3450 |
. . . . . . . . . . . . . . . . . 18
β’
(β―β{π£})
= 1 |
31 | 28, 30 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = {π£} β (β―βπ₯) = 1) |
32 | 31 | breq2d 5118 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = {π£} β (2 β€ (β―βπ₯) β 2 β€
1)) |
33 | 32 | notbid 318 |
. . . . . . . . . . . . . . 15
β’ (π₯ = {π£} β (Β¬ 2 β€ (β―βπ₯) β Β¬ 2 β€
1)) |
34 | 21, 22, 27, 33 | ralpr 4662 |
. . . . . . . . . . . . . 14
β’
(βπ₯ β
{β
, {π£}} Β¬ 2 β€
(β―βπ₯) β
(Β¬ 2 β€ 0 β§ Β¬ 2 β€ 1)) |
35 | 16, 20, 34 | mpbir2an 710 |
. . . . . . . . . . . . 13
β’
βπ₯ β
{β
, {π£}} Β¬ 2 β€
(β―βπ₯) |
36 | | pwsn 4858 |
. . . . . . . . . . . . . 14
β’ π«
{π£} = {β
, {π£}} |
37 | 36 | raleqi 3310 |
. . . . . . . . . . . . 13
β’
(βπ₯ β
π« {π£} Β¬ 2 β€
(β―βπ₯) β
βπ₯ β {β
,
{π£}} Β¬ 2 β€
(β―βπ₯)) |
38 | 35, 37 | mpbir 230 |
. . . . . . . . . . . 12
β’
βπ₯ β
π« {π£} Β¬ 2 β€
(β―βπ₯) |
39 | | rabeq0 4345 |
. . . . . . . . . . . 12
β’ ({π₯ β π« {π£} β£ 2 β€
(β―βπ₯)} =
β
β βπ₯
β π« {π£} Β¬
2 β€ (β―βπ₯)) |
40 | 38, 39 | mpbir 230 |
. . . . . . . . . . 11
β’ {π₯ β π« {π£} β£ 2 β€
(β―βπ₯)} =
β
|
41 | 11, 40 | eqtrdi 2789 |
. . . . . . . . . 10
β’ (π = {π£} β {π₯ β π« π β£ 2 β€ (β―βπ₯)} = β
) |
42 | 41 | a1d 25 |
. . . . . . . . 9
β’ (π = {π£} β (πΊ β UHGraph β {π₯ β π« π β£ 2 β€ (β―βπ₯)} = β
)) |
43 | 42 | exlimiv 1934 |
. . . . . . . 8
β’
(βπ£ π = {π£} β (πΊ β UHGraph β {π₯ β π« π β£ 2 β€ (β―βπ₯)} = β
)) |
44 | 9, 43 | sylbi 216 |
. . . . . . 7
β’
((β―βπ) =
1 β (πΊ β UHGraph
β {π₯ β π«
π β£ 2 β€
(β―βπ₯)} =
β
)) |
45 | 44 | impcom 409 |
. . . . . 6
β’ ((πΊ β UHGraph β§
(β―βπ) = 1)
β {π₯ β π«
π β£ 2 β€
(β―βπ₯)} =
β
) |
46 | 5, 45 | eqtrid 2785 |
. . . . 5
β’ ((πΊ β UHGraph β§
(β―βπ) = 1)
β πΈ =
β
) |
47 | 2, 4, 46 | feq123d 6658 |
. . . 4
β’ ((πΊ β UHGraph β§
(β―βπ) = 1)
β (πΌ:dom πΌβΆπΈ β (iEdgβπΊ):dom (iEdgβπΊ)βΆβ
)) |
48 | 47 | biimp3a 1470 |
. . 3
β’ ((πΊ β UHGraph β§
(β―βπ) = 1 β§
πΌ:dom πΌβΆπΈ) β (iEdgβπΊ):dom (iEdgβπΊ)βΆβ
) |
49 | | f00 6725 |
. . . 4
β’
((iEdgβπΊ):dom
(iEdgβπΊ)βΆβ
β ((iEdgβπΊ) = β
β§ dom
(iEdgβπΊ) =
β
)) |
50 | 49 | simplbi 499 |
. . 3
β’
((iEdgβπΊ):dom
(iEdgβπΊ)βΆβ
β (iEdgβπΊ) = β
) |
51 | 48, 50 | syl 17 |
. 2
β’ ((πΊ β UHGraph β§
(β―βπ) = 1 β§
πΌ:dom πΌβΆπΈ) β (iEdgβπΊ) = β
) |
52 | | uhgriedg0edg0 28120 |
. . 3
β’ (πΊ β UHGraph β
((EdgβπΊ) = β
β (iEdgβπΊ) =
β
)) |
53 | 52 | 3ad2ant1 1134 |
. 2
β’ ((πΊ β UHGraph β§
(β―βπ) = 1 β§
πΌ:dom πΌβΆπΈ) β ((EdgβπΊ) = β
β (iEdgβπΊ) = β
)) |
54 | 51, 53 | mpbird 257 |
1
β’ ((πΊ β UHGraph β§
(β―βπ) = 1 β§
πΌ:dom πΌβΆπΈ) β (EdgβπΊ) = β
) |