Theorem inopn 20704

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

Assertion

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

Proof of Theorem inopn

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		istopg 20700	. . . . 5 |- ( 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 256	. . . 4 |- ( 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 479	. . 3 |- ( J e. Top -> A. x e. J A. y e. J ( x i^i y ) e. J )
4		ineq1 3807	. . . . 5 |- ( x = A -> ( x i^i y ) = ( A i^i y ) )
5	4	eleq1d 2686	. . . 4 |- ( x = A -> ( ( x i^i y ) e. J <-> ( A i^i y ) e. J ) )
6		ineq2 3808	. . . . 5 |- ( y = B -> ( A i^i y ) = ( A i^i B ) )
7	6	eleq1d 2686	. . . 4 |- ( y = B -> ( ( A i^i y ) e. J <-> ( A i^i B ) e. J ) )
8	5, 7	rspc2v 3322	. . 3 |- ( ( 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 31	. 2 |- ( J e. Top -> ( ( A e. J /\ B e. J ) -> ( A i^i B ) e. J ) )
10	9	3impib 1262	1 |- ( ( J e. Top /\ A e. J /\ B e. J ) -> ( A i^i B ) e. J )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037   A.wal 1481   = wceq 1483   e. wcel 1990   A.wral 2912   i^i cin 3573   C_ wss 3574   U.cuni 4436   Topctop 20698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-v 3202  df-in 3581  df-ss 3588  df-pw 4160  df-top 20699

This theorem is referenced by:  fitop  20705  tgclb  20774  topbas  20776  difopn  20838  uncld  20845  ntrin  20865  toponmre  20897  innei  20929  restopnb  20979  ordtopn3  21000  cnprest  21093  islly2  21287  kgentopon  21341  llycmpkgen2  21353  ptbasin  21380  txcnp  21423  txcnmpt  21427  qtoptop2  21502  opnfbas  21646  hauspwpwf1  21791  mopnin  22302  reconnlem2  22630  lmxrge0  29998  cvmsss2  31256  cvmcov2  31257  icccncfext  40100