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

Theorem fri 5637
Description: A nonempty subset of an 𝑅-well-founded class has an 𝑅-minimal element (inference form). (Contributed by BJ, 16-Nov-2024.) (Proof shortened by BJ, 19-Nov-2024.)
Assertion
Ref Expression
fri (((𝐵𝐶𝑅 Fr 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦   𝑥,𝑅,𝑦

Proof of Theorem fri
StepHypRef Expression
1 simplr 768 . 2 (((𝐵𝐶𝑅 Fr 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → 𝑅 Fr 𝐴)
2 simprl 770 . 2 (((𝐵𝐶𝑅 Fr 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → 𝐵𝐴)
3 simpll 766 . 2 (((𝐵𝐶𝑅 Fr 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → 𝐵𝐶)
4 simprr 772 . 2 (((𝐵𝐶𝑅 Fr 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → 𝐵 ≠ ∅)
51, 2, 3, 4frd 5636 1 (((𝐵𝐶𝑅 Fr 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397  wcel 2107  wne 2941  wral 3062  wrex 3071  wss 3949  c0 4323   class class class wbr 5149   Fr wfr 5629
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 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-v 3477  df-dif 3952  df-in 3956  df-ss 3966  df-pw 4605  df-sn 4630  df-fr 5632
This theorem is referenced by:  frc  5643  fr2nr  5655  frminex  5657  wereu  5673  wereu2  5674  frpomin  6342  fr3nr  7759  frfi  9288  fimax2g  9289  fimin2g  9492  wofib  9540  wemapso  9546  wemapso2lem  9547  noinfep  9655  cflim2  10258  isfin1-3  10381  fin12  10408  fpwwe2lem11  10636  fpwwe2lem12  10637  fpwwe2  10638  bnj110  33869  frinfm  36603  fdc  36613  fnwe2lem2  41793
  Copyright terms: Public domain W3C validator