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	⊢ Ⅎ 𝑥 𝐴
	nnwof.2	⊢ Ⅎ 𝑦 𝐴
Assertion	nnwof	⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		nnwof.1	⊢ Ⅎ 𝑥 𝐴
2		nnwof.2	⊢ Ⅎ 𝑦 𝐴
3		nnwo	⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝐴 ≠ ∅ ) → ∃ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 𝑤 ≤ 𝑣 )
4		nfcv	⊢ Ⅎ 𝑤 𝐴
5		nfv	⊢ Ⅎ 𝑥 𝑤 ≤ 𝑣
6	1 5	nfralw	⊢ Ⅎ 𝑥 ∀ 𝑣 ∈ 𝐴 𝑤 ≤ 𝑣
7		nfv	⊢ Ⅎ 𝑤 ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦
8		breq1	⊢ ( 𝑤 = 𝑥 → ( 𝑤 ≤ 𝑣 ↔ 𝑥 ≤ 𝑣 ) )
9	8	ralbidv	⊢ ( 𝑤 = 𝑥 → ( ∀ 𝑣 ∈ 𝐴 𝑤 ≤ 𝑣 ↔ ∀ 𝑣 ∈ 𝐴 𝑥 ≤ 𝑣 ) )
10		nfcv	⊢ Ⅎ 𝑣 𝐴
11		nfv	⊢ Ⅎ 𝑦 𝑥 ≤ 𝑣
12		nfv	⊢ Ⅎ 𝑣 𝑥 ≤ 𝑦
13		breq2	⊢ ( 𝑣 = 𝑦 → ( 𝑥 ≤ 𝑣 ↔ 𝑥 ≤ 𝑦 ) )
14	10 2 11 12 13	cbvralfw	⊢ ( ∀ 𝑣 ∈ 𝐴 𝑥 ≤ 𝑣 ↔ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )
15	9 14	bitrdi	⊢ ( 𝑤 = 𝑥 → ( ∀ 𝑣 ∈ 𝐴 𝑤 ≤ 𝑣 ↔ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) )
16	4 1 6 7 15	cbvrexfw	⊢ ( ∃ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 𝑤 ≤ 𝑣 ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )
17	3 16	sylib	⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )