Metamath Proof Explorer

Theorem sdom0

Description: The empty set does not strictly dominate any set. (Contributed by NM, 26-Oct-2003)

Ref Expression
Assertion sdom0 
|- -. A ~< (/)

Proof

Step Hyp Ref Expression
1 relsdom 
 |-  Rel ~<
2 1 brrelex1i 
 |-  ( A ~< (/) -> A e. _V )
3 0domg 
 |-  ( A e. _V -> (/) ~<_ A )
4 2 3 syl 
 |-  ( A ~< (/) -> (/) ~<_ A )
5 domnsym 
 |-  ( (/) ~<_ A -> -. A ~< (/) )
6 5 con2i 
 |-  ( A ~< (/) -> -. (/) ~<_ A )
7 4 6 pm2.65i 
 |-  -. A ~< (/)