This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elcls2

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

Ref Expression
Hypothesis clscld.1 ⊢ 𝑋 = ∪ 𝐽
Assertion elcls2 ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑃 ∈ 𝑋 ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) ) )

Proof

Step Hyp Ref Expression
1 clscld.1 ⊢ 𝑋 = ∪ 𝐽
2 1 clsss3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑋 )
3 ssel ⊢ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑋 → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) → 𝑃 ∈ 𝑋 ) )
4 3 pm4.71rd ⊢ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑋 → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑃 ∈ 𝑋 ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) )
5 2 4 syl ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑃 ∈ 𝑋 ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) )
6 1 elcls ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) )
7 6 3expa ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) )
8 7 pm5.32da ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝑃 ∈ 𝑋 ∧ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ↔ ( 𝑃 ∈ 𝑋 ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) ) )
9 5 8 bitrd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑃 ∈ 𝑋 ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) ) )