This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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