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 ) =/= (/) )