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

Metamath Proof Explorer

Theorem rexuz2

Description: Restricted existential quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005)

Ref Expression
Assertion rexuz2 ( ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) 𝜑 ↔ ( 𝑀 ∈ ℤ ∧ ∃ 𝑛 ∈ ℤ ( 𝑀 ≤ 𝑛 ∧ 𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 eluz2 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑀 ≤ 𝑛 ) )
2 df-3an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑀 ≤ 𝑛 ) ↔ ( ( 𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑀 ≤ 𝑛 ) )
3 1 2 bitri ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( ( 𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑀 ≤ 𝑛 ) )
4 3 anbi1i ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝜑 ) ↔ ( ( ( 𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑀 ≤ 𝑛 ) ∧ 𝜑 ) )
5 anass ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑀 ≤ 𝑛 ) ∧ 𝜑 ) ↔ ( ( 𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝑛 ∧ 𝜑 ) ) )
6 an21 ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝑛 ∧ 𝜑 ) ) ↔ ( 𝑛 ∈ ℤ ∧ ( 𝑀 ∈ ℤ ∧ ( 𝑀 ≤ 𝑛 ∧ 𝜑 ) ) ) )
7 5 6 bitri ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑀 ≤ 𝑛 ) ∧ 𝜑 ) ↔ ( 𝑛 ∈ ℤ ∧ ( 𝑀 ∈ ℤ ∧ ( 𝑀 ≤ 𝑛 ∧ 𝜑 ) ) ) )
8 4 7 bitri ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝜑 ) ↔ ( 𝑛 ∈ ℤ ∧ ( 𝑀 ∈ ℤ ∧ ( 𝑀 ≤ 𝑛 ∧ 𝜑 ) ) ) )
9 8 rexbii2 ⊢ ( ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) 𝜑 ↔ ∃ 𝑛 ∈ ℤ ( 𝑀 ∈ ℤ ∧ ( 𝑀 ≤ 𝑛 ∧ 𝜑 ) ) )
10 r19.42v ⊢ ( ∃ 𝑛 ∈ ℤ ( 𝑀 ∈ ℤ ∧ ( 𝑀 ≤ 𝑛 ∧ 𝜑 ) ) ↔ ( 𝑀 ∈ ℤ ∧ ∃ 𝑛 ∈ ℤ ( 𝑀 ≤ 𝑛 ∧ 𝜑 ) ) )
11 9 10 bitri ⊢ ( ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) 𝜑 ↔ ( 𝑀 ∈ ℤ ∧ ∃ 𝑛 ∈ ℤ ( 𝑀 ≤ 𝑛 ∧ 𝜑 ) ) )