Theorem upgrres1lem1

Description: Lemma 1 for upgrres1 . (Contributed by AV, 7-Nov-2020)

	Ref	Expression
Hypotheses	upgrres1.v	|- V = ( Vtx ` G )
	upgrres1.e	|- E = ( Edg ` G )
	upgrres1.f	|- F = { e e. E | N e/ e }
Assertion	upgrres1lem1	|- ( ( V \ { N } ) e. _V /\ ( _I |` F ) e. _V )

Proof

Step	Hyp	Ref	Expression
1		upgrres1.v	|- V = ( Vtx ` G )
2		upgrres1.e	|- E = ( Edg ` G )
3		upgrres1.f	|- F = { e e. E | N e/ e }
4	1	fvexi	|- V e. _V
5	4	difexi	|- ( V \ { N } ) e. _V
6	2	fvexi	|- E e. _V
7	3 6	rabex2	|- F e. _V
8		resiexg	|- ( F e. _V -> ( _I |` F ) e. _V )
9	7 8	ax-mp	|- ( _I |` F ) e. _V
10	5 9	pm3.2i	|- ( ( V \ { N } ) e. _V /\ ( _I |` F ) e. _V )