Theorem frgrwopreglem1 27176

Description: Lemma 1 for frgrwopreg 27187: 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.)

Hypotheses

Ref	Expression
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

Ref	Expression
frgrwopreglem1	|- ( A e. _V /\ B e. _V )

Distinct variable group:   x, V

Allowed substitution hints:   A( x)   B( x)   D( x)   G( x)   K( x)

Proof of Theorem frgrwopreglem1

Step	Hyp	Ref	Expression
1		frgrwopreg.v	. . 3 |- V = (Vtx ` G )
2		fvex 6201	. . 3 |- (Vtx ` G ) e. _V
3	1, 2	eqeltri 2697	. 2 |- V e. _V
4		frgrwopreg.a	. . . 4 |- A = { x e. V | ( D ` x ) = K }
5		rabexg 4812	. . . 4 |- ( V e. _V -> { x e. V | ( D ` x ) = K } e. _V )
6	4, 5	syl5eqel 2705	. . 3 |- ( V e. _V -> A e. _V )
7		frgrwopreg.b	. . . 4 |- B = ( V \ A )
8		difexg 4808	. . . 4 |- ( V e. _V -> ( V \ A ) e. _V )
9	7, 8	syl5eqel 2705	. . 3 |- ( V e. _V -> B e. _V )
10	6, 9	jca 554	. 2 |- ( V e. _V -> ( A e. _V /\ B e. _V ) )
11	3, 10	ax-mp 5	1 |- ( A e. _V /\ B e. _V )

Syntax hints:   /\ wa 384   = wceq 1483   e. wcel 1990   {crab 2916   _Vcvv 3200   \ cdif 3571   ` cfv 5888  Vtxcvtx 25874  VtxDegcvtxdg 26361

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-sn 4178  df-pr 4180  df-uni 4437  df-iota 5851  df-fv 5896

This theorem is referenced by:  frgrwopreg2  27183  frgrwopreglem5  27185  frgrwopreglem5ALT  27186  frgrwopreg  27187