MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iscld Structured version   Unicode version

Theorem iscld 19373
Description: The predicate " S is a closed set." (Contributed by NM, 2-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
Hypothesis
Ref Expression
iscld.1  |-  X  = 
U. J
Assertion
Ref Expression
iscld  |-  ( J  e.  Top  ->  ( S  e.  ( Clsd `  J )  <->  ( S  C_  X  /\  ( X 
\  S )  e.  J ) ) )

Proof of Theorem iscld
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 iscld.1 . . . . 5  |-  X  = 
U. J
21cldval 19369 . . . 4  |-  ( J  e.  Top  ->  ( Clsd `  J )  =  { x  e.  ~P X  |  ( X  \  x )  e.  J } )
32eleq2d 2537 . . 3  |-  ( J  e.  Top  ->  ( S  e.  ( Clsd `  J )  <->  S  e.  { x  e.  ~P X  |  ( X  \  x )  e.  J } ) )
4 difeq2 3621 . . . . 5  |-  ( x  =  S  ->  ( X  \  x )  =  ( X  \  S
) )
54eleq1d 2536 . . . 4  |-  ( x  =  S  ->  (
( X  \  x
)  e.  J  <->  ( X  \  S )  e.  J
) )
65elrab 3266 . . 3  |-  ( S  e.  { x  e. 
~P X  |  ( X  \  x )  e.  J }  <->  ( S  e.  ~P X  /\  ( X  \  S )  e.  J ) )
73, 6syl6bb 261 . 2  |-  ( J  e.  Top  ->  ( S  e.  ( Clsd `  J )  <->  ( S  e.  ~P X  /\  ( X  \  S )  e.  J ) ) )
81topopn 19261 . . . 4  |-  ( J  e.  Top  ->  X  e.  J )
9 elpw2g 4615 . . . 4  |-  ( X  e.  J  ->  ( S  e.  ~P X  <->  S 
C_  X ) )
108, 9syl 16 . . 3  |-  ( J  e.  Top  ->  ( S  e.  ~P X  <->  S 
C_  X ) )
1110anbi1d 704 . 2  |-  ( J  e.  Top  ->  (
( S  e.  ~P X  /\  ( X  \  S )  e.  J
)  <->  ( S  C_  X  /\  ( X  \  S )  e.  J
) ) )
127, 11bitrd 253 1  |-  ( J  e.  Top  ->  ( S  e.  ( Clsd `  J )  <->  ( S  C_  X  /\  ( X 
\  S )  e.  J ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1379    e. wcel 1767   {crab 2821    \ cdif 3478    C_ wss 3481   ~Pcpw 4015   U.cuni 4250   ` cfv 5593   Topctop 19240   Clsdccld 19362
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-rab 2826  df-v 3120  df-sbc 3337  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4251  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-iota 5556  df-fun 5595  df-fv 5601  df-top 19245  df-cld 19365
This theorem is referenced by:  iscld2  19374  cldss  19375  cldopn  19377  topcld  19381  discld  19435  indiscld  19437  restcld  19518  ordtcld1  19543  ordtcld2  19544  hauscmp  19752  txcld  19949  ptcld  19959  qtopcld  20059  opnsubg  20451  sszcld  21167  stoweidlem57  31648
  Copyright terms: Public domain W3C validator