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 ⊢ N ∈ ℤ
Assertion dfuzi ⊢ z ∈ ℤ | N ≤ z = ⋂ x | N ∈ x ∧ ∀ y ∈ x y + 1 ∈ x

Proof

Step Hyp Ref Expression
1 dfuzi.1 ⊢ N ∈ ℤ
2 ssintab ⊢ z ∈ ℤ | N ≤ z ⊆ ⋂ x | N ∈ x ∧ ∀ y ∈ x y + 1 ∈ x ↔ ∀ x N ∈ x ∧ ∀ y ∈ x y + 1 ∈ x → z ∈ ℤ | N ≤ z ⊆ x
3 1 peano5uzi ⊢ N ∈ x ∧ ∀ y ∈ x y + 1 ∈ x → z ∈ ℤ | N ≤ z ⊆ x
4 2 3 mpgbir ⊢ z ∈ ℤ | N ≤ z ⊆ ⋂ x | N ∈ x ∧ ∀ y ∈ x y + 1 ∈ x
5 1 zrei ⊢ N ∈ ℝ
6 5 leidi ⊢ N ≤ N
7 breq2 ⊢ z = N → N ≤ z ↔ N ≤ N
8 7 elrab ⊢ N ∈ z ∈ ℤ | N ≤ z ↔ N ∈ ℤ ∧ N ≤ N
9 1 6 8 mpbir2an ⊢ N ∈ z ∈ ℤ | N ≤ z
10 peano2uz2 ⊢ N ∈ ℤ ∧ y ∈ z ∈ ℤ | N ≤ z → y + 1 ∈ z ∈ ℤ | N ≤ z
11 1 10 mpan ⊢ y ∈ z ∈ ℤ | N ≤ z → y + 1 ∈ z ∈ ℤ | N ≤ z
12 11 rgen ⊢ ∀ y ∈ z ∈ ℤ | N ≤ z y + 1 ∈ z ∈ ℤ | N ≤ z
13 zex ⊢ ℤ ∈ V
14 13 rabex ⊢ z ∈ ℤ | N ≤ z ∈ V
15 eleq2 ⊢ x = z ∈ ℤ | N ≤ z → N ∈ x ↔ N ∈ z ∈ ℤ | N ≤ z
16 eleq2 ⊢ x = z ∈ ℤ | N ≤ z → y + 1 ∈ x ↔ y + 1 ∈ z ∈ ℤ | N ≤ z
17 16 raleqbi1dv ⊢ x = z ∈ ℤ | N ≤ z → ∀ y ∈ x y + 1 ∈ x ↔ ∀ y ∈ z ∈ ℤ | N ≤ z y + 1 ∈ z ∈ ℤ | N ≤ z
18 15 17 anbi12d ⊢ x = z ∈ ℤ | N ≤ z → N ∈ x ∧ ∀ y ∈ x y + 1 ∈ x ↔ N ∈ z ∈ ℤ | N ≤ z ∧ ∀ y ∈ z ∈ ℤ | N ≤ z y + 1 ∈ z ∈ ℤ | N ≤ z
19 14 18 elab ⊢ z ∈ ℤ | N ≤ z ∈ x | N ∈ x ∧ ∀ y ∈ x y + 1 ∈ x ↔ N ∈ z ∈ ℤ | N ≤ z ∧ ∀ y ∈ z ∈ ℤ | N ≤ z y + 1 ∈ z ∈ ℤ | N ≤ z
20 9 12 19 mpbir2an ⊢ z ∈ ℤ | N ≤ z ∈ x | N ∈ x ∧ ∀ y ∈ x y + 1 ∈ x
21 intss1 ⊢ z ∈ ℤ | N ≤ z ∈ x | N ∈ x ∧ ∀ y ∈ x y + 1 ∈ x → ⋂ x | N ∈ x ∧ ∀ y ∈ x y + 1 ∈ x ⊆ z ∈ ℤ | N ≤ z
22 20 21 ax-mp ⊢ ⋂ x | N ∈ x ∧ ∀ y ∈ x y + 1 ∈ x ⊆ z ∈ ℤ | N ≤ z
23 4 22 eqssi ⊢ z ∈ ℤ | N ≤ z = ⋂ x | N ∈ x ∧ ∀ y ∈ x y + 1 ∈ x