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

Metamath Proof Explorer

Theorem peano5uzti

Description: Peano's inductive postulate for upper integers. (Contributed by NM, 6-Jul-2005) (Revised by Mario Carneiro, 25-Jul-2013)

Ref Expression
Assertion peano5uzti ⊢ N ∈ ℤ → N ∈ A ∧ ∀ x ∈ A x + 1 ∈ A → k ∈ ℤ | N ≤ k ⊆ A

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ N = if N ∈ ℤ N 1 → N ∈ A ↔ if N ∈ ℤ N 1 ∈ A
2 1 anbi1d ⊢ N = if N ∈ ℤ N 1 → N ∈ A ∧ ∀ x ∈ A x + 1 ∈ A ↔ if N ∈ ℤ N 1 ∈ A ∧ ∀ x ∈ A x + 1 ∈ A
3 breq1 ⊢ N = if N ∈ ℤ N 1 → N ≤ k ↔ if N ∈ ℤ N 1 ≤ k
4 3 rabbidv ⊢ N = if N ∈ ℤ N 1 → k ∈ ℤ | N ≤ k = k ∈ ℤ | if N ∈ ℤ N 1 ≤ k
5 4 sseq1d ⊢ N = if N ∈ ℤ N 1 → k ∈ ℤ | N ≤ k ⊆ A ↔ k ∈ ℤ | if N ∈ ℤ N 1 ≤ k ⊆ A
6 2 5 imbi12d ⊢ N = if N ∈ ℤ N 1 → N ∈ A ∧ ∀ x ∈ A x + 1 ∈ A → k ∈ ℤ | N ≤ k ⊆ A ↔ if N ∈ ℤ N 1 ∈ A ∧ ∀ x ∈ A x + 1 ∈ A → k ∈ ℤ | if N ∈ ℤ N 1 ≤ k ⊆ A
7 1z ⊢ 1 ∈ ℤ
8 7 elimel ⊢ if N ∈ ℤ N 1 ∈ ℤ
9 8 peano5uzi ⊢ if N ∈ ℤ N 1 ∈ A ∧ ∀ x ∈ A x + 1 ∈ A → k ∈ ℤ | if N ∈ ℤ N 1 ≤ k ⊆ A
10 6 9 dedth ⊢ N ∈ ℤ → N ∈ A ∧ ∀ x ∈ A x + 1 ∈ A → k ∈ ℤ | N ≤ k ⊆ A