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 ∈ J P ∈ 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 ∈ J P ∈ x → x ∩ S ≠ ∅
7 6 3expa ⊢ J ∈ Top ∧ S ⊆ X ∧ P ∈ X → P ∈ cls ⁡ J ⁡ S ↔ ∀ x ∈ J P ∈ x → x ∩ S ≠ ∅
8 7 pm5.32da ⊢ J ∈ Top ∧ S ⊆ X → P ∈ X ∧ P ∈ cls ⁡ J ⁡ S ↔ P ∈ X ∧ ∀ x ∈ J P ∈ x → x ∩ S ≠ ∅
9 5 8 bitrd ⊢ J ∈ Top ∧ S ⊆ X → P ∈ cls ⁡ J ⁡ S ↔ P ∈ X ∧ ∀ x ∈ J P ∈ x → x ∩ S ≠ ∅