Theorem wdompwdom

Description: Weak dominance strengthens to usual dominance on the power sets. (Contributed by Stefan O'Rear, 11-Feb-2015) (Revised by Mario Carneiro, 5-May-2015)

	Ref	Expression
Assertion	wdompwdom	|- ( X ~<_* Y -> ~P X ~<_ ~P Y )

Proof

Step	Hyp	Ref	Expression
1		relwdom	|- Rel ~<_*
2	1	brrelex2i	|- ( X ~<_* Y -> Y e. _V )
3	2	pwexd	|- ( X ~<_* Y -> ~P Y e. _V )
4		0ss	|- (/) C_ Y
5	4	sspwi	|- ~P (/) C_ ~P Y
6		ssdomg	|- ( ~P Y e. _V -> ( ~P (/) C_ ~P Y -> ~P (/) ~<_ ~P Y ) )
7	3 5 6	mpisyl	|- ( X ~<_* Y -> ~P (/) ~<_ ~P Y )
8		pweq	|- ( X = (/) -> ~P X = ~P (/) )
9	8	breq1d	|- ( X = (/) -> ( ~P X ~<_ ~P Y <-> ~P (/) ~<_ ~P Y ) )
10	7 9	imbitrrid	|- ( X = (/) -> ( X ~<_* Y -> ~P X ~<_ ~P Y ) )
11		brwdomn0	|- ( X =/= (/) -> ( X ~<_* Y <-> E. z z : Y -onto-> X ) )
12		vex	|- z e. _V
13		fopwdom	|- ( ( z e. _V /\ z : Y -onto-> X ) -> ~P X ~<_ ~P Y )
14	12 13	mpan	|- ( z : Y -onto-> X -> ~P X ~<_ ~P Y )
15	14	exlimiv	|- ( E. z z : Y -onto-> X -> ~P X ~<_ ~P Y )
16	11 15	biimtrdi	|- ( X =/= (/) -> ( X ~<_* Y -> ~P X ~<_ ~P Y ) )
17	10 16	pm2.61ine	|- ( X ~<_* Y -> ~P X ~<_ ~P Y )