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 )