Theorem eltop3

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

	Ref	Expression
Assertion	eltop3	⊢ ( 𝐽 ∈ Top → ( 𝐴 ∈ 𝐽 ↔ ∃ 𝑥 ( 𝑥 ⊆ 𝐽 ∧ 𝐴 = ∪ 𝑥 ) ) )

Proof

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