Theorem nnwof

Description: Well-ordering principle: any nonempty set of positive integers has a least element. This version allows x and y to be present in A as long as they are effectively not free. (Contributed by NM, 17-Aug-2001) (Revised by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Hypotheses	nnwof.1	$$⊢\underset{\_}{Ⅎ}xA$$
	nnwof.2	$$⊢\underset{\_}{Ⅎ}yA$$
Assertion	nnwof	$$⊢\left(A\subseteq \mathbb{N}\wedge A\ne \varnothing \right)\to \exists x\in A\forall y\in Ax\le y$$

Proof

Step	Hyp	Ref	Expression
1		nnwof.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		nnwof.2	$$⊢\underset{\_}{Ⅎ}yA$$
3		nnwo	$$⊢\left(A\subseteq \mathbb{N}\wedge A\ne \varnothing \right)\to \exists w\in A\forall v\in Aw\le v$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}wA$$
5		nfv	$$⊢Ⅎxw\le v$$
6	1 5	nfralw	$$⊢Ⅎx\forall v\in Aw\le v$$
7		nfv	$$⊢Ⅎw\forall y\in Ax\le y$$
8		breq1	$$⊢w=x\to \left(w\le v\leftrightarrow x\le v\right)$$
9	8	ralbidv	$$⊢w=x\to \left(\forall v\in Aw\le v\leftrightarrow \forall v\in Ax\le v\right)$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}vA$$
11		nfv	$$⊢Ⅎyx\le v$$
12		nfv	$$⊢Ⅎvx\le y$$
13		breq2	$$⊢v=y\to \left(x\le v\leftrightarrow x\le y\right)$$
14	10 2 11 12 13	cbvralfw	$$⊢\forall v\in Ax\le v\leftrightarrow \forall y\in Ax\le y$$
15	9 14	bitrdi	$$⊢w=x\to \left(\forall v\in Aw\le v\leftrightarrow \forall y\in Ax\le y\right)$$
16	4 1 6 7 15	cbvrexfw	$$⊢\exists w\in A\forall v\in Aw\le v\leftrightarrow \exists x\in A\forall y\in Ax\le y$$
17	3 16	sylib	$$⊢\left(A\subseteq \mathbb{N}\wedge A\ne \varnothing \right)\to \exists x\in A\forall y\in Ax\le y$$