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

Theorem restopn2 20128
Description: The if  A is open, then  B is open in  A iff it is an open subset of  A. (Contributed by Mario Carneiro, 2-Mar-2015.)
Assertion
Ref Expression
restopn2  |-  ( ( J  e.  Top  /\  A  e.  J )  ->  ( B  e.  ( Jt  A )  <->  ( B  e.  J  /\  B  C_  A ) ) )

Proof of Theorem restopn2
StepHypRef Expression
1 elssuni 4184 . . . . 5  |-  ( B  e.  ( Jt  A )  ->  B  C_  U. ( Jt  A ) )
2 elssuni 4184 . . . . . . 7  |-  ( A  e.  J  ->  A  C_ 
U. J )
3 eqid 2422 . . . . . . . 8  |-  U. J  =  U. J
43restuni 20113 . . . . . . 7  |-  ( ( J  e.  Top  /\  A  C_  U. J )  ->  A  =  U. ( Jt  A ) )
52, 4sylan2 476 . . . . . 6  |-  ( ( J  e.  Top  /\  A  e.  J )  ->  A  =  U. ( Jt  A ) )
65sseq2d 3428 . . . . 5  |-  ( ( J  e.  Top  /\  A  e.  J )  ->  ( B  C_  A  <->  B 
C_  U. ( Jt  A ) ) )
71, 6syl5ibr 224 . . . 4  |-  ( ( J  e.  Top  /\  A  e.  J )  ->  ( B  e.  ( Jt  A )  ->  B  C_  A ) )
87pm4.71rd 639 . . 3  |-  ( ( J  e.  Top  /\  A  e.  J )  ->  ( B  e.  ( Jt  A )  <->  ( B  C_  A  /\  B  e.  ( Jt  A ) ) ) )
9 simpll 758 . . . . 5  |-  ( ( ( J  e.  Top  /\  A  e.  J )  /\  B  C_  A
)  ->  J  e.  Top )
10 simplr 760 . . . . 5  |-  ( ( ( J  e.  Top  /\  A  e.  J )  /\  B  C_  A
)  ->  A  e.  J )
11 ssid 3419 . . . . . 6  |-  A  C_  A
1211a1i 11 . . . . 5  |-  ( ( ( J  e.  Top  /\  A  e.  J )  /\  B  C_  A
)  ->  A  C_  A
)
13 simpr 462 . . . . 5  |-  ( ( ( J  e.  Top  /\  A  e.  J )  /\  B  C_  A
)  ->  B  C_  A
)
14 restopnb 20126 . . . . 5  |-  ( ( ( J  e.  Top  /\  A  e.  J )  /\  ( A  e.  J  /\  A  C_  A  /\  B  C_  A
) )  ->  ( B  e.  J  <->  B  e.  ( Jt  A ) ) )
159, 10, 10, 12, 13, 14syl23anc 1271 . . . 4  |-  ( ( ( J  e.  Top  /\  A  e.  J )  /\  B  C_  A
)  ->  ( B  e.  J  <->  B  e.  ( Jt  A ) ) )
1615pm5.32da 645 . . 3  |-  ( ( J  e.  Top  /\  A  e.  J )  ->  ( ( B  C_  A  /\  B  e.  J
)  <->  ( B  C_  A  /\  B  e.  ( Jt  A ) ) ) )
178, 16bitr4d 259 . 2  |-  ( ( J  e.  Top  /\  A  e.  J )  ->  ( B  e.  ( Jt  A )  <->  ( B  C_  A  /\  B  e.  J ) ) )
18 ancom 451 . 2  |-  ( ( B  C_  A  /\  B  e.  J )  <->  ( B  e.  J  /\  B  C_  A ) )
1917, 18syl6bb 264 1  |-  ( ( J  e.  Top  /\  A  e.  J )  ->  ( B  e.  ( Jt  A )  <->  ( B  e.  J  /\  B  C_  A ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437    e. wcel 1872    C_ wss 3372   U.cuni 4155  (class class class)co 6242   ↾t crest 15255   Topctop 19852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2402  ax-rep 4472  ax-sep 4482  ax-nul 4491  ax-pow 4538  ax-pr 4596  ax-un 6534
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2274  df-mo 2275  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2552  df-ne 2595  df-ral 2713  df-rex 2714  df-reu 2715  df-rab 2717  df-v 3018  df-sbc 3236  df-csb 3332  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-pss 3388  df-nul 3698  df-if 3848  df-pw 3919  df-sn 3935  df-pr 3937  df-tp 3939  df-op 3941  df-uni 4156  df-int 4192  df-iun 4237  df-br 4360  df-opab 4419  df-mpt 4420  df-tr 4455  df-eprel 4700  df-id 4704  df-po 4710  df-so 4711  df-fr 4748  df-we 4750  df-xp 4795  df-rel 4796  df-cnv 4797  df-co 4798  df-dm 4799  df-rn 4800  df-res 4801  df-ima 4802  df-pred 5335  df-ord 5381  df-on 5382  df-lim 5383  df-suc 5384  df-iota 5501  df-fun 5539  df-fn 5540  df-f 5541  df-f1 5542  df-fo 5543  df-f1o 5544  df-fv 5545  df-ov 6245  df-oprab 6246  df-mpt2 6247  df-om 6644  df-1st 6744  df-2nd 6745  df-wrecs 6976  df-recs 7038  df-rdg 7076  df-oadd 7134  df-er 7311  df-en 7518  df-fin 7521  df-fi 7871  df-rest 15257  df-topgen 15278  df-top 19856  df-bases 19857  df-topon 19858
This theorem is referenced by:  restdis  20129  perfopn  20136  llyrest  20435  nllyrest  20436  llyidm  20438  nllyidm  20439  lly1stc  20446  qtoprest  20667  xrtgioo  21759  lhop  22903  efopnlem2  23537  cvmopnlem  29946  cvmlift2lem9a  29971  cvmlift2lem9  29979  cvmlift3lem6  29992
  Copyright terms: Public domain W3C validator