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