Metamath Proof Explorer

Theorem pwdjuidm

Description: If the natural numbers inject into A , then ~P A is idempotent under cardinal sum. (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion pwdjuidm 
|- ( _om ~<_ A -> ( ~P A |_| ~P A ) ~~ ~P A )

Proof

Step Hyp Ref Expression
1 reldom 
 |-  Rel ~<_
2 1 brrelex2i 
 |-  ( _om ~<_ A -> A e. _V )
3 pwdju1 
 |-  ( A e. _V -> ( ~P A |_| ~P A ) ~~ ~P ( A |_| 1o ) )
4 2 3 syl 
 |-  ( _om ~<_ A -> ( ~P A |_| ~P A ) ~~ ~P ( A |_| 1o ) )
5 infdju1 
 |-  ( _om ~<_ A -> ( A |_| 1o ) ~~ A )
6 pwen 
 |-  ( ( A |_| 1o ) ~~ A -> ~P ( A |_| 1o ) ~~ ~P A )
7 5 6 syl 
 |-  ( _om ~<_ A -> ~P ( A |_| 1o ) ~~ ~P A )
8 entr 
 |-  ( ( ( ~P A |_| ~P A ) ~~ ~P ( A |_| 1o ) /\ ~P ( A |_| 1o ) ~~ ~P A ) -> ( ~P A |_| ~P A ) ~~ ~P A )
9 4 7 8 syl2anc 
 |-  ( _om ~<_ A -> ( ~P A |_| ~P A ) ~~ ~P A )