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 
|- ( E. n e. ( ZZ>= ` M ) ph <-> ( M e. ZZ /\ E. n e. ZZ ( M <_ n /\ ph ) ) )

Proof

Step Hyp Ref Expression
1 eluz2 
 |-  ( n e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ n e. ZZ /\ M <_ n ) )
2 df-3an 
 |-  ( ( M e. ZZ /\ n e. ZZ /\ M <_ n ) <-> ( ( M e. ZZ /\ n e. ZZ ) /\ M <_ n ) )
3 1 2 bitri 
 |-  ( n e. ( ZZ>= ` M ) <-> ( ( M e. ZZ /\ n e. ZZ ) /\ M <_ n ) )
4 3 anbi1i 
 |-  ( ( n e. ( ZZ>= ` M ) /\ ph ) <-> ( ( ( M e. ZZ /\ n e. ZZ ) /\ M <_ n ) /\ ph ) )
5 anass 
 |-  ( ( ( ( M e. ZZ /\ n e. ZZ ) /\ M <_ n ) /\ ph ) <-> ( ( M e. ZZ /\ n e. ZZ ) /\ ( M <_ n /\ ph ) ) )
6 an21 
 |-  ( ( ( M e. ZZ /\ n e. ZZ ) /\ ( M <_ n /\ ph ) ) <-> ( n e. ZZ /\ ( M e. ZZ /\ ( M <_ n /\ ph ) ) ) )
7 5 6 bitri 
 |-  ( ( ( ( M e. ZZ /\ n e. ZZ ) /\ M <_ n ) /\ ph ) <-> ( n e. ZZ /\ ( M e. ZZ /\ ( M <_ n /\ ph ) ) ) )
8 4 7 bitri 
 |-  ( ( n e. ( ZZ>= ` M ) /\ ph ) <-> ( n e. ZZ /\ ( M e. ZZ /\ ( M <_ n /\ ph ) ) ) )
9 8 rexbii2 
 |-  ( E. n e. ( ZZ>= ` M ) ph <-> E. n e. ZZ ( M e. ZZ /\ ( M <_ n /\ ph ) ) )
10 r19.42v 
 |-  ( E. n e. ZZ ( M e. ZZ /\ ( M <_ n /\ ph ) ) <-> ( M e. ZZ /\ E. n e. ZZ ( M <_ n /\ ph ) ) )
11 9 10 bitri 
 |-  ( E. n e. ( ZZ>= ` M ) ph <-> ( M e. ZZ /\ E. n e. ZZ ( M <_ n /\ ph ) ) )