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 → ( 𝐴 ∈ 𝐽 ↔ 𝐴 ⊆ ∪ ( 𝐽 ∩ 𝒫 𝐴 ) ) )