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	$$⊢\left(RFrSeA\wedge B\subseteq A\wedge B\ne \varnothing \right)\to \exists x\in B\forall y\in B\neg yRx$$

Proof

Step	Hyp	Ref	Expression
1		biid	$$⊢\left(RFrSeA\wedge B\subseteq A\wedge B\ne \varnothing \right)\leftrightarrow \left(RFrSeA\wedge B\subseteq A\wedge B\ne \varnothing \right)$$
2		biid	$$⊢\left(x\in B\wedge y\in B\wedge yRx\right)\leftrightarrow \left(x\in B\wedge y\in B\wedge yRx\right)$$
3		biid	$$⊢\forall y\in B\neg yRx\leftrightarrow \forall y\in B\neg yRx$$
4	1 2 3	bnj1189	$$⊢\left(RFrSeA\wedge B\subseteq A\wedge B\ne \varnothing \right)\to \exists x\in B\forall y\in B\neg yRx$$