Metamath Proof Explorer

Theorem eltop2

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

Ref Expression
Assertion eltop2 ⊢ J ∈ Top → A ∈ J ↔ ∀ x ∈ A ∃ y ∈ J x ∈ y ∧ y ⊆ A

Proof

Step Hyp Ref Expression
1 tgtop ⊢ J ∈ Top → topGen ⁡ J = J
2 1 eleq2d ⊢ J ∈ Top → A ∈ topGen ⁡ J ↔ A ∈ J
3 eltg2b ⊢ J ∈ Top → A ∈ topGen ⁡ J ↔ ∀ x ∈ A ∃ y ∈ J x ∈ y ∧ y ⊆ A
4 2 3 bitr3d ⊢ J ∈ Top → A ∈ J ↔ ∀ x ∈ A ∃ y ∈ J x ∈ y ∧ y ⊆ A