Metamath Proof Explorer

Theorem raluz2

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

Ref Expression
Assertion raluz2 
|- ( A. n e. ( ZZ>= ` M ) ph <-> ( M e. ZZ -> A. 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 3anass 
 |-  ( ( 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 imbi1i 
 |-  ( ( n e. ( ZZ>= ` M ) -> ph ) <-> ( ( M e. ZZ /\ ( n e. ZZ /\ M <_ n ) ) -> ph ) )
5 impexp 
 |-  ( ( ( M e. ZZ /\ ( n e. ZZ /\ M <_ n ) ) -> ph ) <-> ( M e. ZZ -> ( ( n e. ZZ /\ M <_ n ) -> ph ) ) )
6 impexp 
 |-  ( ( ( n e. ZZ /\ M <_ n ) -> ph ) <-> ( n e. ZZ -> ( M <_ n -> ph ) ) )
7 6 imbi2i 
 |-  ( ( M e. ZZ -> ( ( n e. ZZ /\ M <_ n ) -> ph ) ) <-> ( M e. ZZ -> ( n e. ZZ -> ( M <_ n -> ph ) ) ) )
8 5 7 bitri 
 |-  ( ( ( M e. ZZ /\ ( n e. ZZ /\ M <_ n ) ) -> ph ) <-> ( M e. ZZ -> ( n e. ZZ -> ( M <_ n -> ph ) ) ) )
9 bi2.04 
 |-  ( ( M e. ZZ -> ( n e. ZZ -> ( M <_ n -> ph ) ) ) <-> ( n e. ZZ -> ( M e. ZZ -> ( M <_ n -> ph ) ) ) )
10 8 9 bitri 
 |-  ( ( ( M e. ZZ /\ ( n e. ZZ /\ M <_ n ) ) -> ph ) <-> ( n e. ZZ -> ( M e. ZZ -> ( M <_ n -> ph ) ) ) )
11 4 10 bitri 
 |-  ( ( n e. ( ZZ>= ` M ) -> ph ) <-> ( n e. ZZ -> ( M e. ZZ -> ( M <_ n -> ph ) ) ) )
12 11 ralbii2 
 |-  ( A. n e. ( ZZ>= ` M ) ph <-> A. n e. ZZ ( M e. ZZ -> ( M <_ n -> ph ) ) )
13 r19.21v 
 |-  ( A. n e. ZZ ( M e. ZZ -> ( M <_ n -> ph ) ) <-> ( M e. ZZ -> A. n e. ZZ ( M <_ n -> ph ) ) )
14 12 13 bitri 
 |-  ( A. n e. ( ZZ>= ` M ) ph <-> ( M e. ZZ -> A. n e. ZZ ( M <_ n -> ph ) ) )