Metamath Proof Explorer


Theorem eltop

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

Ref Expression
Assertion eltop ( 𝐽 ∈ Top → ( 𝐴𝐽𝐴 ( 𝐽 ∩ 𝒫 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 tgtop ( 𝐽 ∈ Top → ( topGen ‘ 𝐽 ) = 𝐽 )
2 1 eleq2d ( 𝐽 ∈ Top → ( 𝐴 ∈ ( topGen ‘ 𝐽 ) ↔ 𝐴𝐽 ) )
3 eltg ( 𝐽 ∈ Top → ( 𝐴 ∈ ( topGen ‘ 𝐽 ) ↔ 𝐴 ( 𝐽 ∩ 𝒫 𝐴 ) ) )
4 2 3 bitr3d ( 𝐽 ∈ Top → ( 𝐴𝐽𝐴 ( 𝐽 ∩ 𝒫 𝐴 ) ) )