Step | Hyp | Ref
| Expression |
1 | | umgr2v2evtx.g |
. . . 4
β’ πΊ = β¨π, {β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}β© |
2 | 1 | umgr2v2e 28515 |
. . 3
β’ (((π β π β§ π΄ β π β§ π΅ β π) β§ π΄ β π΅) β πΊ β UMGraph) |
3 | 1 | umgr2v2evtxel 28512 |
. . . . 5
β’ ((π β π β§ π΄ β π) β π΄ β (VtxβπΊ)) |
4 | 3 | 3adant3 1133 |
. . . 4
β’ ((π β π β§ π΄ β π β§ π΅ β π) β π΄ β (VtxβπΊ)) |
5 | 4 | adantr 482 |
. . 3
β’ (((π β π β§ π΄ β π β§ π΅ β π) β§ π΄ β π΅) β π΄ β (VtxβπΊ)) |
6 | | eqid 2733 |
. . . 4
β’
(VtxβπΊ) =
(VtxβπΊ) |
7 | | eqid 2733 |
. . . 4
β’
(iEdgβπΊ) =
(iEdgβπΊ) |
8 | | eqid 2733 |
. . . 4
β’ dom
(iEdgβπΊ) = dom
(iEdgβπΊ) |
9 | | eqid 2733 |
. . . 4
β’
(VtxDegβπΊ) =
(VtxDegβπΊ) |
10 | 6, 7, 8, 9 | vtxdumgrval 28476 |
. . 3
β’ ((πΊ β UMGraph β§ π΄ β (VtxβπΊ)) β ((VtxDegβπΊ)βπ΄) = (β―β{π₯ β dom (iEdgβπΊ) β£ π΄ β ((iEdgβπΊ)βπ₯)})) |
11 | 2, 5, 10 | syl2anc 585 |
. 2
β’ (((π β π β§ π΄ β π β§ π΅ β π) β§ π΄ β π΅) β ((VtxDegβπΊ)βπ΄) = (β―β{π₯ β dom (iEdgβπΊ) β£ π΄ β ((iEdgβπΊ)βπ₯)})) |
12 | 1 | umgr2v2eiedg 28513 |
. . . . . . . 8
β’ ((π β π β§ π΄ β π β§ π΅ β π) β (iEdgβπΊ) = {β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}) |
13 | 12 | dmeqd 5862 |
. . . . . . 7
β’ ((π β π β§ π΄ β π β§ π΅ β π) β dom (iEdgβπΊ) = dom {β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}) |
14 | | prex 5390 |
. . . . . . . 8
β’ {π΄, π΅} β V |
15 | 14, 14 | dmprop 6170 |
. . . . . . 7
β’ dom
{β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©} = {0, 1} |
16 | 13, 15 | eqtrdi 2789 |
. . . . . 6
β’ ((π β π β§ π΄ β π β§ π΅ β π) β dom (iEdgβπΊ) = {0, 1}) |
17 | 12 | fveq1d 6845 |
. . . . . . 7
β’ ((π β π β§ π΄ β π β§ π΅ β π) β ((iEdgβπΊ)βπ₯) = ({β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}βπ₯)) |
18 | 17 | eleq2d 2820 |
. . . . . 6
β’ ((π β π β§ π΄ β π β§ π΅ β π) β (π΄ β ((iEdgβπΊ)βπ₯) β π΄ β ({β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}βπ₯))) |
19 | 16, 18 | rabeqbidv 3423 |
. . . . 5
β’ ((π β π β§ π΄ β π β§ π΅ β π) β {π₯ β dom (iEdgβπΊ) β£ π΄ β ((iEdgβπΊ)βπ₯)} = {π₯ β {0, 1} β£ π΄ β ({β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}βπ₯)}) |
20 | 19 | fveq2d 6847 |
. . . 4
β’ ((π β π β§ π΄ β π β§ π΅ β π) β (β―β{π₯ β dom (iEdgβπΊ) β£ π΄ β ((iEdgβπΊ)βπ₯)}) = (β―β{π₯ β {0, 1} β£ π΄ β ({β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}βπ₯)})) |
21 | | prid1g 4722 |
. . . . . . . . . . 11
β’ (π΄ β π β π΄ β {π΄, π΅}) |
22 | | 0ne1 12229 |
. . . . . . . . . . . 12
β’ 0 β
1 |
23 | | c0ex 11154 |
. . . . . . . . . . . . 13
β’ 0 β
V |
24 | 23, 14 | fvpr1 7140 |
. . . . . . . . . . . 12
β’ (0 β 1
β ({β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}β0) = {π΄, π΅}) |
25 | 22, 24 | ax-mp 5 |
. . . . . . . . . . 11
β’
({β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}β0) = {π΄, π΅} |
26 | 21, 25 | eleqtrrdi 2845 |
. . . . . . . . . 10
β’ (π΄ β π β π΄ β ({β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}β0)) |
27 | | 1ex 11156 |
. . . . . . . . . . . . 13
β’ 1 β
V |
28 | 27, 14 | fvpr2 7142 |
. . . . . . . . . . . 12
β’ (0 β 1
β ({β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}β1) = {π΄, π΅}) |
29 | 22, 28 | ax-mp 5 |
. . . . . . . . . . 11
β’
({β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}β1) = {π΄, π΅} |
30 | 21, 29 | eleqtrrdi 2845 |
. . . . . . . . . 10
β’ (π΄ β π β π΄ β ({β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}β1)) |
31 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π₯ = 0 β ({β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}βπ₯) = ({β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}β0)) |
32 | 31 | eleq2d 2820 |
. . . . . . . . . . 11
β’ (π₯ = 0 β (π΄ β ({β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}βπ₯) β π΄ β ({β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}β0))) |
33 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π₯ = 1 β ({β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}βπ₯) = ({β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}β1)) |
34 | 33 | eleq2d 2820 |
. . . . . . . . . . 11
β’ (π₯ = 1 β (π΄ β ({β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}βπ₯) β π΄ β ({β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}β1))) |
35 | 23, 27, 32, 34 | ralpr 4662 |
. . . . . . . . . 10
β’
(βπ₯ β
{0, 1}π΄ β ({β¨0,
{π΄, π΅}β©, β¨1, {π΄, π΅}β©}βπ₯) β (π΄ β ({β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}β0) β§ π΄ β ({β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}β1))) |
36 | 26, 30, 35 | sylanbrc 584 |
. . . . . . . . 9
β’ (π΄ β π β βπ₯ β {0, 1}π΄ β ({β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}βπ₯)) |
37 | | rabid2 3435 |
. . . . . . . . 9
β’ ({0, 1} =
{π₯ β {0, 1} β£
π΄ β ({β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}βπ₯)} β βπ₯ β {0, 1}π΄ β ({β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}βπ₯)) |
38 | 36, 37 | sylibr 233 |
. . . . . . . 8
β’ (π΄ β π β {0, 1} = {π₯ β {0, 1} β£ π΄ β ({β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}βπ₯)}) |
39 | 38 | eqcomd 2739 |
. . . . . . 7
β’ (π΄ β π β {π₯ β {0, 1} β£ π΄ β ({β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}βπ₯)} = {0, 1}) |
40 | 39 | fveq2d 6847 |
. . . . . 6
β’ (π΄ β π β (β―β{π₯ β {0, 1} β£ π΄ β ({β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}βπ₯)}) = (β―β{0,
1})) |
41 | | prhash2ex 14305 |
. . . . . 6
β’
(β―β{0, 1}) = 2 |
42 | 40, 41 | eqtrdi 2789 |
. . . . 5
β’ (π΄ β π β (β―β{π₯ β {0, 1} β£ π΄ β ({β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}βπ₯)}) = 2) |
43 | 42 | 3ad2ant2 1135 |
. . . 4
β’ ((π β π β§ π΄ β π β§ π΅ β π) β (β―β{π₯ β {0, 1} β£ π΄ β ({β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}βπ₯)}) = 2) |
44 | 20, 43 | eqtrd 2773 |
. . 3
β’ ((π β π β§ π΄ β π β§ π΅ β π) β (β―β{π₯ β dom (iEdgβπΊ) β£ π΄ β ((iEdgβπΊ)βπ₯)}) = 2) |
45 | 44 | adantr 482 |
. 2
β’ (((π β π β§ π΄ β π β§ π΅ β π) β§ π΄ β π΅) β (β―β{π₯ β dom (iEdgβπΊ) β£ π΄ β ((iEdgβπΊ)βπ₯)}) = 2) |
46 | 11, 45 | eqtrd 2773 |
1
β’ (((π β π β§ π΄ β π β§ π΅ β π) β§ π΄ β π΅) β ((VtxDegβπΊ)βπ΄) = 2) |