Theorem fri 5574

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

Step	Hyp	Ref	Expression
1		simplr 768	. 2 ⊢ (((𝐵 ∈ 𝐶 ∧ 𝑅 Fr 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → 𝑅 Fr 𝐴)
2		simprl 770	. 2 ⊢ (((𝐵 ∈ 𝐶 ∧ 𝑅 Fr 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → 𝐵 ⊆ 𝐴)
3		simpll 766	. 2 ⊢ (((𝐵 ∈ 𝐶 ∧ 𝑅 Fr 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → 𝐵 ∈ 𝐶)
4		simprr 772	. 2 ⊢ (((𝐵 ∈ 𝐶 ∧ 𝑅 Fr 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → 𝐵 ≠ ∅)
5	1, 2, 3, 4	frd 5573	1 ⊢ (((𝐵 ∈ 𝐶 ∧ 𝑅 Fr 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2111   ≠ wne 2928  ∀wral 3047  ∃wrex 3056   ⊆ wss 3902  ∅c0 4283   class class class wbr 5091   Fr wfr 5566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-v 3438  df-dif 3905  df-ss 3919  df-pw 4552  df-sn 4577  df-fr 5569

This theorem is referenced by:  frc  5579  fr2nr  5593  frminex  5595  wereu  5612  wereu2  5613  frpomin  6287  fr3nr  7705  frfi  9169  fimax2g  9170  fimin2g  9383  wofib  9431  wemapso  9437  wemapso2lem  9438  noinfep  9550  cflim2  10151  isfin1-3  10274  fin12  10301  fpwwe2lem11  10529  fpwwe2lem12  10530  fpwwe2  10531  bnj110  34865  frinfm  37774  fdc  37784  fnwe2lem2  43083  sswfaxreg  45019