Metamath Proof Explorer

Theorem elcls2

Description: Membership in a closure. (Contributed by NM, 5-Mar-2007)

Ref Expression
Hypothesis clscld.1 ⊢X=⋃J
Assertion elcls2 ⊢J∈Top∧S⊆X→P∈cls⁡J⁡S↔P∈X∧∀x∈JP∈x→x∩S≠∅

Proof

Step Hyp Ref Expression
1 clscld.1 ⊢X=⋃J
2 1 clsss3 ⊢J∈Top∧S⊆X→cls⁡J⁡S⊆X
3 ssel ⊢cls⁡J⁡S⊆X→P∈cls⁡J⁡S→P∈X
4 3 pm4.71rd ⊢cls⁡J⁡S⊆X→P∈cls⁡J⁡S↔P∈X∧P∈cls⁡J⁡S
5 2 4 syl ⊢J∈Top∧S⊆X→P∈cls⁡J⁡S↔P∈X∧P∈cls⁡J⁡S
6 1 elcls ⊢J∈Top∧S⊆X∧P∈X→P∈cls⁡J⁡S↔∀x∈JP∈x→x∩S≠∅
7 6 3expa ⊢J∈Top∧S⊆X∧P∈X→P∈cls⁡J⁡S↔∀x∈JP∈x→x∩S≠∅
8 7 pm5.32da ⊢J∈Top∧S⊆X→P∈X∧P∈cls⁡J⁡S↔P∈X∧∀x∈JP∈x→x∩S≠∅
9 5 8 bitrd ⊢J∈Top∧S⊆X→P∈cls⁡J⁡S↔P∈X∧∀x∈JP∈x→x∩S≠∅