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∈Ax+1∈A→k∈ℤ|N≤k⊆A

Proof

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