This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑅 , 𝐵 , 𝑥 ) = ∅ )