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 ) ∈ 𝐴 ) → { 𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘 } ⊆ 𝐴 ) )