MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isopn3i Structured version   Visualization version   GIF version

Theorem isopn3i 23004
Description: An open subset equals its own interior. (Contributed by Mario Carneiro, 30-Dec-2016.)
Assertion
Ref Expression
isopn3i ((𝐽 ∈ Top ∧ 𝑆𝐽) → ((int‘𝐽)‘𝑆) = 𝑆)

Proof of Theorem isopn3i
StepHypRef Expression
1 simpr 483 . 2 ((𝐽 ∈ Top ∧ 𝑆𝐽) → 𝑆𝐽)
2 elssuni 4942 . . 3 (𝑆𝐽𝑆 𝐽)
3 eqid 2727 . . . 4 𝐽 = 𝐽
43isopn3 22988 . . 3 ((𝐽 ∈ Top ∧ 𝑆 𝐽) → (𝑆𝐽 ↔ ((int‘𝐽)‘𝑆) = 𝑆))
52, 4sylan2 591 . 2 ((𝐽 ∈ Top ∧ 𝑆𝐽) → (𝑆𝐽 ↔ ((int‘𝐽)‘𝑆) = 𝑆))
61, 5mpbid 231 1 ((𝐽 ∈ Top ∧ 𝑆𝐽) → ((int‘𝐽)‘𝑆) = 𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394   = wceq 1533  wcel 2098  wss 3947   cuni 4910  cfv 6551  Topctop 22813  intcnt 22939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2698  ax-rep 5287  ax-sep 5301  ax-nul 5308  ax-pow 5367  ax-pr 5431  ax-un 7744
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2937  df-ral 3058  df-rex 3067  df-reu 3373  df-rab 3429  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4325  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4911  df-iun 5000  df-br 5151  df-opab 5213  df-mpt 5234  df-id 5578  df-xp 5686  df-rel 5687  df-cnv 5688  df-co 5689  df-dm 5690  df-rn 5691  df-res 5692  df-ima 5693  df-iota 6503  df-fun 6553  df-fn 6554  df-f 6555  df-f1 6556  df-fo 6557  df-f1o 6558  df-fv 6559  df-top 22814  df-ntr 22942
This theorem is referenced by:  maxlp  23069  cnntr  23197  bcth2  25276  dvrec  25905  dvmptres  25913  dvcnvlem  25926  dvlip  25944  dvlipcn  25945  dvlip2  25946  dvne0  25962  lhop2  25966  lhop  25967  psercn  26381  dvlog  26603  dvlog2  26605  cxpcn3  26701  efrlim  26919  efrlimOLD  26920  lgamgulmlem2  26980  cvmlift2lem11  34928  cvmlift2lem12  34929  dvrelog3  41540  binomcxplemdvbinom  43793  binomcxplemnotnn0  43796  limciccioolb  45011  limcicciooub  45027  limcresiooub  45032  limcresioolb  45033  dirkercncflem2  45494  fourierdlem32  45529  fourierdlem33  45530  fourierdlem48  45544  fourierdlem49  45545  fourierdlem62  45558  fouriersw  45621
  Copyright terms: Public domain W3C validator