Step |
Hyp |
Ref |
Expression |
1 |
|
upgrres.v |
|- V = ( Vtx ` G ) |
2 |
|
upgrres.e |
|- E = ( iEdg ` G ) |
3 |
|
upgrres.f |
|- F = { i e. dom E | N e/ ( E ` i ) } |
4 |
|
upgrres.s |
|- S = <. ( V \ { N } ) , ( E |` F ) >. |
5 |
|
upgruhgr |
|- ( G e. UPGraph -> G e. UHGraph ) |
6 |
2
|
uhgrfun |
|- ( G e. UHGraph -> Fun E ) |
7 |
|
funres |
|- ( Fun E -> Fun ( E |` F ) ) |
8 |
5 6 7
|
3syl |
|- ( G e. UPGraph -> Fun ( E |` F ) ) |
9 |
8
|
funfnd |
|- ( G e. UPGraph -> ( E |` F ) Fn dom ( E |` F ) ) |
10 |
9
|
adantr |
|- ( ( G e. UPGraph /\ N e. V ) -> ( E |` F ) Fn dom ( E |` F ) ) |
11 |
1 2 3
|
upgrreslem |
|- ( ( G e. UPGraph /\ N e. V ) -> ran ( E |` F ) C_ { p e. ( ~P ( V \ { N } ) \ { (/) } ) | ( # ` p ) <_ 2 } ) |
12 |
|
df-f |
|- ( ( E |` F ) : dom ( E |` F ) --> { p e. ( ~P ( V \ { N } ) \ { (/) } ) | ( # ` p ) <_ 2 } <-> ( ( E |` F ) Fn dom ( E |` F ) /\ ran ( E |` F ) C_ { p e. ( ~P ( V \ { N } ) \ { (/) } ) | ( # ` p ) <_ 2 } ) ) |
13 |
10 11 12
|
sylanbrc |
|- ( ( G e. UPGraph /\ N e. V ) -> ( E |` F ) : dom ( E |` F ) --> { p e. ( ~P ( V \ { N } ) \ { (/) } ) | ( # ` p ) <_ 2 } ) |
14 |
|
opex |
|- <. ( V \ { N } ) , ( E |` F ) >. e. _V |
15 |
4 14
|
eqeltri |
|- S e. _V |
16 |
1 2 3 4
|
uhgrspan1lem2 |
|- ( Vtx ` S ) = ( V \ { N } ) |
17 |
16
|
eqcomi |
|- ( V \ { N } ) = ( Vtx ` S ) |
18 |
1 2 3 4
|
uhgrspan1lem3 |
|- ( iEdg ` S ) = ( E |` F ) |
19 |
18
|
eqcomi |
|- ( E |` F ) = ( iEdg ` S ) |
20 |
17 19
|
isupgr |
|- ( S e. _V -> ( S e. UPGraph <-> ( E |` F ) : dom ( E |` F ) --> { p e. ( ~P ( V \ { N } ) \ { (/) } ) | ( # ` p ) <_ 2 } ) ) |
21 |
15 20
|
mp1i |
|- ( ( G e. UPGraph /\ N e. V ) -> ( S e. UPGraph <-> ( E |` F ) : dom ( E |` F ) --> { p e. ( ~P ( V \ { N } ) \ { (/) } ) | ( # ` p ) <_ 2 } ) ) |
22 |
13 21
|
mpbird |
|- ( ( G e. UPGraph /\ N e. V ) -> S e. UPGraph ) |