Metamath Proof Explorer

Theorem 0opn

Description: The empty set is an open subset of any topology. (Contributed by Stefan Allan, 27-Feb-2006)

Ref Expression
Assertion 0opn 
|- ( J e. Top -> (/) e. J )

Proof

Step Hyp Ref Expression
1 uni0 
 |-  U. (/) = (/)
2 0ss 
 |-  (/) C_ J
3 uniopn 
 |-  ( ( J e. Top /\ (/) C_ J ) -> U. (/) e. J )
4 2 3 mpan2 
 |-  ( J e. Top -> U. (/) e. J )
5 1 4 eqeltrrid 
 |-  ( J e. Top -> (/) e. J )