Metamath Proof Explorer

Theorem pwdju1

Description: The sum of a powerset with itself is equipotent to the successor powerset. (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion pwdju1 
|- ( A e. V -> ( ~P A |_| ~P A ) ~~ ~P ( A |_| 1o ) )

Proof

Step Hyp Ref Expression
1 1on 
 |-  1o e. On
2 pwdjuen 
 |-  ( ( A e. V /\ 1o e. On ) -> ~P ( A |_| 1o ) ~~ ( ~P A X. ~P 1o ) )
3 1 2 mpan2 
 |-  ( A e. V -> ~P ( A |_| 1o ) ~~ ( ~P A X. ~P 1o ) )
4 pwexg 
 |-  ( A e. V -> ~P A e. _V )
5 1oex 
 |-  1o e. _V
6 5 pwex 
 |-  ~P 1o e. _V
7 xpcomeng 
 |-  ( ( ~P A e. _V /\ ~P 1o e. _V ) -> ( ~P A X. ~P 1o ) ~~ ( ~P 1o X. ~P A ) )
8 4 6 7 sylancl 
 |-  ( A e. V -> ( ~P A X. ~P 1o ) ~~ ( ~P 1o X. ~P A ) )
9 entr 
 |-  ( ( ~P ( A |_| 1o ) ~~ ( ~P A X. ~P 1o ) /\ ( ~P A X. ~P 1o ) ~~ ( ~P 1o X. ~P A ) ) -> ~P ( A |_| 1o ) ~~ ( ~P 1o X. ~P A ) )
10 3 8 9 syl2anc 
 |-  ( A e. V -> ~P ( A |_| 1o ) ~~ ( ~P 1o X. ~P A ) )
11 pwpw0 
 |-  ~P { (/) } = { (/) , { (/) } }
12 df1o2 
 |-  1o = { (/) }
13 12 pweqi 
 |-  ~P 1o = ~P { (/) }
14 df2o2 
 |-  2o = { (/) , { (/) } }
15 11 13 14 3eqtr4i 
 |-  ~P 1o = 2o
16 15 xpeq1i 
 |-  ( ~P 1o X. ~P A ) = ( 2o X. ~P A )
17 xp2dju 
 |-  ( 2o X. ~P A ) = ( ~P A |_| ~P A )
18 16 17 eqtri 
 |-  ( ~P 1o X. ~P A ) = ( ~P A |_| ~P A )
19 10 18 breqtrdi 
 |-  ( A e. V -> ~P ( A |_| 1o ) ~~ ( ~P A |_| ~P A ) )
20 19 ensymd 
 |-  ( A e. V -> ( ~P A |_| ~P A ) ~~ ~P ( A |_| 1o ) )