Metamath Proof Explorer

Theorem uzin2

Description: The upper integers are closed under intersection. (Contributed by Mario Carneiro, 24-Dec-2013)

Ref Expression
Assertion uzin2 
|- ( ( A e. ran ZZ>= /\ B e. ran ZZ>= ) -> ( A i^i B ) e. ran ZZ>= )

Proof

Step Hyp Ref Expression
1 uzf 
 |-  ZZ>= : ZZ --> ~P ZZ
2 ffn 
 |-  ( ZZ>= : ZZ --> ~P ZZ -> ZZ>= Fn ZZ )
3 1 2 ax-mp 
 |-  ZZ>= Fn ZZ
4 fvelrnb 
 |-  ( ZZ>= Fn ZZ -> ( A e. ran ZZ>= <-> E. x e. ZZ ( ZZ>= ` x ) = A ) )
5 3 4 ax-mp 
 |-  ( A e. ran ZZ>= <-> E. x e. ZZ ( ZZ>= ` x ) = A )
6 fvelrnb 
 |-  ( ZZ>= Fn ZZ -> ( B e. ran ZZ>= <-> E. y e. ZZ ( ZZ>= ` y ) = B ) )
7 3 6 ax-mp 
 |-  ( B e. ran ZZ>= <-> E. y e. ZZ ( ZZ>= ` y ) = B )
8 ineq1 
 |-  ( ( ZZ>= ` x ) = A -> ( ( ZZ>= ` x ) i^i ( ZZ>= ` y ) ) = ( A i^i ( ZZ>= ` y ) ) )
9 8 eleq1d 
 |-  ( ( ZZ>= ` x ) = A -> ( ( ( ZZ>= ` x ) i^i ( ZZ>= ` y ) ) e. ran ZZ>= <-> ( A i^i ( ZZ>= ` y ) ) e. ran ZZ>= ) )
10 ineq2 
 |-  ( ( ZZ>= ` y ) = B -> ( A i^i ( ZZ>= ` y ) ) = ( A i^i B ) )
11 10 eleq1d 
 |-  ( ( ZZ>= ` y ) = B -> ( ( A i^i ( ZZ>= ` y ) ) e. ran ZZ>= <-> ( A i^i B ) e. ran ZZ>= ) )
12 uzin 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( ( ZZ>= ` x ) i^i ( ZZ>= ` y ) ) = ( ZZ>= ` if ( x <_ y , y , x ) ) )
13 ifcl 
 |-  ( ( y e. ZZ /\ x e. ZZ ) -> if ( x <_ y , y , x ) e. ZZ )
14 13 ancoms 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> if ( x <_ y , y , x ) e. ZZ )
15 fnfvelrn 
 |-  ( ( ZZ>= Fn ZZ /\ if ( x <_ y , y , x ) e. ZZ ) -> ( ZZ>= ` if ( x <_ y , y , x ) ) e. ran ZZ>= )
16 3 14 15 sylancr 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( ZZ>= ` if ( x <_ y , y , x ) ) e. ran ZZ>= )
17 12 16 eqeltrd 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( ( ZZ>= ` x ) i^i ( ZZ>= ` y ) ) e. ran ZZ>= )
18 5 7 9 11 17 2gencl 
 |-  ( ( A e. ran ZZ>= /\ B e. ran ZZ>= ) -> ( A i^i B ) e. ran ZZ>= )