Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  frgrwopreglem1 Structured version   Visualization version   GIF version

Theorem frgrwopreglem1 41478
Description: Lemma 1 for frgrwopreg 41483: 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 𝑉 = (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‘𝐺)
2 fvex 6093 . . 3 (Vtx‘𝐺) ∈ V
31, 2eqeltri 2678 . 2 𝑉 ∈ V
4 frgrwopreg.a . . . 4 𝐴 = {𝑥𝑉 ∣ (𝐷𝑥) = 𝐾}
5 rabexg 4729 . . . 4 (𝑉 ∈ V → {𝑥𝑉 ∣ (𝐷𝑥) = 𝐾} ∈ V)
64, 5syl5eqel 2686 . . 3 (𝑉 ∈ V → 𝐴 ∈ V)
7 frgrwopreg.b . . . 4 𝐵 = (𝑉𝐴)
8 difexg 4725 . . . 4 (𝑉 ∈ V → (𝑉𝐴) ∈ V)
97, 8syl5eqel 2686 . . 3 (𝑉 ∈ V → 𝐵 ∈ V)
106, 9jca 552 . 2 (𝑉 ∈ V → (𝐴 ∈ V ∧ 𝐵 ∈ V))
113, 10ax-mp 5 1 (𝐴 ∈ V ∧ 𝐵 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wa 382   = wceq 1474  wcel 1975  {crab 2894  Vcvv 3167  cdif 3531  cfv 5785  Vtxcvtx 40226  VtxDegcvtxdg 40678
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2227  ax-ext 2584  ax-sep 4698  ax-nul 4707
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2456  df-clab 2591  df-cleq 2597  df-clel 2600  df-nfc 2734  df-ral 2895  df-rex 2896  df-rab 2899  df-v 3169  df-sbc 3397  df-dif 3537  df-un 3539  df-in 3541  df-ss 3548  df-nul 3869  df-sn 4120  df-pr 4122  df-uni 4362  df-iota 5749  df-fv 5793
This theorem is referenced by:  frgrwopreglem5  41482  frgrwopreg  41483  frgrwopreg2  41485
  Copyright terms: Public domain W3C validator