Metamath Proof Explorer

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 ⊢ V = Vtx ⁡ G
frgrwopreg.d ⊢ D = VtxDeg ⁡ G
frgrwopreg.a ⊢ A = x ∈ V | D ⁡ x = K
frgrwopreg.b ⊢ B = V ∖ A
Assertion frgrwopreglem1 ⊢ A ∈ V ∧ B ∈ V

Proof

Step Hyp Ref Expression
1 frgrwopreg.v ⊢ V = Vtx ⁡ G
2 frgrwopreg.d ⊢ D = VtxDeg ⁡ G
3 frgrwopreg.a ⊢ A = x ∈ V | D ⁡ x = K
4 frgrwopreg.b ⊢ B = V ∖ A
5 1 fvexi ⊢ V ∈ V
6 rabexg ⊢ V ∈ V → x ∈ V | D ⁡ x = K ∈ V
7 3 6 eqeltrid ⊢ V ∈ V → A ∈ V
8 difexg ⊢ V ∈ V → V ∖ A ∈ V
9 4 8 eqeltrid ⊢ V ∈ V → B ∈ V
10 7 9 jca ⊢ V ∈ V → A ∈ V ∧ B ∈ V
11 5 10 ax-mp ⊢ A ∈ V ∧ B ∈ V