Metamath Proof Explorer


Theorem frpomin2

Description: Every nonempty (possibly proper) subclass of a class A with a well-founded set-like partial order R has a minimal element. The additional condition of partial order over frmin enables avoiding the axiom of infinity. (Contributed by Scott Fenton, 11-Feb-2022)

Ref Expression
Assertion frpomin2 ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝐵 ≠ ∅ ) ) → ∃ 𝑥𝐵 Pred ( 𝑅 , 𝐵 , 𝑥 ) = ∅ )

Proof

Step Hyp Ref Expression
1 frpomin ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝐵 ≠ ∅ ) ) → ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 𝑅 𝑥 )
2 vex 𝑥 ∈ V
3 2 dfpred3 Pred ( 𝑅 , 𝐵 , 𝑥 ) = { 𝑦𝐵𝑦 𝑅 𝑥 }
4 3 eqeq1i ( Pred ( 𝑅 , 𝐵 , 𝑥 ) = ∅ ↔ { 𝑦𝐵𝑦 𝑅 𝑥 } = ∅ )
5 rabeq0 ( { 𝑦𝐵𝑦 𝑅 𝑥 } = ∅ ↔ ∀ 𝑦𝐵 ¬ 𝑦 𝑅 𝑥 )
6 4 5 bitri ( Pred ( 𝑅 , 𝐵 , 𝑥 ) = ∅ ↔ ∀ 𝑦𝐵 ¬ 𝑦 𝑅 𝑥 )
7 6 rexbii ( ∃ 𝑥𝐵 Pred ( 𝑅 , 𝐵 , 𝑥 ) = ∅ ↔ ∃ 𝑥𝐵𝑦𝐵 ¬ 𝑦 𝑅 𝑥 )
8 1 7 sylibr ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴𝐵 ≠ ∅ ) ) → ∃ 𝑥𝐵 Pred ( 𝑅 , 𝐵 , 𝑥 ) = ∅ )