Metamath Proof Explorer

Theorem bnj1228

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
Hypothesis bnj1228.1 ⊢ w ∈ B → ∀ x w ∈ B
Assertion bnj1228 ⊢ R FrSe A ∧ B ⊆ A ∧ B ≠ ∅ → ∃ x ∈ B ∀ y ∈ B ¬ y R x

Proof

Step Hyp Ref Expression
1 bnj1228.1 ⊢ w ∈ B → ∀ x w ∈ B
2 bnj69 ⊢ R FrSe A ∧ B ⊆ A ∧ B ≠ ∅ → ∃ z ∈ B ∀ y ∈ B ¬ y R z
3 nfv ⊢ Ⅎ z x ∈ B ∧ ∀ y ∈ B ¬ y R x
4 1 nfcii ⊢ Ⅎ _ x B
5 4 nfcri ⊢ Ⅎ x z ∈ B
6 nfv ⊢ Ⅎ x ¬ y R z
7 4 6 nfralw ⊢ Ⅎ x ∀ y ∈ B ¬ y R z
8 5 7 nfan ⊢ Ⅎ x z ∈ B ∧ ∀ y ∈ B ¬ y R z
9 eleq1w ⊢ x = z → x ∈ B ↔ z ∈ B
10 breq2 ⊢ x = z → y R x ↔ y R z
11 10 notbid ⊢ x = z → ¬ y R x ↔ ¬ y R z
12 11 ralbidv ⊢ x = z → ∀ y ∈ B ¬ y R x ↔ ∀ y ∈ B ¬ y R z
13 9 12 anbi12d ⊢ x = z → x ∈ B ∧ ∀ y ∈ B ¬ y R x ↔ z ∈ B ∧ ∀ y ∈ B ¬ y R z
14 3 8 13 cbvexv1 ⊢ ∃ x x ∈ B ∧ ∀ y ∈ B ¬ y R x ↔ ∃ z z ∈ B ∧ ∀ y ∈ B ¬ y R z
15 df-rex ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y R x ↔ ∃ x x ∈ B ∧ ∀ y ∈ B ¬ y R x
16 df-rex ⊢ ∃ z ∈ B ∀ y ∈ B ¬ y R z ↔ ∃ z z ∈ B ∧ ∀ y ∈ B ¬ y R z
17 14 15 16 3bitr4i ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y R x ↔ ∃ z ∈ B ∀ y ∈ B ¬ y R z
18 2 17 sylibr ⊢ R FrSe A ∧ B ⊆ A ∧ B ≠ ∅ → ∃ x ∈ B ∀ y ∈ B ¬ y R x