Metamath Proof Explorer


Theorem dfuzi

Description: An expression for the upper integers that start at N that is analogous to dfnn2 for positive integers. (Contributed by NM, 6-Jul-2005) (Proof shortened by Mario Carneiro, 3-May-2014)

Ref Expression
Hypothesis dfuzi.1 𝑁 ∈ ℤ
Assertion dfuzi { 𝑧 ∈ ℤ ∣ 𝑁𝑧 } = { 𝑥 ∣ ( 𝑁𝑥 ∧ ∀ 𝑦𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) }

Proof

Step Hyp Ref Expression
1 dfuzi.1 𝑁 ∈ ℤ
2 ssintab ( { 𝑧 ∈ ℤ ∣ 𝑁𝑧 } ⊆ { 𝑥 ∣ ( 𝑁𝑥 ∧ ∀ 𝑦𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) } ↔ ∀ 𝑥 ( ( 𝑁𝑥 ∧ ∀ 𝑦𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) → { 𝑧 ∈ ℤ ∣ 𝑁𝑧 } ⊆ 𝑥 ) )
3 1 peano5uzi ( ( 𝑁𝑥 ∧ ∀ 𝑦𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) → { 𝑧 ∈ ℤ ∣ 𝑁𝑧 } ⊆ 𝑥 )
4 2 3 mpgbir { 𝑧 ∈ ℤ ∣ 𝑁𝑧 } ⊆ { 𝑥 ∣ ( 𝑁𝑥 ∧ ∀ 𝑦𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) }
5 1 zrei 𝑁 ∈ ℝ
6 5 leidi 𝑁𝑁
7 breq2 ( 𝑧 = 𝑁 → ( 𝑁𝑧𝑁𝑁 ) )
8 7 elrab ( 𝑁 ∈ { 𝑧 ∈ ℤ ∣ 𝑁𝑧 } ↔ ( 𝑁 ∈ ℤ ∧ 𝑁𝑁 ) )
9 1 6 8 mpbir2an 𝑁 ∈ { 𝑧 ∈ ℤ ∣ 𝑁𝑧 }
10 peano2uz2 ( ( 𝑁 ∈ ℤ ∧ 𝑦 ∈ { 𝑧 ∈ ℤ ∣ 𝑁𝑧 } ) → ( 𝑦 + 1 ) ∈ { 𝑧 ∈ ℤ ∣ 𝑁𝑧 } )
11 1 10 mpan ( 𝑦 ∈ { 𝑧 ∈ ℤ ∣ 𝑁𝑧 } → ( 𝑦 + 1 ) ∈ { 𝑧 ∈ ℤ ∣ 𝑁𝑧 } )
12 11 rgen 𝑦 ∈ { 𝑧 ∈ ℤ ∣ 𝑁𝑧 } ( 𝑦 + 1 ) ∈ { 𝑧 ∈ ℤ ∣ 𝑁𝑧 }
13 zex ℤ ∈ V
14 13 rabex { 𝑧 ∈ ℤ ∣ 𝑁𝑧 } ∈ V
15 eleq2 ( 𝑥 = { 𝑧 ∈ ℤ ∣ 𝑁𝑧 } → ( 𝑁𝑥𝑁 ∈ { 𝑧 ∈ ℤ ∣ 𝑁𝑧 } ) )
16 eleq2 ( 𝑥 = { 𝑧 ∈ ℤ ∣ 𝑁𝑧 } → ( ( 𝑦 + 1 ) ∈ 𝑥 ↔ ( 𝑦 + 1 ) ∈ { 𝑧 ∈ ℤ ∣ 𝑁𝑧 } ) )
17 16 raleqbi1dv ( 𝑥 = { 𝑧 ∈ ℤ ∣ 𝑁𝑧 } → ( ∀ 𝑦𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ↔ ∀ 𝑦 ∈ { 𝑧 ∈ ℤ ∣ 𝑁𝑧 } ( 𝑦 + 1 ) ∈ { 𝑧 ∈ ℤ ∣ 𝑁𝑧 } ) )
18 15 17 anbi12d ( 𝑥 = { 𝑧 ∈ ℤ ∣ 𝑁𝑧 } → ( ( 𝑁𝑥 ∧ ∀ 𝑦𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) ↔ ( 𝑁 ∈ { 𝑧 ∈ ℤ ∣ 𝑁𝑧 } ∧ ∀ 𝑦 ∈ { 𝑧 ∈ ℤ ∣ 𝑁𝑧 } ( 𝑦 + 1 ) ∈ { 𝑧 ∈ ℤ ∣ 𝑁𝑧 } ) ) )
19 14 18 elab ( { 𝑧 ∈ ℤ ∣ 𝑁𝑧 } ∈ { 𝑥 ∣ ( 𝑁𝑥 ∧ ∀ 𝑦𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) } ↔ ( 𝑁 ∈ { 𝑧 ∈ ℤ ∣ 𝑁𝑧 } ∧ ∀ 𝑦 ∈ { 𝑧 ∈ ℤ ∣ 𝑁𝑧 } ( 𝑦 + 1 ) ∈ { 𝑧 ∈ ℤ ∣ 𝑁𝑧 } ) )
20 9 12 19 mpbir2an { 𝑧 ∈ ℤ ∣ 𝑁𝑧 } ∈ { 𝑥 ∣ ( 𝑁𝑥 ∧ ∀ 𝑦𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) }
21 intss1 ( { 𝑧 ∈ ℤ ∣ 𝑁𝑧 } ∈ { 𝑥 ∣ ( 𝑁𝑥 ∧ ∀ 𝑦𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) } → { 𝑥 ∣ ( 𝑁𝑥 ∧ ∀ 𝑦𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) } ⊆ { 𝑧 ∈ ℤ ∣ 𝑁𝑧 } )
22 20 21 ax-mp { 𝑥 ∣ ( 𝑁𝑥 ∧ ∀ 𝑦𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) } ⊆ { 𝑧 ∈ ℤ ∣ 𝑁𝑧 }
23 4 22 eqssi { 𝑧 ∈ ℤ ∣ 𝑁𝑧 } = { 𝑥 ∣ ( 𝑁𝑥 ∧ ∀ 𝑦𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) }