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 ( 𝑁 ∈ ℤ → ( ( 𝑁 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → { 𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘 } ⊆ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ ( 𝑁 = if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) → ( 𝑁 ∈ 𝐴 ↔ if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) ∈ 𝐴 ) )
2 1 anbi1d ⊢ ( 𝑁 = if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) → ( ( 𝑁 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) ↔ ( if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) ) )
3 breq1 ⊢ ( 𝑁 = if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) → ( 𝑁 ≤ 𝑘 ↔ if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) ≤ 𝑘 ) )
4 3 rabbidv ⊢ ( 𝑁 = if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) → { 𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘 } = { 𝑘 ∈ ℤ ∣ if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) ≤ 𝑘 } )
5 4 sseq1d ⊢ ( 𝑁 = if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) → ( { 𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘 } ⊆ 𝐴 ↔ { 𝑘 ∈ ℤ ∣ if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) ≤ 𝑘 } ⊆ 𝐴 ) )
6 2 5 imbi12d ⊢ ( 𝑁 = if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) → ( ( ( 𝑁 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → { 𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘 } ⊆ 𝐴 ) ↔ ( ( if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → { 𝑘 ∈ ℤ ∣ if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) ≤ 𝑘 } ⊆ 𝐴 ) ) )
7 1z ⊢ 1 ∈ ℤ
8 7 elimel ⊢ if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) ∈ ℤ
9 8 peano5uzi ⊢ ( ( if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → { 𝑘 ∈ ℤ ∣ if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) ≤ 𝑘 } ⊆ 𝐴 )
10 6 9 dedth ⊢ ( 𝑁 ∈ ℤ → ( ( 𝑁 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → { 𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘 } ⊆ 𝐴 ) )