MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  frgrwopreglem1 Structured version   Visualization version   GIF version

Theorem frgrwopreglem1 29298
Description: Lemma 1 for frgrwopreg 29309: the classes 𝐴 and 𝐡 are sets. The definition of 𝐴 and 𝐡 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 𝑉 = (Vtxβ€˜πΊ)
frgrwopreg.d 𝐷 = (VtxDegβ€˜πΊ)
frgrwopreg.a 𝐴 = {π‘₯ ∈ 𝑉 ∣ (π·β€˜π‘₯) = 𝐾}
frgrwopreg.b 𝐡 = (𝑉 βˆ– 𝐴)
Assertion
Ref Expression
frgrwopreglem1 (𝐴 ∈ V ∧ 𝐡 ∈ V)
Distinct variable group:   π‘₯,𝑉
Allowed substitution hints:   𝐴(π‘₯)   𝐡(π‘₯)   𝐷(π‘₯)   𝐺(π‘₯)   𝐾(π‘₯)

Proof of Theorem frgrwopreglem1
StepHypRef Expression
1 frgrwopreg.v . . 3 𝑉 = (Vtxβ€˜πΊ)
21fvexi 6861 . 2 𝑉 ∈ V
3 frgrwopreg.a . . . 4 𝐴 = {π‘₯ ∈ 𝑉 ∣ (π·β€˜π‘₯) = 𝐾}
4 rabexg 5293 . . . 4 (𝑉 ∈ V β†’ {π‘₯ ∈ 𝑉 ∣ (π·β€˜π‘₯) = 𝐾} ∈ V)
53, 4eqeltrid 2842 . . 3 (𝑉 ∈ V β†’ 𝐴 ∈ V)
6 frgrwopreg.b . . . 4 𝐡 = (𝑉 βˆ– 𝐴)
7 difexg 5289 . . . 4 (𝑉 ∈ V β†’ (𝑉 βˆ– 𝐴) ∈ V)
86, 7eqeltrid 2842 . . 3 (𝑉 ∈ V β†’ 𝐡 ∈ V)
95, 8jca 513 . 2 (𝑉 ∈ V β†’ (𝐴 ∈ V ∧ 𝐡 ∈ V))
102, 9ax-mp 5 1 (𝐴 ∈ V ∧ 𝐡 ∈ V)
Colors of variables: wff setvar class
Syntax hints:   ∧ wa 397   = wceq 1542   ∈ wcel 2107  {crab 3410  Vcvv 3448   βˆ– cdif 3912  β€˜cfv 6501  Vtxcvtx 27989  VtxDegcvtxdg 28455
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-sep 5261  ax-nul 5268
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2945  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-sn 4592  df-pr 4594  df-uni 4871  df-iota 6453  df-fv 6509
This theorem is referenced by:  frgrwopreg2  29305  frgrwopreglem5  29307  frgrwopreglem5ALT  29308  frgrwopreg  29309
  Copyright terms: Public domain W3C validator