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

Metamath Proof Explorer

Theorem eltop

Description: Membership in a topology, expressed without quantifiers. (Contributed by NM, 19-Jul-2006)

Ref Expression
Assertion eltop ⊢ J ∈ Top → A ∈ J ↔ A ⊆ ⋃ J ∩ 𝒫 A

Proof

Step Hyp Ref Expression
1 tgtop ⊢ J ∈ Top → topGen ⁡ J = J
2 1 eleq2d ⊢ J ∈ Top → A ∈ topGen ⁡ J ↔ A ∈ J
3 eltg ⊢ J ∈ Top → A ∈ topGen ⁡ J ↔ A ⊆ ⋃ J ∩ 𝒫 A
4 2 3 bitr3d ⊢ J ∈ Top → A ∈ J ↔ A ⊆ ⋃ J ∩ 𝒫 A