Theorem upgrss

Description: An edge is a subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015) (Revised by AV, 29-Nov-2020)

	Ref	Expression
Hypotheses	isupgr.v	|- V = ( Vtx ` G )
	isupgr.e	|- E = ( iEdg ` G )
Assertion	upgrss	|- ( ( G e. UPGraph /\ F e. dom E ) -> ( E ` F ) C_ V )

Proof

Step	Hyp	Ref	Expression
1		isupgr.v	|- V = ( Vtx ` G )
2		isupgr.e	|- E = ( iEdg ` G )
3		ssrab2	|- { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } C_ ( ~P V \ { (/) } )
4		difss	|- ( ~P V \ { (/) } ) C_ ~P V
5	3 4	sstri	|- { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } C_ ~P V
6	1 2	upgrf	|- ( G e. UPGraph -> E : dom E --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } )
7	6	ffvelcdmda	|- ( ( G e. UPGraph /\ F e. dom E ) -> ( E ` F ) e. { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } )
8	5 7	sselid	|- ( ( G e. UPGraph /\ F e. dom E ) -> ( E ` F ) e. ~P V )
9	8	elpwid	|- ( ( G e. UPGraph /\ F e. dom E ) -> ( E ` F ) C_ V )