Metamath Proof Explorer

Theorem wereu

Description: A nonempty subset of an R -well-ordered class has a unique R -minimal element. (Contributed by NM, 18-Mar-1997) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion wereu ⊢ R We A ∧ B ∈ V ∧ B ⊆ A ∧ B ≠ ∅ → ∃! x ∈ B ∀ y ∈ B ¬ y R x

Proof

Step Hyp Ref Expression
1 wefr ⊢ R We A → R Fr A
2 fri ⊢ B ∈ V ∧ R Fr A ∧ B ⊆ A ∧ B ≠ ∅ → ∃ x ∈ B ∀ y ∈ B ¬ y R x
3 2 exp32 ⊢ B ∈ V ∧ R Fr A → B ⊆ A → B ≠ ∅ → ∃ x ∈ B ∀ y ∈ B ¬ y R x
4 3 expcom ⊢ R Fr A → B ∈ V → B ⊆ A → B ≠ ∅ → ∃ x ∈ B ∀ y ∈ B ¬ y R x
5 4 3imp2 ⊢ R Fr A ∧ B ∈ V ∧ B ⊆ A ∧ B ≠ ∅ → ∃ x ∈ B ∀ y ∈ B ¬ y R x
6 1 5 sylan ⊢ R We A ∧ B ∈ V ∧ B ⊆ A ∧ B ≠ ∅ → ∃ x ∈ B ∀ y ∈ B ¬ y R x
7 weso ⊢ R We A → R Or A
8 soss ⊢ B ⊆ A → R Or A → R Or B
9 7 8 mpan9 ⊢ R We A ∧ B ⊆ A → R Or B
10 somo ⊢ R Or B → ∃* x ∈ B ∀ y ∈ B ¬ y R x
11 9 10 syl ⊢ R We A ∧ B ⊆ A → ∃* x ∈ B ∀ y ∈ B ¬ y R x
12 11 3ad2antr2 ⊢ R We A ∧ B ∈ V ∧ B ⊆ A ∧ B ≠ ∅ → ∃* x ∈ B ∀ y ∈ B ¬ y R x
13 reu5 ⊢ ∃! x ∈ B ∀ y ∈ B ¬ y R x ↔ ∃ x ∈ B ∀ y ∈ B ¬ y R x ∧ ∃* x ∈ B ∀ y ∈ B ¬ y R x
14 6 12 13 sylanbrc ⊢ R We A ∧ B ∈ V ∧ B ⊆ A ∧ B ≠ ∅ → ∃! x ∈ B ∀ y ∈ B ¬ y R x