Theorem isopn3i 22177

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

Step	Hyp	Ref	Expression
1		simpr 484	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽) → 𝑆 ∈ 𝐽)
2		elssuni 4873	. . 3 ⊢ (𝑆 ∈ 𝐽 → 𝑆 ⊆ ∪ 𝐽)
3		eqid 2737	. . . 4 ⊢ ∪ 𝐽 = ∪ 𝐽
4	3	isopn3 22161	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽) → (𝑆 ∈ 𝐽 ↔ ((int‘𝐽)‘𝑆) = 𝑆))
5	2, 4	sylan2 592	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽) → (𝑆 ∈ 𝐽 ↔ ((int‘𝐽)‘𝑆) = 𝑆))
6	1, 5	mpbid 231	1 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽) → ((int‘𝐽)‘𝑆) = 𝑆)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539   ∈ wcel 2107   ⊆ wss 3888  ∪ cuni 4841  ‘cfv 6423  Topctop 21986  intcnt 22112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5210  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7571

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3067  df-rex 3068  df-reu 3069  df-rab 3071  df-v 3429  df-sbc 3717  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4259  df-if 4462  df-pw 4537  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4842  df-iun 4928  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5485  df-xp 5591  df-rel 5592  df-cnv 5593  df-co 5594  df-dm 5595  df-rn 5596  df-res 5597  df-ima 5598  df-iota 6381  df-fun 6425  df-fn 6426  df-f 6427  df-f1 6428  df-fo 6429  df-f1o 6430  df-fv 6431  df-top 21987  df-ntr 22115

This theorem is referenced by:  maxlp  22242  cnntr  22370  bcth2  24437  dvrec  25062  dvmptres  25070  dvcnvlem  25083  dvlip  25100  dvlipcn  25101  dvlip2  25102  dvne0  25118  lhop2  25122  lhop  25123  psercn  25528  dvlog  25749  dvlog2  25751  cxpcn3  25844  efrlim  26062  lgamgulmlem2  26122  cvmlift2lem11  33217  cvmlift2lem12  33218  dvrelog3  40043  binomcxplemdvbinom  41902  binomcxplemnotnn0  41905  limciccioolb  43094  limcicciooub  43110  limcresiooub  43115  limcresioolb  43116  dirkercncflem2  43577  fourierdlem32  43612  fourierdlem33  43613  fourierdlem48  43627  fourierdlem49  43628  fourierdlem62  43641  fouriersw  43704