Theorem fri 5624

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 781	. 2 ⊢ (((𝐵 ∈ 𝐶 ∧ 𝑅 Fr 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → 𝑅 Fr 𝐴)
2		simprl 783	. 2 ⊢ (((𝐵 ∈ 𝐶 ∧ 𝑅 Fr 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → 𝐵 ⊆ 𝐴)
3		simpll 779	. 2 ⊢ (((𝐵 ∈ 𝐶 ∧ 𝑅 Fr 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → 𝐵 ∈ 𝐶)
4		simprr 785	. 2 ⊢ (((𝐵 ∈ 𝐶 ∧ 𝑅 Fr 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → 𝐵 ≠ ∅)
5	1, 2, 3, 4	frd 5623	1 ⊢ (((𝐵 ∈ 𝐶 ∧ 𝑅 Fr 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∈ wcel 2146   ≠ wne 2961  ∀wral 3082  ∃wrex 3092   ⊆ wss 3908  ∅c0 4289   class class class wbr 5114   Fr wfr 5616

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-ral 3083  df-rex 3093  df-v 3460  df-dif 3911  df-ss 3925  df-pw 4569  df-sn 4595  df-fr 5619

This theorem is used by:  frc  5629  fr2nr  5643  frminex  5645  wereu  5662  wereu2  5663  frpomin  6348  fr3nr  7780  frfi  9255  fimax2g  9256  fimin2g  9469  wofib  9517  wemapso  9523  wemapso2lem  9524  noinfep  9639  cflim2  10265  isfin1-3  10388  fin12  10415  fpwwe2lem11  10644  fpwwe2lem12  10645  fpwwe2  10646  bnj110  35278  frinfm  38427  fdc  38437  fnwe2lem2  43819  sswfaxreg  45737