Metamath Proof Explorer

Theorem isopn2

Description: A subset of the underlying set of a topology is open iff its complement is closed. (Contributed by NM, 4-Oct-2006)

Ref Expression
Hypothesis iscld.1 ${⊢}{X}=\bigcup {J}$
Assertion isopn2 ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \left({S}\in {J}↔{X}\setminus {S}\in \mathrm{Clsd}\left({J}\right)\right)$

Proof

Step Hyp Ref Expression
1 iscld.1 ${⊢}{X}=\bigcup {J}$
2 difss ${⊢}{X}\setminus {S}\subseteq {X}$
3 1 iscld2 ${⊢}\left({J}\in \mathrm{Top}\wedge {X}\setminus {S}\subseteq {X}\right)\to \left({X}\setminus {S}\in \mathrm{Clsd}\left({J}\right)↔{X}\setminus \left({X}\setminus {S}\right)\in {J}\right)$
4 2 3 mpan2 ${⊢}{J}\in \mathrm{Top}\to \left({X}\setminus {S}\in \mathrm{Clsd}\left({J}\right)↔{X}\setminus \left({X}\setminus {S}\right)\in {J}\right)$
5 dfss4 ${⊢}{S}\subseteq {X}↔{X}\setminus \left({X}\setminus {S}\right)={S}$
6 5 biimpi ${⊢}{S}\subseteq {X}\to {X}\setminus \left({X}\setminus {S}\right)={S}$
7 6 eleq1d ${⊢}{S}\subseteq {X}\to \left({X}\setminus \left({X}\setminus {S}\right)\in {J}↔{S}\in {J}\right)$
8 4 7 sylan9bb ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \left({X}\setminus {S}\in \mathrm{Clsd}\left({J}\right)↔{S}\in {J}\right)$
9 8 bicomd ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \left({S}\in {J}↔{X}\setminus {S}\in \mathrm{Clsd}\left({J}\right)\right)$