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

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 ) ∈ 𝑥 ) }