Metamath Proof Explorer

Theorem pwssun

Description: The power class of the union of two classes is a subset of the union of their power classes, iff one class is a subclass of the other. Exercise 4.12(l) of Mendelson p. 235. (Contributed by NM, 23-Nov-2003)

Ref Expression
Assertion pwssun 
|- ( ( A C_ B \/ B C_ A ) <-> ~P ( A u. B ) C_ ( ~P A u. ~P B ) )

Proof

Step Hyp Ref Expression
1 ssequn2 
 |-  ( B C_ A <-> ( A u. B ) = A )
2 pweq 
 |-  ( ( A u. B ) = A -> ~P ( A u. B ) = ~P A )
3 eqimss 
 |-  ( ~P ( A u. B ) = ~P A -> ~P ( A u. B ) C_ ~P A )
4 2 3 syl 
 |-  ( ( A u. B ) = A -> ~P ( A u. B ) C_ ~P A )
5 1 4 sylbi 
 |-  ( B C_ A -> ~P ( A u. B ) C_ ~P A )
6 ssequn1 
 |-  ( A C_ B <-> ( A u. B ) = B )
7 pweq 
 |-  ( ( A u. B ) = B -> ~P ( A u. B ) = ~P B )
8 eqimss 
 |-  ( ~P ( A u. B ) = ~P B -> ~P ( A u. B ) C_ ~P B )
9 7 8 syl 
 |-  ( ( A u. B ) = B -> ~P ( A u. B ) C_ ~P B )
10 6 9 sylbi 
 |-  ( A C_ B -> ~P ( A u. B ) C_ ~P B )
11 5 10 orim12i 
 |-  ( ( B C_ A \/ A C_ B ) -> ( ~P ( A u. B ) C_ ~P A \/ ~P ( A u. B ) C_ ~P B ) )
12 11 orcoms 
 |-  ( ( A C_ B \/ B C_ A ) -> ( ~P ( A u. B ) C_ ~P A \/ ~P ( A u. B ) C_ ~P B ) )
13 ssun 
 |-  ( ( ~P ( A u. B ) C_ ~P A \/ ~P ( A u. B ) C_ ~P B ) -> ~P ( A u. B ) C_ ( ~P A u. ~P B ) )
14 12 13 syl 
 |-  ( ( A C_ B \/ B C_ A ) -> ~P ( A u. B ) C_ ( ~P A u. ~P B ) )
15 vex 
 |-  x e. _V
16 15 snss 
 |-  ( x e. A <-> { x } C_ A )
17 vex 
 |-  y e. _V
18 17 snss 
 |-  ( y e. B <-> { y } C_ B )
19 unss12 
 |-  ( ( { x } C_ A /\ { y } C_ B ) -> ( { x } u. { y } ) C_ ( A u. B ) )
20 16 18 19 syl2anb 
 |-  ( ( x e. A /\ y e. B ) -> ( { x } u. { y } ) C_ ( A u. B ) )
21 zfpair2 
 |-  { x , y } e. _V
22 21 elpw 
 |-  ( { x , y } e. ~P ( A u. B ) <-> { x , y } C_ ( A u. B ) )
23 df-pr 
 |-  { x , y } = ( { x } u. { y } )
24 23 sseq1i 
 |-  ( { x , y } C_ ( A u. B ) <-> ( { x } u. { y } ) C_ ( A u. B ) )
25 22 24 bitr2i 
 |-  ( ( { x } u. { y } ) C_ ( A u. B ) <-> { x , y } e. ~P ( A u. B ) )
26 20 25 sylib 
 |-  ( ( x e. A /\ y e. B ) -> { x , y } e. ~P ( A u. B ) )
27 ssel 
 |-  ( ~P ( A u. B ) C_ ( ~P A u. ~P B ) -> ( { x , y } e. ~P ( A u. B ) -> { x , y } e. ( ~P A u. ~P B ) ) )
28 26 27 syl5 
 |-  ( ~P ( A u. B ) C_ ( ~P A u. ~P B ) -> ( ( x e. A /\ y e. B ) -> { x , y } e. ( ~P A u. ~P B ) ) )
29 28 expcomd 
 |-  ( ~P ( A u. B ) C_ ( ~P A u. ~P B ) -> ( y e. B -> ( x e. A -> { x , y } e. ( ~P A u. ~P B ) ) ) )
30 29 imp31 
 |-  ( ( ( ~P ( A u. B ) C_ ( ~P A u. ~P B ) /\ y e. B ) /\ x e. A ) -> { x , y } e. ( ~P A u. ~P B ) )
31 elun 
 |-  ( { x , y } e. ( ~P A u. ~P B ) <-> ( { x , y } e. ~P A \/ { x , y } e. ~P B ) )
32 30 31 sylib 
 |-  ( ( ( ~P ( A u. B ) C_ ( ~P A u. ~P B ) /\ y e. B ) /\ x e. A ) -> ( { x , y } e. ~P A \/ { x , y } e. ~P B ) )
33 21 elpw 
 |-  ( { x , y } e. ~P A <-> { x , y } C_ A )
34 15 17 prss 
 |-  ( ( x e. A /\ y e. A ) <-> { x , y } C_ A )
35 33 34 bitr4i 
 |-  ( { x , y } e. ~P A <-> ( x e. A /\ y e. A ) )
36 35 simprbi 
 |-  ( { x , y } e. ~P A -> y e. A )
37 21 elpw 
 |-  ( { x , y } e. ~P B <-> { x , y } C_ B )
38 15 17 prss 
 |-  ( ( x e. B /\ y e. B ) <-> { x , y } C_ B )
39 37 38 bitr4i 
 |-  ( { x , y } e. ~P B <-> ( x e. B /\ y e. B ) )
40 39 simplbi 
 |-  ( { x , y } e. ~P B -> x e. B )
41 36 40 orim12i 
 |-  ( ( { x , y } e. ~P A \/ { x , y } e. ~P B ) -> ( y e. A \/ x e. B ) )
42 32 41 syl 
 |-  ( ( ( ~P ( A u. B ) C_ ( ~P A u. ~P B ) /\ y e. B ) /\ x e. A ) -> ( y e. A \/ x e. B ) )
43 42 ord 
 |-  ( ( ( ~P ( A u. B ) C_ ( ~P A u. ~P B ) /\ y e. B ) /\ x e. A ) -> ( -. y e. A -> x e. B ) )
44 43 impancom 
 |-  ( ( ( ~P ( A u. B ) C_ ( ~P A u. ~P B ) /\ y e. B ) /\ -. y e. A ) -> ( x e. A -> x e. B ) )
45 44 ssrdv 
 |-  ( ( ( ~P ( A u. B ) C_ ( ~P A u. ~P B ) /\ y e. B ) /\ -. y e. A ) -> A C_ B )
46 45 exp31 
 |-  ( ~P ( A u. B ) C_ ( ~P A u. ~P B ) -> ( y e. B -> ( -. y e. A -> A C_ B ) ) )
47 con1b 
 |-  ( ( -. y e. A -> A C_ B ) <-> ( -. A C_ B -> y e. A ) )
48 46 47 syl6ib 
 |-  ( ~P ( A u. B ) C_ ( ~P A u. ~P B ) -> ( y e. B -> ( -. A C_ B -> y e. A ) ) )
49 48 com23 
 |-  ( ~P ( A u. B ) C_ ( ~P A u. ~P B ) -> ( -. A C_ B -> ( y e. B -> y e. A ) ) )
50 49 imp 
 |-  ( ( ~P ( A u. B ) C_ ( ~P A u. ~P B ) /\ -. A C_ B ) -> ( y e. B -> y e. A ) )
51 50 ssrdv 
 |-  ( ( ~P ( A u. B ) C_ ( ~P A u. ~P B ) /\ -. A C_ B ) -> B C_ A )
52 51 ex 
 |-  ( ~P ( A u. B ) C_ ( ~P A u. ~P B ) -> ( -. A C_ B -> B C_ A ) )
53 52 orrd 
 |-  ( ~P ( A u. B ) C_ ( ~P A u. ~P B ) -> ( A C_ B \/ B C_ A ) )
54 14 53 impbii 
 |-  ( ( A C_ B \/ B C_ A ) <-> ~P ( A u. B ) C_ ( ~P A u. ~P B ) )