Theorem eltop2

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

	Ref	Expression
Assertion	eltop2	⊢ ( 𝐽 ∈ Top → ( 𝐴 ∈ 𝐽 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		tgtop	⊢ ( 𝐽 ∈ Top → ( topGen ‘ 𝐽 ) = 𝐽 )
2	1	eleq2d	⊢ ( 𝐽 ∈ Top → ( 𝐴 ∈ ( topGen ‘ 𝐽 ) ↔ 𝐴 ∈ 𝐽 ) )
3		eltg2b	⊢ ( 𝐽 ∈ Top → ( 𝐴 ∈ ( topGen ‘ 𝐽 ) ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴 ) ) )
4	2 3	bitr3d	⊢ ( 𝐽 ∈ Top → ( 𝐴 ∈ 𝐽 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴 ) ) )