Metamath Proof Explorer

Theorem pwdom

Description: Injection of sets implies injection on power sets. (Contributed by Mario Carneiro, 9-Apr-2015)

Ref Expression
Assertion pwdom 
|- ( A ~<_ B -> ~P A ~<_ ~P B )

Proof

Step Hyp Ref Expression
1 pweq 
 |-  ( A = (/) -> ~P A = ~P (/) )
2 1 breq1d 
 |-  ( A = (/) -> ( ~P A ~<_ ~P B <-> ~P (/) ~<_ ~P B ) )
3 reldom 
 |-  Rel ~<_
4 3 brrelex1i 
 |-  ( A ~<_ B -> A e. _V )
5 0sdomg 
 |-  ( A e. _V -> ( (/) ~< A <-> A =/= (/) ) )
6 4 5 syl 
 |-  ( A ~<_ B -> ( (/) ~< A <-> A =/= (/) ) )
7 6 biimpar 
 |-  ( ( A ~<_ B /\ A =/= (/) ) -> (/) ~< A )
8 simpl 
 |-  ( ( A ~<_ B /\ A =/= (/) ) -> A ~<_ B )
9 fodomr 
 |-  ( ( (/) ~< A /\ A ~<_ B ) -> E. f f : B -onto-> A )
10 7 8 9 syl2anc 
 |-  ( ( A ~<_ B /\ A =/= (/) ) -> E. f f : B -onto-> A )
11 vex 
 |-  f e. _V
12 fopwdom 
 |-  ( ( f e. _V /\ f : B -onto-> A ) -> ~P A ~<_ ~P B )
13 11 12 mpan 
 |-  ( f : B -onto-> A -> ~P A ~<_ ~P B )
14 13 exlimiv 
 |-  ( E. f f : B -onto-> A -> ~P A ~<_ ~P B )
15 10 14 syl 
 |-  ( ( A ~<_ B /\ A =/= (/) ) -> ~P A ~<_ ~P B )
16 3 brrelex2i 
 |-  ( A ~<_ B -> B e. _V )
17 16 pwexd 
 |-  ( A ~<_ B -> ~P B e. _V )
18 0ss 
 |-  (/) C_ B
19 18 sspwi 
 |-  ~P (/) C_ ~P B
20 ssdomg 
 |-  ( ~P B e. _V -> ( ~P (/) C_ ~P B -> ~P (/) ~<_ ~P B ) )
21 17 19 20 mpisyl 
 |-  ( A ~<_ B -> ~P (/) ~<_ ~P B )
22 2 15 21 pm2.61ne 
 |-  ( A ~<_ B -> ~P A ~<_ ~P B )