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

Theorem fri 5635
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 767 . 2 (((𝐵𝐶𝑅 Fr 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → 𝑅 Fr 𝐴)
2 simprl 769 . 2 (((𝐵𝐶𝑅 Fr 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → 𝐵𝐴)
3 simpll 765 . 2 (((𝐵𝐶𝑅 Fr 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → 𝐵𝐶)
4 simprr 771 . 2 (((𝐵𝐶𝑅 Fr 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → 𝐵 ≠ ∅)
51, 2, 3, 4frd 5634 1 (((𝐵𝐶𝑅 Fr 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wcel 2106  wne 2940  wral 3061  wrex 3070  wss 3947  c0 4321   class class class wbr 5147   Fr wfr 5627
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rex 3071  df-v 3476  df-dif 3950  df-in 3954  df-ss 3964  df-pw 4603  df-sn 4628  df-fr 5630
This theorem is referenced by:  frc  5641  fr2nr  5653  frminex  5655  wereu  5671  wereu2  5672  frpomin  6338  fr3nr  7755  frfi  9284  fimax2g  9285  fimin2g  9488  wofib  9536  wemapso  9542  wemapso2lem  9543  noinfep  9651  cflim2  10254  isfin1-3  10377  fin12  10404  fpwwe2lem11  10632  fpwwe2lem12  10633  fpwwe2  10634  bnj110  33857  frinfm  36591  fdc  36601  fnwe2lem2  41778
  Copyright terms: Public domain W3C validator