Metamath Proof Explorer

Theorem eltopss

Description: A member of a topology is a subset of its underlying set. (Contributed by NM, 12-Sep-2006)

Ref Expression
Hypothesis 1open.1 
|- X = U. J
Assertion eltopss 
|- ( ( J e. Top /\ A e. J ) -> A C_ X )

Proof

Step Hyp Ref Expression
1 1open.1 
 |-  X = U. J
2 elssuni 
 |-  ( A e. J -> A C_ U. J )
3 2 1 sseqtrrdi 
 |-  ( A e. J -> A C_ X )
4 3 adantl 
 |-  ( ( J e. Top /\ A e. J ) -> A C_ X )