Metamath Proof Explorer

Theorem nnwos

Description: Well-ordering principle: any nonempty set of positive integers has a least element (schema form). (Contributed by NM, 17-Aug-2001)

Ref Expression
Hypothesis nnwos.1 ⊢x=y→φ↔ψ
Assertion nnwos ⊢∃x∈ℕφ→∃x∈ℕφ∧∀y∈ℕψ→x≤y

Proof

Step Hyp Ref Expression
1 nnwos.1 ⊢x=y→φ↔ψ
2 nfrab1 ⊢Ⅎ_xx∈ℕ|φ
3 nfcv ⊢Ⅎ_yx∈ℕ|φ
4 2 3 nnwof ⊢x∈ℕ|φ⊆ℕ∧x∈ℕ|φ≠∅→∃x∈x∈ℕ|φ∀y∈x∈ℕ|φx≤y
5 ssrab2 ⊢x∈ℕ|φ⊆ℕ
6 5 biantrur ⊢x∈ℕ|φ≠∅↔x∈ℕ|φ⊆ℕ∧x∈ℕ|φ≠∅
7 rabn0 ⊢x∈ℕ|φ≠∅↔∃x∈ℕφ
8 6 7 bitr3i ⊢x∈ℕ|φ⊆ℕ∧x∈ℕ|φ≠∅↔∃x∈ℕφ
9 df-rex ⊢∃x∈x∈ℕ|φ∀y∈x∈ℕ|φx≤y↔∃xx∈x∈ℕ|φ∧∀y∈x∈ℕ|φx≤y
10 rabid ⊢x∈x∈ℕ|φ↔x∈ℕ∧φ
11 df-ral ⊢∀y∈x∈ℕ|φx≤y↔∀yy∈x∈ℕ|φ→x≤y
12 1 elrab ⊢y∈x∈ℕ|φ↔y∈ℕ∧ψ
13 12 imbi1i ⊢y∈x∈ℕ|φ→x≤y↔y∈ℕ∧ψ→x≤y
14 impexp ⊢y∈ℕ∧ψ→x≤y↔y∈ℕ→ψ→x≤y
15 13 14 bitri ⊢y∈x∈ℕ|φ→x≤y↔y∈ℕ→ψ→x≤y
16 15 albii ⊢∀yy∈x∈ℕ|φ→x≤y↔∀yy∈ℕ→ψ→x≤y
17 11 16 bitri ⊢∀y∈x∈ℕ|φx≤y↔∀yy∈ℕ→ψ→x≤y
18 10 17 anbi12i ⊢x∈x∈ℕ|φ∧∀y∈x∈ℕ|φx≤y↔x∈ℕ∧φ∧∀yy∈ℕ→ψ→x≤y
19 18 exbii ⊢∃xx∈x∈ℕ|φ∧∀y∈x∈ℕ|φx≤y↔∃xx∈ℕ∧φ∧∀yy∈ℕ→ψ→x≤y
20 df-ral ⊢∀y∈ℕψ→x≤y↔∀yy∈ℕ→ψ→x≤y
21 20 anbi2i ⊢x∈ℕ∧φ∧∀y∈ℕψ→x≤y↔x∈ℕ∧φ∧∀yy∈ℕ→ψ→x≤y
22 anass ⊢x∈ℕ∧φ∧∀y∈ℕψ→x≤y↔x∈ℕ∧φ∧∀y∈ℕψ→x≤y
23 21 22 bitr3i ⊢x∈ℕ∧φ∧∀yy∈ℕ→ψ→x≤y↔x∈ℕ∧φ∧∀y∈ℕψ→x≤y
24 23 exbii ⊢∃xx∈ℕ∧φ∧∀yy∈ℕ→ψ→x≤y↔∃xx∈ℕ∧φ∧∀y∈ℕψ→x≤y
25 df-rex ⊢∃x∈ℕφ∧∀y∈ℕψ→x≤y↔∃xx∈ℕ∧φ∧∀y∈ℕψ→x≤y
26 24 25 bitr4i ⊢∃xx∈ℕ∧φ∧∀yy∈ℕ→ψ→x≤y↔∃x∈ℕφ∧∀y∈ℕψ→x≤y
27 9 19 26 3bitri ⊢∃x∈x∈ℕ|φ∀y∈x∈ℕ|φx≤y↔∃x∈ℕφ∧∀y∈ℕψ→x≤y
28 4 8 27 3imtr3i ⊢∃x∈ℕφ→∃x∈ℕφ∧∀y∈ℕψ→x≤y