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

Metamath Proof Explorer

Theorem bnj69

Description: Existence of a minimal element in certain classes: if R is well-founded and set-like on A , then every nonempty subclass of A has a minimal element. The proof has been taken from Chapter 4 of Don Monk's notes on Set Theory. See http://euclid.colorado.edu/~monkd/setth.pdf . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Assertion bnj69 ⊢ R FrSe A ∧ B ⊆ A ∧ B ≠ ∅ → ∃ x ∈ B ∀ y ∈ B ¬ y R x

Proof

Step Hyp Ref Expression
1 biid ⊢ R FrSe A ∧ B ⊆ A ∧ B ≠ ∅ ↔ R FrSe A ∧ B ⊆ A ∧ B ≠ ∅
2 biid ⊢ x ∈ B ∧ y ∈ B ∧ y R x ↔ x ∈ B ∧ y ∈ B ∧ y R x
3 biid ⊢ ∀ y ∈ B ¬ y R x ↔ ∀ y ∈ B ¬ y R x
4 1 2 3 bnj1189 ⊢ R FrSe A ∧ B ⊆ A ∧ B ≠ ∅ → ∃ x ∈ B ∀ y ∈ B ¬ y R x