Theorem fri 5609

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 5608	1 ⊢ (((𝐵 ∈ 𝐶 ∧ 𝑅 Fr 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∈ wcel 2145   ≠ wne 2956  ∀wral 3077  ∃wrex 3087   ⊆ wss 3899  ∅c0 4279   class class class wbr 5103   Fr wfr 5601

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-v 3453  df-dif 3902  df-ss 3916  df-pw 4559  df-sn 4585  df-fr 5604

This theorem is used by:  frc  5614  fr2nr  5628  frminex  5630  wereu  5647  wereu2  5648  frpomin  6336  fr3nr  7775  frfi  9260  fimax2g  9261  fimin2g  9475  wofib  9523  wemapso  9529  wemapso2lem  9530  noinfep  9645  cflim2  10322  isfin1-3  10445  fin12  10472  fpwwe2lem11  10707  fpwwe2lem12  10708  fpwwe2  10709  bnj110  35471  frinfm  38637  fdc  38647  fnwe2lem2  44011  sswfaxreg  45929