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 ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑃 ∈ 𝑋 ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) ) )