Metamath Proof Explorer

Theorem inopn

Description: The intersection of two open sets of a topology is an open set. (Contributed by NM, 17-Jul-2006)

Ref Expression
Assertion inopn 
|- ( ( J e. Top /\ A e. J /\ B e. J ) -> ( A i^i B ) e. J )

Proof

Step Hyp Ref Expression
1 istopg 
 |-  ( J e. Top -> ( J e. Top <-> ( A. x ( x C_ J -> U. x e. J ) /\ A. x e. J A. y e. J ( x i^i y ) e. J ) ) )
2 1 ibi 
 |-  ( J e. Top -> ( A. x ( x C_ J -> U. x e. J ) /\ A. x e. J A. y e. J ( x i^i y ) e. J ) )
3 2 simprd 
 |-  ( J e. Top -> A. x e. J A. y e. J ( x i^i y ) e. J )
4 ineq1 
 |-  ( x = A -> ( x i^i y ) = ( A i^i y ) )
5 4 eleq1d 
 |-  ( x = A -> ( ( x i^i y ) e. J <-> ( A i^i y ) e. J ) )
6 ineq2 
 |-  ( y = B -> ( A i^i y ) = ( A i^i B ) )
7 6 eleq1d 
 |-  ( y = B -> ( ( A i^i y ) e. J <-> ( A i^i B ) e. J ) )
8 5 7 rspc2v 
 |-  ( ( A e. J /\ B e. J ) -> ( A. x e. J A. y e. J ( x i^i y ) e. J -> ( A i^i B ) e. J ) )
9 3 8 syl5com 
 |-  ( J e. Top -> ( ( A e. J /\ B e. J ) -> ( A i^i B ) e. J ) )
10 9 3impib 
 |-  ( ( J e. Top /\ A e. J /\ B e. J ) -> ( A i^i B ) e. J )