Metamath Proof Explorer

Theorem domunsn

Description: Dominance over a set with one element added. (Contributed by Mario Carneiro, 18-May-2015)

Ref Expression
Assertion domunsn 
|- ( A ~< B -> ( A u. { C } ) ~<_ B )

Proof

Step Hyp Ref Expression
1 sdom0 
 |-  -. A ~< (/)
2 breq2 
 |-  ( B = (/) -> ( A ~< B <-> A ~< (/) ) )
3 1 2 mtbiri 
 |-  ( B = (/) -> -. A ~< B )
4 3 con2i 
 |-  ( A ~< B -> -. B = (/) )
5 neq0 
 |-  ( -. B = (/) <-> E. z z e. B )
6 4 5 sylib 
 |-  ( A ~< B -> E. z z e. B )
7 domdifsn 
 |-  ( A ~< B -> A ~<_ ( B \ { z } ) )
8 7 adantr 
 |-  ( ( A ~< B /\ z e. B ) -> A ~<_ ( B \ { z } ) )
9 en2sn 
 |-  ( ( C e. _V /\ z e. _V ) -> { C } ~~ { z } )
10 9 elvd 
 |-  ( C e. _V -> { C } ~~ { z } )
11 endom 
 |-  ( { C } ~~ { z } -> { C } ~<_ { z } )
12 10 11 syl 
 |-  ( C e. _V -> { C } ~<_ { z } )
13 snprc 
 |-  ( -. C e. _V <-> { C } = (/) )
14 13 biimpi 
 |-  ( -. C e. _V -> { C } = (/) )
15 snex 
 |-  { z } e. _V
16 15 0dom 
 |-  (/) ~<_ { z }
17 14 16 eqbrtrdi 
 |-  ( -. C e. _V -> { C } ~<_ { z } )
18 12 17 pm2.61i 
 |-  { C } ~<_ { z }
19 incom 
 |-  ( ( B \ { z } ) i^i { z } ) = ( { z } i^i ( B \ { z } ) )
20 disjdif 
 |-  ( { z } i^i ( B \ { z } ) ) = (/)
21 19 20 eqtri 
 |-  ( ( B \ { z } ) i^i { z } ) = (/)
22 undom 
 |-  ( ( ( A ~<_ ( B \ { z } ) /\ { C } ~<_ { z } ) /\ ( ( B \ { z } ) i^i { z } ) = (/) ) -> ( A u. { C } ) ~<_ ( ( B \ { z } ) u. { z } ) )
23 21 22 mpan2 
 |-  ( ( A ~<_ ( B \ { z } ) /\ { C } ~<_ { z } ) -> ( A u. { C } ) ~<_ ( ( B \ { z } ) u. { z } ) )
24 8 18 23 sylancl 
 |-  ( ( A ~< B /\ z e. B ) -> ( A u. { C } ) ~<_ ( ( B \ { z } ) u. { z } ) )
25 uncom 
 |-  ( ( B \ { z } ) u. { z } ) = ( { z } u. ( B \ { z } ) )
26 simpr 
 |-  ( ( A ~< B /\ z e. B ) -> z e. B )
27 26 snssd 
 |-  ( ( A ~< B /\ z e. B ) -> { z } C_ B )
28 undif 
 |-  ( { z } C_ B <-> ( { z } u. ( B \ { z } ) ) = B )
29 27 28 sylib 
 |-  ( ( A ~< B /\ z e. B ) -> ( { z } u. ( B \ { z } ) ) = B )
30 25 29 syl5eq 
 |-  ( ( A ~< B /\ z e. B ) -> ( ( B \ { z } ) u. { z } ) = B )
31 24 30 breqtrd 
 |-  ( ( A ~< B /\ z e. B ) -> ( A u. { C } ) ~<_ B )
32 6 31 exlimddv 
 |-  ( A ~< B -> ( A u. { C } ) ~<_ B )