Step | Hyp | Ref
| Expression |
1 | | elopab 5527 |
. . . . 5
β’ (π β {β¨π£, πβ© β£ π:β
βΆβ
} β βπ£βπ(π = β¨π£, πβ© β§ π:β
βΆβ
)) |
2 | | f0bi 6774 |
. . . . . . . . . 10
β’ (π:β
βΆβ
β
π =
β
) |
3 | | opeq2 4874 |
. . . . . . . . . . . 12
β’ (π = β
β β¨π£, πβ© = β¨π£, β
β©) |
4 | | usgr0eop 28541 |
. . . . . . . . . . . . 13
β’ (π£ β V β β¨π£, β
β© β
USGraph) |
5 | 4 | elv 3480 |
. . . . . . . . . . . 12
β’
β¨π£,
β
β© β USGraph |
6 | 3, 5 | eqeltrdi 2841 |
. . . . . . . . . . 11
β’ (π = β
β β¨π£, πβ© β USGraph) |
7 | | vex 3478 |
. . . . . . . . . . . . 13
β’ π£ β V |
8 | | vex 3478 |
. . . . . . . . . . . . 13
β’ π β V |
9 | 7, 8 | opiedgfvi 28308 |
. . . . . . . . . . . 12
β’
(iEdgββ¨π£,
πβ©) = π |
10 | | id 22 |
. . . . . . . . . . . 12
β’ (π = β
β π = β
) |
11 | 9, 10 | eqtrid 2784 |
. . . . . . . . . . 11
β’ (π = β
β
(iEdgββ¨π£, πβ©) =
β
) |
12 | 6, 11 | jca 512 |
. . . . . . . . . 10
β’ (π = β
β (β¨π£, πβ© β USGraph β§
(iEdgββ¨π£, πβ©) =
β
)) |
13 | 2, 12 | sylbi 216 |
. . . . . . . . 9
β’ (π:β
βΆβ
β
(β¨π£, πβ© β USGraph β§
(iEdgββ¨π£, πβ©) =
β
)) |
14 | 13 | adantl 482 |
. . . . . . . 8
β’ ((π = β¨π£, πβ© β§ π:β
βΆβ
) β (β¨π£, πβ© β USGraph β§
(iEdgββ¨π£, πβ©) =
β
)) |
15 | | eleq1 2821 |
. . . . . . . . . 10
β’ (π = β¨π£, πβ© β (π β USGraph β β¨π£, πβ© β USGraph)) |
16 | | fveqeq2 6900 |
. . . . . . . . . 10
β’ (π = β¨π£, πβ© β ((iEdgβπ) = β
β (iEdgββ¨π£, πβ©) = β
)) |
17 | 15, 16 | anbi12d 631 |
. . . . . . . . 9
β’ (π = β¨π£, πβ© β ((π β USGraph β§ (iEdgβπ) = β
) β (β¨π£, πβ© β USGraph β§
(iEdgββ¨π£, πβ©) =
β
))) |
18 | 17 | adantr 481 |
. . . . . . . 8
β’ ((π = β¨π£, πβ© β§ π:β
βΆβ
) β ((π β USGraph β§
(iEdgβπ) = β
)
β (β¨π£, πβ© β USGraph β§
(iEdgββ¨π£, πβ©) =
β
))) |
19 | 14, 18 | mpbird 256 |
. . . . . . 7
β’ ((π = β¨π£, πβ© β§ π:β
βΆβ
) β (π β USGraph β§
(iEdgβπ) =
β
)) |
20 | | fveqeq2 6900 |
. . . . . . . 8
β’ (π = π β ((iEdgβπ) = β
β (iEdgβπ) = β
)) |
21 | 20 | elrab 3683 |
. . . . . . 7
β’ (π β {π β USGraph β£ (iEdgβπ) = β
} β (π β USGraph β§
(iEdgβπ) =
β
)) |
22 | 19, 21 | sylibr 233 |
. . . . . 6
β’ ((π = β¨π£, πβ© β§ π:β
βΆβ
) β π β {π β USGraph β£ (iEdgβπ) = β
}) |
23 | 22 | exlimivv 1935 |
. . . . 5
β’
(βπ£βπ(π = β¨π£, πβ© β§ π:β
βΆβ
) β π β {π β USGraph β£ (iEdgβπ) = β
}) |
24 | 1, 23 | sylbi 216 |
. . . 4
β’ (π β {β¨π£, πβ© β£ π:β
βΆβ
} β π β {π β USGraph β£ (iEdgβπ) = β
}) |
25 | 24 | ssriv 3986 |
. . 3
β’
{β¨π£, πβ© β£ π:β
βΆβ
} β
{π β USGraph β£
(iEdgβπ) =
β
} |
26 | | eqid 2732 |
. . . 4
β’
{β¨π£, πβ© β£ π:β
βΆβ
} =
{β¨π£, πβ© β£ π:β
βΆβ
} |
27 | 26 | griedg0prc 28559 |
. . 3
β’
{β¨π£, πβ© β£ π:β
βΆβ
} β
V |
28 | | prcssprc 5325 |
. . 3
β’
(({β¨π£, πβ© β£ π:β
βΆβ
} β
{π β USGraph β£
(iEdgβπ) = β
}
β§ {β¨π£, πβ© β£ π:β
βΆβ
} β
V) β {π β USGraph
β£ (iEdgβπ) =
β
} β V) |
29 | 25, 27, 28 | mp2an 690 |
. 2
β’ {π β USGraph β£
(iEdgβπ) = β
}
β V |
30 | | df-3an 1089 |
. . . . . . . 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 12552 |
. . . . . . 7
β’ 0 β
β0* |
34 | | ibar 529 |
. . . . . . 7
β’ ((π β USGraph β§ 0 β
β0*) β (βπ£ β (Vtxβπ)((VtxDegβπ)βπ£) = 0 β ((π β USGraph β§ 0 β
β0*) β§ βπ£ β (Vtxβπ)((VtxDegβπ)βπ£) = 0))) |
35 | 33, 34 | mpan2 689 |
. . . . . 6
β’ (π β USGraph β
(βπ£ β
(Vtxβπ)((VtxDegβπ)βπ£) = 0 β ((π β USGraph β§ 0 β
β0*) β§ βπ£ β (Vtxβπ)((VtxDegβπ)βπ£) = 0))) |
36 | | eqid 2732 |
. . . . . . . 8
β’
(Vtxβπ) =
(Vtxβπ) |
37 | | eqid 2732 |
. . . . . . . 8
β’
(VtxDegβπ) =
(VtxDegβπ) |
38 | 36, 37 | isrusgr0 28861 |
. . . . . . 7
β’ ((π β USGraph β§ 0 β
β0*) β (π RegUSGraph 0 β (π β USGraph β§ 0 β
β0* β§ βπ£ β (Vtxβπ)((VtxDegβπ)βπ£) = 0))) |
39 | 33, 38 | mpan2 689 |
. . . . . 6
β’ (π β USGraph β (π RegUSGraph 0 β (π β USGraph β§ 0 β
β0* β§ βπ£ β (Vtxβπ)((VtxDegβπ)βπ£) = 0))) |
40 | 32, 35, 39 | 3bitr4d 310 |
. . . . 5
β’ (π β USGraph β
(βπ£ β
(Vtxβπ)((VtxDegβπ)βπ£) = 0 β π RegUSGraph 0)) |
41 | 40 | rabbiia 3436 |
. . . 4
β’ {π β USGraph β£
βπ£ β
(Vtxβπ)((VtxDegβπ)βπ£) = 0} = {π β USGraph β£ π RegUSGraph 0} |
42 | | usgr0edg0rusgr 28870 |
. . . . . 6
β’ (π β USGraph β (π RegUSGraph 0 β
(Edgβπ) =
β
)) |
43 | | usgruhgr 28481 |
. . . . . . 7
β’ (π β USGraph β π β
UHGraph) |
44 | | uhgriedg0edg0 28425 |
. . . . . . 7
β’ (π β UHGraph β
((Edgβπ) = β
β (iEdgβπ) =
β
)) |
45 | 43, 44 | syl 17 |
. . . . . 6
β’ (π β USGraph β
((Edgβπ) = β
β (iEdgβπ) =
β
)) |
46 | 42, 45 | bitrd 278 |
. . . . 5
β’ (π β USGraph β (π RegUSGraph 0 β
(iEdgβπ) =
β
)) |
47 | 46 | rabbiia 3436 |
. . . 4
β’ {π β USGraph β£ π RegUSGraph 0} = {π β USGraph β£
(iEdgβπ) =
β
} |
48 | 41, 47 | eqtri 2760 |
. . 3
β’ {π β USGraph β£
βπ£ β
(Vtxβπ)((VtxDegβπ)βπ£) = 0} = {π β USGraph β£ (iEdgβπ) = β
} |
49 | | neleq1 3052 |
. . 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 |