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

Theorem fri 5645
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 769 . 2 (((𝐵𝐶𝑅 Fr 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → 𝑅 Fr 𝐴)
2 simprl 771 . 2 (((𝐵𝐶𝑅 Fr 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → 𝐵𝐴)
3 simpll 767 . 2 (((𝐵𝐶𝑅 Fr 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → 𝐵𝐶)
4 simprr 773 . 2 (((𝐵𝐶𝑅 Fr 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → 𝐵 ≠ ∅)
51, 2, 3, 4frd 5644 1 (((𝐵𝐶𝑅 Fr 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wcel 2105  wne 2937  wral 3058  wrex 3067  wss 3962  c0 4338   class class class wbr 5147   Fr wfr 5637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-v 3479  df-dif 3965  df-ss 3979  df-pw 4606  df-sn 4631  df-fr 5640
This theorem is referenced by:  frc  5651  fr2nr  5665  frminex  5667  wereu  5684  wereu2  5685  frpomin  6362  fr3nr  7790  frfi  9318  fimax2g  9319  fimin2g  9534  wofib  9582  wemapso  9588  wemapso2lem  9589  noinfep  9697  cflim2  10300  isfin1-3  10423  fin12  10450  fpwwe2lem11  10678  fpwwe2lem12  10679  fpwwe2  10680  bnj110  34850  frinfm  37721  fdc  37731  fnwe2lem2  43039
  Copyright terms: Public domain W3C validator