Metamath Proof Explorer

Theorem sdomdif

Description: The difference of a set from a smaller set cannot be empty. (Contributed by Mario Carneiro, 5-Feb-2013)

Ref Expression
Assertion sdomdif 
|- ( A ~< B -> ( B \ A ) =/= (/) )

Proof

Step Hyp Ref Expression
1 relsdom 
 |-  Rel ~<
2 1 brrelex1i 
 |-  ( A ~< B -> A e. _V )
3 ssdif0 
 |-  ( B C_ A <-> ( B \ A ) = (/) )
4 ssdomg 
 |-  ( A e. _V -> ( B C_ A -> B ~<_ A ) )
5 domnsym 
 |-  ( B ~<_ A -> -. A ~< B )
6 4 5 syl6 
 |-  ( A e. _V -> ( B C_ A -> -. A ~< B ) )
7 3 6 syl5bir 
 |-  ( A e. _V -> ( ( B \ A ) = (/) -> -. A ~< B ) )
8 2 7 syl 
 |-  ( A ~< B -> ( ( B \ A ) = (/) -> -. A ~< B ) )
9 8 con2d 
 |-  ( A ~< B -> ( A ~< B -> -. ( B \ A ) = (/) ) )
10 9 pm2.43i 
 |-  ( A ~< B -> -. ( B \ A ) = (/) )
11 10 neqned 
 |-  ( A ~< B -> ( B \ A ) =/= (/) )