Step | Hyp | Ref
| Expression |
1 | | elopab 5528 |
. . . . 5
β’ (π β {β¨π£, πβ© β£ π:β
βΆβ
} β βπ£βπ(π = β¨π£, πβ© β§ π:β
βΆβ
)) |
2 | | f0bi 6775 |
. . . . . . . . . 10
β’ (π:β
βΆβ
β
π =
β
) |
3 | | opeq2 4875 |
. . . . . . . . . . . 12
β’ (π = β
β β¨π£, πβ© = β¨π£, β
β©) |
4 | | usgr0eop 28503 |
. . . . . . . . . . . . 13
β’ (π£ β V β β¨π£, β
β© β
USGraph) |
5 | 4 | elv 3481 |
. . . . . . . . . . . 12
β’
β¨π£,
β
β© β USGraph |
6 | 3, 5 | eqeltrdi 2842 |
. . . . . . . . . . 11
β’ (π = β
β β¨π£, πβ© β USGraph) |
7 | | vex 3479 |
. . . . . . . . . . . . 13
β’ π£ β V |
8 | | vex 3479 |
. . . . . . . . . . . . 13
β’ π β V |
9 | 7, 8 | opiedgfvi 28270 |
. . . . . . . . . . . 12
β’
(iEdgββ¨π£,
πβ©) = π |
10 | | id 22 |
. . . . . . . . . . . 12
β’ (π = β
β π = β
) |
11 | 9, 10 | eqtrid 2785 |
. . . . . . . . . . 11
β’ (π = β
β
(iEdgββ¨π£, πβ©) =
β
) |
12 | 6, 11 | jca 513 |
. . . . . . . . . 10
β’ (π = β
β (β¨π£, πβ© β USGraph β§
(iEdgββ¨π£, πβ©) =
β
)) |
13 | 2, 12 | sylbi 216 |
. . . . . . . . 9
β’ (π:β
βΆβ
β
(β¨π£, πβ© β USGraph β§
(iEdgββ¨π£, πβ©) =
β
)) |
14 | 13 | adantl 483 |
. . . . . . . 8
β’ ((π = β¨π£, πβ© β§ π:β
βΆβ
) β (β¨π£, πβ© β USGraph β§
(iEdgββ¨π£, πβ©) =
β
)) |
15 | | eleq1 2822 |
. . . . . . . . . 10
β’ (π = β¨π£, πβ© β (π β USGraph β β¨π£, πβ© β USGraph)) |
16 | | fveqeq2 6901 |
. . . . . . . . . 10
β’ (π = β¨π£, πβ© β ((iEdgβπ) = β
β (iEdgββ¨π£, πβ©) = β
)) |
17 | 15, 16 | anbi12d 632 |
. . . . . . . . 9
β’ (π = β¨π£, πβ© β ((π β USGraph β§ (iEdgβπ) = β
) β (β¨π£, πβ© β USGraph β§
(iEdgββ¨π£, πβ©) =
β
))) |
18 | 17 | adantr 482 |
. . . . . . . 8
β’ ((π = β¨π£, πβ© β§ π:β
βΆβ
) β ((π β USGraph β§
(iEdgβπ) = β
)
β (β¨π£, πβ© β USGraph β§
(iEdgββ¨π£, πβ©) =
β
))) |
19 | 14, 18 | mpbird 257 |
. . . . . . 7
β’ ((π = β¨π£, πβ© β§ π:β
βΆβ
) β (π β USGraph β§
(iEdgβπ) =
β
)) |
20 | | fveqeq2 6901 |
. . . . . . . 8
β’ (π = π β ((iEdgβπ) = β
β (iEdgβπ) = β
)) |
21 | 20 | elrab 3684 |
. . . . . . 7
β’ (π β {π β USGraph β£ (iEdgβπ) = β
} β (π β USGraph β§
(iEdgβπ) =
β
)) |
22 | 19, 21 | sylibr 233 |
. . . . . 6
β’ ((π = β¨π£, πβ© β§ π:β
βΆβ
) β π β {π β USGraph β£ (iEdgβπ) = β
}) |
23 | 22 | exlimivv 1936 |
. . . . 5
β’
(βπ£βπ(π = β¨π£, πβ© β§ π:β
βΆβ
) β π β {π β USGraph β£ (iEdgβπ) = β
}) |
24 | 1, 23 | sylbi 216 |
. . . 4
β’ (π β {β¨π£, πβ© β£ π:β
βΆβ
} β π β {π β USGraph β£ (iEdgβπ) = β
}) |
25 | 24 | ssriv 3987 |
. . 3
β’
{β¨π£, πβ© β£ π:β
βΆβ
} β
{π β USGraph β£
(iEdgβπ) =
β
} |
26 | | eqid 2733 |
. . . 4
β’
{β¨π£, πβ© β£ π:β
βΆβ
} =
{β¨π£, πβ© β£ π:β
βΆβ
} |
27 | 26 | griedg0prc 28521 |
. . 3
β’
{β¨π£, πβ© β£ π:β
βΆβ
} β
V |
28 | | prcssprc 5326 |
. . 3
β’
(({β¨π£, πβ© β£ π:β
βΆβ
} β
{π β USGraph β£
(iEdgβπ) = β
}
β§ {β¨π£, πβ© β£ π:β
βΆβ
} β
V) β {π β USGraph
β£ (iEdgβπ) =
β
} β V) |
29 | 25, 27, 28 | mp2an 691 |
. 2
β’ {π β USGraph β£
(iEdgβπ) = β
}
β V |
30 | | df-3an 1090 |
. . . . . . . 8
β’ ((π β USGraph β§ 0 β
β0* β§ βπ£ β (Vtxβπ)((VtxDegβπ)βπ£) = 0) β ((π β USGraph β§ 0 β
β0*) β§ βπ£ β (Vtxβπ)((VtxDegβπ)βπ£) = 0)) |
31 | 30 | bicomi 223 |
. . . . . . 7
β’ (((π β USGraph β§ 0 β
β0*) β§ βπ£ β (Vtxβπ)((VtxDegβπ)βπ£) = 0) β (π β USGraph β§ 0 β
β0* β§ βπ£ β (Vtxβπ)((VtxDegβπ)βπ£) = 0)) |
32 | 31 | a1i 11 |
. . . . . 6
β’ (π β USGraph β (((π β USGraph β§ 0 β
β0*) β§ βπ£ β (Vtxβπ)((VtxDegβπ)βπ£) = 0) β (π β USGraph β§ 0 β
β0* β§ βπ£ β (Vtxβπ)((VtxDegβπ)βπ£) = 0))) |
33 | | 0xnn0 12550 |
. . . . . . 7
β’ 0 β
β0* |
34 | | ibar 530 |
. . . . . . 7
β’ ((π β USGraph β§ 0 β
β0*) β (βπ£ β (Vtxβπ)((VtxDegβπ)βπ£) = 0 β ((π β USGraph β§ 0 β
β0*) β§ βπ£ β (Vtxβπ)((VtxDegβπ)βπ£) = 0))) |
35 | 33, 34 | mpan2 690 |
. . . . . 6
β’ (π β USGraph β
(βπ£ β
(Vtxβπ)((VtxDegβπ)βπ£) = 0 β ((π β USGraph β§ 0 β
β0*) β§ βπ£ β (Vtxβπ)((VtxDegβπ)βπ£) = 0))) |
36 | | eqid 2733 |
. . . . . . . 8
β’
(Vtxβπ) =
(Vtxβπ) |
37 | | eqid 2733 |
. . . . . . . 8
β’
(VtxDegβπ) =
(VtxDegβπ) |
38 | 36, 37 | isrusgr0 28823 |
. . . . . . 7
β’ ((π β USGraph β§ 0 β
β0*) β (π RegUSGraph 0 β (π β USGraph β§ 0 β
β0* β§ βπ£ β (Vtxβπ)((VtxDegβπ)βπ£) = 0))) |
39 | 33, 38 | mpan2 690 |
. . . . . 6
β’ (π β USGraph β (π RegUSGraph 0 β (π β USGraph β§ 0 β
β0* β§ βπ£ β (Vtxβπ)((VtxDegβπ)βπ£) = 0))) |
40 | 32, 35, 39 | 3bitr4d 311 |
. . . . 5
β’ (π β USGraph β
(βπ£ β
(Vtxβπ)((VtxDegβπ)βπ£) = 0 β π RegUSGraph 0)) |
41 | 40 | rabbiia 3437 |
. . . 4
β’ {π β USGraph β£
βπ£ β
(Vtxβπ)((VtxDegβπ)βπ£) = 0} = {π β USGraph β£ π RegUSGraph 0} |
42 | | usgr0edg0rusgr 28832 |
. . . . . 6
β’ (π β USGraph β (π RegUSGraph 0 β
(Edgβπ) =
β
)) |
43 | | usgruhgr 28443 |
. . . . . . 7
β’ (π β USGraph β π β
UHGraph) |
44 | | uhgriedg0edg0 28387 |
. . . . . . 7
β’ (π β UHGraph β
((Edgβπ) = β
β (iEdgβπ) =
β
)) |
45 | 43, 44 | syl 17 |
. . . . . 6
β’ (π β USGraph β
((Edgβπ) = β
β (iEdgβπ) =
β
)) |
46 | 42, 45 | bitrd 279 |
. . . . 5
β’ (π β USGraph β (π RegUSGraph 0 β
(iEdgβπ) =
β
)) |
47 | 46 | rabbiia 3437 |
. . . 4
β’ {π β USGraph β£ π RegUSGraph 0} = {π β USGraph β£
(iEdgβπ) =
β
} |
48 | 41, 47 | eqtri 2761 |
. . 3
β’ {π β USGraph β£
βπ£ β
(Vtxβπ)((VtxDegβπ)βπ£) = 0} = {π β USGraph β£ (iEdgβπ) = β
} |
49 | | neleq1 3053 |
. . 3
β’ ({π β USGraph β£
βπ£ β
(Vtxβπ)((VtxDegβπ)βπ£) = 0} = {π β USGraph β£ (iEdgβπ) = β
} β ({π β USGraph β£
βπ£ β
(Vtxβπ)((VtxDegβπ)βπ£) = 0} β V β {π β USGraph β£ (iEdgβπ) = β
} β
V)) |
50 | 48, 49 | ax-mp 5 |
. 2
β’ ({π β USGraph β£
βπ£ β
(Vtxβπ)((VtxDegβπ)βπ£) = 0} β V β {π β USGraph β£ (iEdgβπ) = β
} β
V) |
51 | 29, 50 | mpbir 230 |
1
β’ {π β USGraph β£
βπ£ β
(Vtxβπ)((VtxDegβπ)βπ£) = 0} β V |