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 \land (B \in V \land B \subseteq A \land B \neq \emptyset)) \to \exists! x \in B \forall y \in B \neg y R x$

Proof

Step	Hyp	Ref	Expression
1		wefr	$⊢ R We A \to R Fr A$
2		fri	$⊢ ((B \in V \land R Fr A) \land (B \subseteq A \land B \neq \emptyset)) \to \exists x \in B \forall y \in B \neg y R x$
3	2	exp32	$⊢ (B \in V \land R Fr A) \to (B \subseteq A \to (B \neq \emptyset \to \exists x \in B \forall y \in B \neg y R x))$
4	3	expcom	$⊢ R Fr A \to (B \in V \to (B \subseteq A \to (B \neq \emptyset \to \exists x \in B \forall y \in B \neg y R x)))$
5	4	3imp2	$⊢ (R Fr A \land (B \in V \land B \subseteq A \land B \neq \emptyset)) \to \exists x \in B \forall y \in B \neg y R x$
6	1 5	sylan	$⊢ (R We A \land (B \in V \land B \subseteq A \land B \neq \emptyset)) \to \exists x \in B \forall y \in B \neg y R x$
7		weso	$⊢ R We A \to R Or A$
8		soss	$⊢ B \subseteq A \to (R Or A \to R Or B)$
9	7 8	mpan9	$⊢ (R We A \land B \subseteq A) \to R Or B$
10		somo	$⊢ R Or B \to \exists^{*} x \in B \forall y \in B \neg y R x$
11	9 10	syl	$⊢ (R We A \land B \subseteq A) \to \exists^{*} x \in B \forall y \in B \neg y R x$
12	11	3ad2antr2	$⊢ (R We A \land (B \in V \land B \subseteq A \land B \neq \emptyset)) \to \exists^{*} x \in B \forall y \in B \neg y R x$
13		reu5	$⊢ \exists! x \in B \forall y \in B \neg y R x \leftrightarrow (\exists x \in B \forall y \in B \neg y R x \land \exists^{*} x \in B \forall y \in B \neg y R x)$
14	6 12 13	sylanbrc	$⊢ (R We A \land (B \in V \land B \subseteq A \land B \neq \emptyset)) \to \exists! x \in B \forall y \in B \neg y R x$