Description: Lemma 1 for frgrwopreg : the classes A and B are sets. The definition of A and B corresponds to definition 3 in Huneke p. 2: "Let A be the set of all vertices of degree k, let B be the set of all vertices of degree different from k, ..." (Contributed by Alexander van der Vekens, 31-Dec-2017) (Revised by AV, 10-May-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | frgrwopreg.v | |- V = ( Vtx ` G ) |
|
| frgrwopreg.d | |- D = ( VtxDeg ` G ) |
||
| frgrwopreg.a | |- A = { x e. V | ( D ` x ) = K } |
||
| frgrwopreg.b | |- B = ( V \ A ) |
||
| Assertion | frgrwopreglem1 | |- ( A e. _V /\ B e. _V ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | frgrwopreg.v | |- V = ( Vtx ` G ) |
|
| 2 | frgrwopreg.d | |- D = ( VtxDeg ` G ) |
|
| 3 | frgrwopreg.a | |- A = { x e. V | ( D ` x ) = K } |
|
| 4 | frgrwopreg.b | |- B = ( V \ A ) |
|
| 5 | 1 | fvexi | |- V e. _V |
| 6 | rabexg | |- ( V e. _V -> { x e. V | ( D ` x ) = K } e. _V ) |
|
| 7 | 3 6 | eqeltrid | |- ( V e. _V -> A e. _V ) |
| 8 | difexg | |- ( V e. _V -> ( V \ A ) e. _V ) |
|
| 9 | 4 8 | eqeltrid | |- ( V e. _V -> B e. _V ) |
| 10 | 7 9 | jca | |- ( V e. _V -> ( A e. _V /\ B e. _V ) ) |
| 11 | 5 10 | ax-mp | |- ( A e. _V /\ B e. _V ) |