Step |
Hyp |
Ref |
Expression |
1 |
|
isupgr.v |
|- V = ( Vtx ` G ) |
2 |
|
isupgr.e |
|- E = ( iEdg ` G ) |
3 |
1 2
|
upgrfn |
|- ( ( G e. UPGraph /\ E Fn A ) -> E : A --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } ) |
4 |
3
|
ffvelrnda |
|- ( ( ( G e. UPGraph /\ E Fn A ) /\ F e. A ) -> ( E ` F ) e. { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } ) |
5 |
4
|
3impa |
|- ( ( G e. UPGraph /\ E Fn A /\ F e. A ) -> ( E ` F ) e. { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } ) |
6 |
|
fveq2 |
|- ( x = ( E ` F ) -> ( # ` x ) = ( # ` ( E ` F ) ) ) |
7 |
6
|
breq1d |
|- ( x = ( E ` F ) -> ( ( # ` x ) <_ 2 <-> ( # ` ( E ` F ) ) <_ 2 ) ) |
8 |
7
|
elrab |
|- ( ( E ` F ) e. { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } <-> ( ( E ` F ) e. ( ~P V \ { (/) } ) /\ ( # ` ( E ` F ) ) <_ 2 ) ) |
9 |
8
|
simprbi |
|- ( ( E ` F ) e. { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } -> ( # ` ( E ` F ) ) <_ 2 ) |
10 |
5 9
|
syl |
|- ( ( G e. UPGraph /\ E Fn A /\ F e. A ) -> ( # ` ( E ` F ) ) <_ 2 ) |