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		disjdifr	|- ( ( B \ { z } ) i^i { z } ) = (/)
20		undom	|- ( ( ( A ~<_ ( B \ { z } ) /\ { C } ~<_ { z } ) /\ ( ( B \ { z } ) i^i { z } ) = (/) ) -> ( A u. { C } ) ~<_ ( ( B \ { z } ) u. { z } ) )
21	19 20	mpan2	|- ( ( A ~<_ ( B \ { z } ) /\ { C } ~<_ { z } ) -> ( A u. { C } ) ~<_ ( ( B \ { z } ) u. { z } ) )
22	8 18 21	sylancl	|- ( ( A ~< B /\ z e. B ) -> ( A u. { C } ) ~<_ ( ( B \ { z } ) u. { z } ) )
23		uncom	|- ( ( B \ { z } ) u. { z } ) = ( { z } u. ( B \ { z } ) )
24		simpr	|- ( ( A ~< B /\ z e. B ) -> z e. B )
25	24	snssd	|- ( ( A ~< B /\ z e. B ) -> { z } C_ B )
26		undif	|- ( { z } C_ B <-> ( { z } u. ( B \ { z } ) ) = B )
27	25 26	sylib	|- ( ( A ~< B /\ z e. B ) -> ( { z } u. ( B \ { z } ) ) = B )
28	23 27	eqtrid	|- ( ( A ~< B /\ z e. B ) -> ( ( B \ { z } ) u. { z } ) = B )
29	22 28	breqtrd	|- ( ( A ~< B /\ z e. B ) -> ( A u. { C } ) ~<_ B )
30	6 29	exlimddv	|- ( A ~< B -> ( A u. { C } ) ~<_ B )