Description: Membership in a topology, expressed without quantifiers. (Contributed by NM, 19-Jul-2006)
Ref | Expression | ||
---|---|---|---|
Assertion | eltop | ⊢ ( 𝐽 ∈ Top → ( 𝐴 ∈ 𝐽 ↔ 𝐴 ⊆ ∪ ( 𝐽 ∩ 𝒫 𝐴 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tgtop | ⊢ ( 𝐽 ∈ Top → ( topGen ‘ 𝐽 ) = 𝐽 ) | |
2 | 1 | eleq2d | ⊢ ( 𝐽 ∈ Top → ( 𝐴 ∈ ( topGen ‘ 𝐽 ) ↔ 𝐴 ∈ 𝐽 ) ) |
3 | eltg | ⊢ ( 𝐽 ∈ Top → ( 𝐴 ∈ ( topGen ‘ 𝐽 ) ↔ 𝐴 ⊆ ∪ ( 𝐽 ∩ 𝒫 𝐴 ) ) ) | |
4 | 2 3 | bitr3d | ⊢ ( 𝐽 ∈ Top → ( 𝐴 ∈ 𝐽 ↔ 𝐴 ⊆ ∪ ( 𝐽 ∩ 𝒫 𝐴 ) ) ) |