Theorem frgrwopreglem1

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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	frgrwopreg.d	⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
	frgrwopreg.a	⊢ 𝐴 = { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 }
	frgrwopreg.b	⊢ 𝐵 = ( 𝑉 ∖ 𝐴 )
Assertion	frgrwopreglem1	⊢ ( 𝐴 ∈ V ∧ 𝐵 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		frgrwopreg.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		frgrwopreg.d	⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
3		frgrwopreg.a	⊢ 𝐴 = { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 }
4		frgrwopreg.b	⊢ 𝐵 = ( 𝑉 ∖ 𝐴 )
5	1	fvexi	⊢ 𝑉 ∈ V
6		rabexg	⊢ ( 𝑉 ∈ V → { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } ∈ V )
7	3 6	eqeltrid	⊢ ( 𝑉 ∈ V → 𝐴 ∈ V )
8		difexg	⊢ ( 𝑉 ∈ V → ( 𝑉 ∖ 𝐴 ) ∈ V )
9	4 8	eqeltrid	⊢ ( 𝑉 ∈ V → 𝐵 ∈ V )
10	7 9	jca	⊢ ( 𝑉 ∈ V → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
11	5 10	ax-mp	⊢ ( 𝐴 ∈ V ∧ 𝐵 ∈ V )