Metamath Proof Explorer

Theorem toponss

Description: A member of a topology is a subset of its underlying set. (Contributed by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion toponss 
|- ( ( J e. ( TopOn ` X ) /\ A e. J ) -> A C_ X )

Proof

Step Hyp Ref Expression
1 elssuni 
 |-  ( A e. J -> A C_ U. J )
2 1 adantl 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. J ) -> A C_ U. J )
3 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
4 3 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. J ) -> X = U. J )
5 2 4 sseqtrrd 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. J ) -> A C_ X )