Step |
Hyp |
Ref |
Expression |
1 |
|
vtxdeqd.g |
|- ( ph -> G e. X ) |
2 |
|
vtxdeqd.h |
|- ( ph -> H e. Y ) |
3 |
|
vtxdeqd.v |
|- ( ph -> ( Vtx ` H ) = ( Vtx ` G ) ) |
4 |
|
vtxdeqd.i |
|- ( ph -> ( iEdg ` H ) = ( iEdg ` G ) ) |
5 |
4
|
dmeqd |
|- ( ph -> dom ( iEdg ` H ) = dom ( iEdg ` G ) ) |
6 |
4
|
fveq1d |
|- ( ph -> ( ( iEdg ` H ) ` x ) = ( ( iEdg ` G ) ` x ) ) |
7 |
6
|
eleq2d |
|- ( ph -> ( u e. ( ( iEdg ` H ) ` x ) <-> u e. ( ( iEdg ` G ) ` x ) ) ) |
8 |
5 7
|
rabeqbidv |
|- ( ph -> { x e. dom ( iEdg ` H ) | u e. ( ( iEdg ` H ) ` x ) } = { x e. dom ( iEdg ` G ) | u e. ( ( iEdg ` G ) ` x ) } ) |
9 |
8
|
fveq2d |
|- ( ph -> ( # ` { x e. dom ( iEdg ` H ) | u e. ( ( iEdg ` H ) ` x ) } ) = ( # ` { x e. dom ( iEdg ` G ) | u e. ( ( iEdg ` G ) ` x ) } ) ) |
10 |
6
|
eqeq1d |
|- ( ph -> ( ( ( iEdg ` H ) ` x ) = { u } <-> ( ( iEdg ` G ) ` x ) = { u } ) ) |
11 |
5 10
|
rabeqbidv |
|- ( ph -> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) = { u } } = { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = { u } } ) |
12 |
11
|
fveq2d |
|- ( ph -> ( # ` { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) = { u } } ) = ( # ` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = { u } } ) ) |
13 |
9 12
|
oveq12d |
|- ( ph -> ( ( # ` { x e. dom ( iEdg ` H ) | u e. ( ( iEdg ` H ) ` x ) } ) +e ( # ` { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) = { u } } ) ) = ( ( # ` { x e. dom ( iEdg ` G ) | u e. ( ( iEdg ` G ) ` x ) } ) +e ( # ` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = { u } } ) ) ) |
14 |
3 13
|
mpteq12dv |
|- ( ph -> ( u e. ( Vtx ` H ) |-> ( ( # ` { x e. dom ( iEdg ` H ) | u e. ( ( iEdg ` H ) ` x ) } ) +e ( # ` { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) = { u } } ) ) ) = ( u e. ( Vtx ` G ) |-> ( ( # ` { x e. dom ( iEdg ` G ) | u e. ( ( iEdg ` G ) ` x ) } ) +e ( # ` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = { u } } ) ) ) ) |
15 |
|
eqid |
|- ( Vtx ` H ) = ( Vtx ` H ) |
16 |
|
eqid |
|- ( iEdg ` H ) = ( iEdg ` H ) |
17 |
|
eqid |
|- dom ( iEdg ` H ) = dom ( iEdg ` H ) |
18 |
15 16 17
|
vtxdgfval |
|- ( H e. Y -> ( VtxDeg ` H ) = ( u e. ( Vtx ` H ) |-> ( ( # ` { x e. dom ( iEdg ` H ) | u e. ( ( iEdg ` H ) ` x ) } ) +e ( # ` { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) = { u } } ) ) ) ) |
19 |
2 18
|
syl |
|- ( ph -> ( VtxDeg ` H ) = ( u e. ( Vtx ` H ) |-> ( ( # ` { x e. dom ( iEdg ` H ) | u e. ( ( iEdg ` H ) ` x ) } ) +e ( # ` { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) = { u } } ) ) ) ) |
20 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
21 |
|
eqid |
|- ( iEdg ` G ) = ( iEdg ` G ) |
22 |
|
eqid |
|- dom ( iEdg ` G ) = dom ( iEdg ` G ) |
23 |
20 21 22
|
vtxdgfval |
|- ( G e. X -> ( VtxDeg ` G ) = ( u e. ( Vtx ` G ) |-> ( ( # ` { x e. dom ( iEdg ` G ) | u e. ( ( iEdg ` G ) ` x ) } ) +e ( # ` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = { u } } ) ) ) ) |
24 |
1 23
|
syl |
|- ( ph -> ( VtxDeg ` G ) = ( u e. ( Vtx ` G ) |-> ( ( # ` { x e. dom ( iEdg ` G ) | u e. ( ( iEdg ` G ) ` x ) } ) +e ( # ` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = { u } } ) ) ) ) |
25 |
14 19 24
|
3eqtr4d |
|- ( ph -> ( VtxDeg ` H ) = ( VtxDeg ` G ) ) |