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

Theorem fri 5594
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 5593 1 (((𝐵𝐶𝑅 Fr 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397  wcel 2107  wne 2944  wral 3065  wrex 3074  wss 3911  c0 4283   class class class wbr 5106   Fr wfr 5586
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
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2945  df-ral 3066  df-rex 3075  df-v 3448  df-dif 3914  df-in 3918  df-ss 3928  df-pw 4563  df-sn 4588  df-fr 5589
This theorem is referenced by:  frc  5600  fr2nr  5612  frminex  5614  wereu  5630  wereu2  5631  frpomin  6295  fr3nr  7707  frfi  9233  fimax2g  9234  fimin2g  9434  wofib  9482  wemapso  9488  wemapso2lem  9489  noinfep  9597  cflim2  10200  isfin1-3  10323  fin12  10350  fpwwe2lem11  10578  fpwwe2lem12  10579  fpwwe2  10580  bnj110  33473  frinfm  36197  fdc  36207  fnwe2lem2  41381
  Copyright terms: Public domain W3C validator