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

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 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion nnwos ( ∃ 𝑥 ∈ ℕ 𝜑 → ∃ 𝑥 ∈ ℕ ( 𝜑 ∧ ∀ 𝑦 ∈ ℕ ( 𝜓 → 𝑥 ≤ 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 nnwos.1 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ ℕ ∣ 𝜑 }
3 nfcv ⊢ Ⅎ 𝑦 { 𝑥 ∈ ℕ ∣ 𝜑 }
4 2 3 nnwof ⊢ ( ( { 𝑥 ∈ ℕ ∣ 𝜑 } ⊆ ℕ ∧ { 𝑥 ∈ ℕ ∣ 𝜑 } ≠ ∅ ) → ∃ 𝑥 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ∀ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } 𝑥 ≤ 𝑦 )
5 ssrab2 ⊢ { 𝑥 ∈ ℕ ∣ 𝜑 } ⊆ ℕ
6 5 biantrur ⊢ ( { 𝑥 ∈ ℕ ∣ 𝜑 } ≠ ∅ ↔ ( { 𝑥 ∈ ℕ ∣ 𝜑 } ⊆ ℕ ∧ { 𝑥 ∈ ℕ ∣ 𝜑 } ≠ ∅ ) )
7 rabn0 ⊢ ( { 𝑥 ∈ ℕ ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑥 ∈ ℕ 𝜑 )
8 6 7 bitr3i ⊢ ( ( { 𝑥 ∈ ℕ ∣ 𝜑 } ⊆ ℕ ∧ { 𝑥 ∈ ℕ ∣ 𝜑 } ≠ ∅ ) ↔ ∃ 𝑥 ∈ ℕ 𝜑 )
9 df-rex ⊢ ( ∃ 𝑥 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ∀ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } 𝑥 ≤ 𝑦 ↔ ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ∧ ∀ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } 𝑥 ≤ 𝑦 ) )
10 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ↔ ( 𝑥 ∈ ℕ ∧ 𝜑 ) )
11 df-ral ⊢ ( ∀ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } 𝑥 ≤ 𝑦 ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } → 𝑥 ≤ 𝑦 ) )
12 1 elrab ⊢ ( 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ↔ ( 𝑦 ∈ ℕ ∧ 𝜓 ) )
13 12 imbi1i ⊢ ( ( 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } → 𝑥 ≤ 𝑦 ) ↔ ( ( 𝑦 ∈ ℕ ∧ 𝜓 ) → 𝑥 ≤ 𝑦 ) )
14 impexp ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝜓 ) → 𝑥 ≤ 𝑦 ) ↔ ( 𝑦 ∈ ℕ → ( 𝜓 → 𝑥 ≤ 𝑦 ) ) )
15 13 14 bitri ⊢ ( ( 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } → 𝑥 ≤ 𝑦 ) ↔ ( 𝑦 ∈ ℕ → ( 𝜓 → 𝑥 ≤ 𝑦 ) ) )
16 15 albii ⊢ ( ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } → 𝑥 ≤ 𝑦 ) ↔ ∀ 𝑦 ( 𝑦 ∈ ℕ → ( 𝜓 → 𝑥 ≤ 𝑦 ) ) )
17 11 16 bitri ⊢ ( ∀ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } 𝑥 ≤ 𝑦 ↔ ∀ 𝑦 ( 𝑦 ∈ ℕ → ( 𝜓 → 𝑥 ≤ 𝑦 ) ) )
18 10 17 anbi12i ⊢ ( ( 𝑥 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ∧ ∀ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } 𝑥 ≤ 𝑦 ) ↔ ( ( 𝑥 ∈ ℕ ∧ 𝜑 ) ∧ ∀ 𝑦 ( 𝑦 ∈ ℕ → ( 𝜓 → 𝑥 ≤ 𝑦 ) ) ) )
19 18 exbii ⊢ ( ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ∧ ∀ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } 𝑥 ≤ 𝑦 ) ↔ ∃ 𝑥 ( ( 𝑥 ∈ ℕ ∧ 𝜑 ) ∧ ∀ 𝑦 ( 𝑦 ∈ ℕ → ( 𝜓 → 𝑥 ≤ 𝑦 ) ) ) )
20 df-ral ⊢ ( ∀ 𝑦 ∈ ℕ ( 𝜓 → 𝑥 ≤ 𝑦 ) ↔ ∀ 𝑦 ( 𝑦 ∈ ℕ → ( 𝜓 → 𝑥 ≤ 𝑦 ) ) )
21 20 anbi2i ⊢ ( ( ( 𝑥 ∈ ℕ ∧ 𝜑 ) ∧ ∀ 𝑦 ∈ ℕ ( 𝜓 → 𝑥 ≤ 𝑦 ) ) ↔ ( ( 𝑥 ∈ ℕ ∧ 𝜑 ) ∧ ∀ 𝑦 ( 𝑦 ∈ ℕ → ( 𝜓 → 𝑥 ≤ 𝑦 ) ) ) )
22 anass ⊢ ( ( ( 𝑥 ∈ ℕ ∧ 𝜑 ) ∧ ∀ 𝑦 ∈ ℕ ( 𝜓 → 𝑥 ≤ 𝑦 ) ) ↔ ( 𝑥 ∈ ℕ ∧ ( 𝜑 ∧ ∀ 𝑦 ∈ ℕ ( 𝜓 → 𝑥 ≤ 𝑦 ) ) ) )
23 21 22 bitr3i ⊢ ( ( ( 𝑥 ∈ ℕ ∧ 𝜑 ) ∧ ∀ 𝑦 ( 𝑦 ∈ ℕ → ( 𝜓 → 𝑥 ≤ 𝑦 ) ) ) ↔ ( 𝑥 ∈ ℕ ∧ ( 𝜑 ∧ ∀ 𝑦 ∈ ℕ ( 𝜓 → 𝑥 ≤ 𝑦 ) ) ) )
24 23 exbii ⊢ ( ∃ 𝑥 ( ( 𝑥 ∈ ℕ ∧ 𝜑 ) ∧ ∀ 𝑦 ( 𝑦 ∈ ℕ → ( 𝜓 → 𝑥 ≤ 𝑦 ) ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ ℕ ∧ ( 𝜑 ∧ ∀ 𝑦 ∈ ℕ ( 𝜓 → 𝑥 ≤ 𝑦 ) ) ) )
25 df-rex ⊢ ( ∃ 𝑥 ∈ ℕ ( 𝜑 ∧ ∀ 𝑦 ∈ ℕ ( 𝜓 → 𝑥 ≤ 𝑦 ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ ℕ ∧ ( 𝜑 ∧ ∀ 𝑦 ∈ ℕ ( 𝜓 → 𝑥 ≤ 𝑦 ) ) ) )
26 24 25 bitr4i ⊢ ( ∃ 𝑥 ( ( 𝑥 ∈ ℕ ∧ 𝜑 ) ∧ ∀ 𝑦 ( 𝑦 ∈ ℕ → ( 𝜓 → 𝑥 ≤ 𝑦 ) ) ) ↔ ∃ 𝑥 ∈ ℕ ( 𝜑 ∧ ∀ 𝑦 ∈ ℕ ( 𝜓 → 𝑥 ≤ 𝑦 ) ) )
27 9 19 26 3bitri ⊢ ( ∃ 𝑥 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ∀ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } 𝑥 ≤ 𝑦 ↔ ∃ 𝑥 ∈ ℕ ( 𝜑 ∧ ∀ 𝑦 ∈ ℕ ( 𝜓 → 𝑥 ≤ 𝑦 ) ) )
28 4 8 27 3imtr3i ⊢ ( ∃ 𝑥 ∈ ℕ 𝜑 → ∃ 𝑥 ∈ ℕ ( 𝜑 ∧ ∀ 𝑦 ∈ ℕ ( 𝜓 → 𝑥 ≤ 𝑦 ) ) )