Description: Lemma 1 for uhgrspan1 . (Contributed by AV, 19-Nov-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | uhgrspan1.v | |- V = ( Vtx ` G ) |
|
uhgrspan1.i | |- I = ( iEdg ` G ) |
||
uhgrspan1.f | |- F = { i e. dom I | N e/ ( I ` i ) } |
||
Assertion | uhgrspan1lem1 | |- ( ( V \ { N } ) e. _V /\ ( I |` F ) e. _V ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uhgrspan1.v | |- V = ( Vtx ` G ) |
|
2 | uhgrspan1.i | |- I = ( iEdg ` G ) |
|
3 | uhgrspan1.f | |- F = { i e. dom I | N e/ ( I ` i ) } |
|
4 | 1 | fvexi | |- V e. _V |
5 | 4 | difexi | |- ( V \ { N } ) e. _V |
6 | 2 | fvexi | |- I e. _V |
7 | 6 | resex | |- ( I |` F ) e. _V |
8 | 5 7 | pm3.2i | |- ( ( V \ { N } ) e. _V /\ ( I |` F ) e. _V ) |