| Step |
Hyp |
Ref |
Expression |
| 1 |
|
p1evtxdeq.v |
|- V = ( Vtx ` G ) |
| 2 |
|
p1evtxdeq.i |
|- I = ( iEdg ` G ) |
| 3 |
|
p1evtxdeq.f |
|- ( ph -> Fun I ) |
| 4 |
|
p1evtxdeq.fv |
|- ( ph -> ( Vtx ` F ) = V ) |
| 5 |
|
p1evtxdeq.fi |
|- ( ph -> ( iEdg ` F ) = ( I u. { <. K , E >. } ) ) |
| 6 |
|
p1evtxdeq.k |
|- ( ph -> K e. X ) |
| 7 |
|
p1evtxdeq.d |
|- ( ph -> K e/ dom I ) |
| 8 |
|
p1evtxdeq.u |
|- ( ph -> U e. V ) |
| 9 |
|
p1evtxdeq.e |
|- ( ph -> E e. Y ) |
| 10 |
1
|
fvexi |
|- V e. _V |
| 11 |
|
snex |
|- { <. K , E >. } e. _V |
| 12 |
10 11
|
pm3.2i |
|- ( V e. _V /\ { <. K , E >. } e. _V ) |
| 13 |
|
opiedgfv |
|- ( ( V e. _V /\ { <. K , E >. } e. _V ) -> ( iEdg ` <. V , { <. K , E >. } >. ) = { <. K , E >. } ) |
| 14 |
13
|
eqcomd |
|- ( ( V e. _V /\ { <. K , E >. } e. _V ) -> { <. K , E >. } = ( iEdg ` <. V , { <. K , E >. } >. ) ) |
| 15 |
12 14
|
ax-mp |
|- { <. K , E >. } = ( iEdg ` <. V , { <. K , E >. } >. ) |
| 16 |
|
opvtxfv |
|- ( ( V e. _V /\ { <. K , E >. } e. _V ) -> ( Vtx ` <. V , { <. K , E >. } >. ) = V ) |
| 17 |
12 16
|
mp1i |
|- ( ph -> ( Vtx ` <. V , { <. K , E >. } >. ) = V ) |
| 18 |
|
dmsnopg |
|- ( E e. Y -> dom { <. K , E >. } = { K } ) |
| 19 |
9 18
|
syl |
|- ( ph -> dom { <. K , E >. } = { K } ) |
| 20 |
19
|
ineq2d |
|- ( ph -> ( dom I i^i dom { <. K , E >. } ) = ( dom I i^i { K } ) ) |
| 21 |
|
df-nel |
|- ( K e/ dom I <-> -. K e. dom I ) |
| 22 |
7 21
|
sylib |
|- ( ph -> -. K e. dom I ) |
| 23 |
|
disjsn |
|- ( ( dom I i^i { K } ) = (/) <-> -. K e. dom I ) |
| 24 |
22 23
|
sylibr |
|- ( ph -> ( dom I i^i { K } ) = (/) ) |
| 25 |
20 24
|
eqtrd |
|- ( ph -> ( dom I i^i dom { <. K , E >. } ) = (/) ) |
| 26 |
|
funsng |
|- ( ( K e. X /\ E e. Y ) -> Fun { <. K , E >. } ) |
| 27 |
6 9 26
|
syl2anc |
|- ( ph -> Fun { <. K , E >. } ) |
| 28 |
2 15 1 17 4 25 3 27 8 5
|
vtxdun |
|- ( ph -> ( ( VtxDeg ` F ) ` U ) = ( ( ( VtxDeg ` G ) ` U ) +e ( ( VtxDeg ` <. V , { <. K , E >. } >. ) ` U ) ) ) |