Metamath Proof Explorer

Theorem djulepw

Description: If A is idempotent under cardinal sum and B is dominated by the power set of A , then so is the cardinal sum of A and B . (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion djulepw 
|- ( ( ( A |_| A ) ~~ A /\ B ~<_ ~P A ) -> ( A |_| B ) ~<_ ~P A )

Proof

Step Hyp Ref Expression
1 djueq1 
 |-  ( A = (/) -> ( A |_| B ) = ( (/) |_| B ) )
2 1 breq1d 
 |-  ( A = (/) -> ( ( A |_| B ) ~<_ ~P A <-> ( (/) |_| B ) ~<_ ~P A ) )
3 relen 
 |-  Rel ~~
4 3 brrelex2i 
 |-  ( ( A |_| A ) ~~ A -> A e. _V )
5 4 adantr 
 |-  ( ( ( A |_| A ) ~~ A /\ B ~<_ ~P A ) -> A e. _V )
6 canth2g 
 |-  ( A e. _V -> A ~< ~P A )
7 sdomdom 
 |-  ( A ~< ~P A -> A ~<_ ~P A )
8 5 6 7 3syl 
 |-  ( ( ( A |_| A ) ~~ A /\ B ~<_ ~P A ) -> A ~<_ ~P A )
9 simpr 
 |-  ( ( ( A |_| A ) ~~ A /\ B ~<_ ~P A ) -> B ~<_ ~P A )
10 reldom 
 |-  Rel ~<_
11 10 brrelex1i 
 |-  ( B ~<_ ~P A -> B e. _V )
12 djudom1 
 |-  ( ( A ~<_ ~P A /\ B e. _V ) -> ( A |_| B ) ~<_ ( ~P A |_| B ) )
13 11 12 sylan2 
 |-  ( ( A ~<_ ~P A /\ B ~<_ ~P A ) -> ( A |_| B ) ~<_ ( ~P A |_| B ) )
14 simpr 
 |-  ( ( A ~<_ ~P A /\ B ~<_ ~P A ) -> B ~<_ ~P A )
15 10 brrelex2i 
 |-  ( B ~<_ ~P A -> ~P A e. _V )
16 djudom2 
 |-  ( ( B ~<_ ~P A /\ ~P A e. _V ) -> ( ~P A |_| B ) ~<_ ( ~P A |_| ~P A ) )
17 14 15 16 syl2anc2 
 |-  ( ( A ~<_ ~P A /\ B ~<_ ~P A ) -> ( ~P A |_| B ) ~<_ ( ~P A |_| ~P A ) )
18 domtr 
 |-  ( ( ( A |_| B ) ~<_ ( ~P A |_| B ) /\ ( ~P A |_| B ) ~<_ ( ~P A |_| ~P A ) ) -> ( A |_| B ) ~<_ ( ~P A |_| ~P A ) )
19 13 17 18 syl2anc 
 |-  ( ( A ~<_ ~P A /\ B ~<_ ~P A ) -> ( A |_| B ) ~<_ ( ~P A |_| ~P A ) )
20 8 9 19 syl2anc 
 |-  ( ( ( A |_| A ) ~~ A /\ B ~<_ ~P A ) -> ( A |_| B ) ~<_ ( ~P A |_| ~P A ) )
21 pwdju1 
 |-  ( A e. _V -> ( ~P A |_| ~P A ) ~~ ~P ( A |_| 1o ) )
22 5 21 syl 
 |-  ( ( ( A |_| A ) ~~ A /\ B ~<_ ~P A ) -> ( ~P A |_| ~P A ) ~~ ~P ( A |_| 1o ) )
23 domentr 
 |-  ( ( ( A |_| B ) ~<_ ( ~P A |_| ~P A ) /\ ( ~P A |_| ~P A ) ~~ ~P ( A |_| 1o ) ) -> ( A |_| B ) ~<_ ~P ( A |_| 1o ) )
24 20 22 23 syl2anc 
 |-  ( ( ( A |_| A ) ~~ A /\ B ~<_ ~P A ) -> ( A |_| B ) ~<_ ~P ( A |_| 1o ) )
25 24 adantr 
 |-  ( ( ( ( A |_| A ) ~~ A /\ B ~<_ ~P A ) /\ A =/= (/) ) -> ( A |_| B ) ~<_ ~P ( A |_| 1o ) )
26 0sdomg 
 |-  ( A e. _V -> ( (/) ~< A <-> A =/= (/) ) )
27 5 26 syl 
 |-  ( ( ( A |_| A ) ~~ A /\ B ~<_ ~P A ) -> ( (/) ~< A <-> A =/= (/) ) )
28 27 biimpar 
 |-  ( ( ( ( A |_| A ) ~~ A /\ B ~<_ ~P A ) /\ A =/= (/) ) -> (/) ~< A )
29 0sdom1dom 
 |-  ( (/) ~< A <-> 1o ~<_ A )
30 28 29 sylib 
 |-  ( ( ( ( A |_| A ) ~~ A /\ B ~<_ ~P A ) /\ A =/= (/) ) -> 1o ~<_ A )
31 5 adantr 
 |-  ( ( ( ( A |_| A ) ~~ A /\ B ~<_ ~P A ) /\ A =/= (/) ) -> A e. _V )
32 djudom2 
 |-  ( ( 1o ~<_ A /\ A e. _V ) -> ( A |_| 1o ) ~<_ ( A |_| A ) )
33 30 31 32 syl2anc 
 |-  ( ( ( ( A |_| A ) ~~ A /\ B ~<_ ~P A ) /\ A =/= (/) ) -> ( A |_| 1o ) ~<_ ( A |_| A ) )
34 simpll 
 |-  ( ( ( ( A |_| A ) ~~ A /\ B ~<_ ~P A ) /\ A =/= (/) ) -> ( A |_| A ) ~~ A )
35 domentr 
 |-  ( ( ( A |_| 1o ) ~<_ ( A |_| A ) /\ ( A |_| A ) ~~ A ) -> ( A |_| 1o ) ~<_ A )
36 33 34 35 syl2anc 
 |-  ( ( ( ( A |_| A ) ~~ A /\ B ~<_ ~P A ) /\ A =/= (/) ) -> ( A |_| 1o ) ~<_ A )
37 pwdom 
 |-  ( ( A |_| 1o ) ~<_ A -> ~P ( A |_| 1o ) ~<_ ~P A )
38 36 37 syl 
 |-  ( ( ( ( A |_| A ) ~~ A /\ B ~<_ ~P A ) /\ A =/= (/) ) -> ~P ( A |_| 1o ) ~<_ ~P A )
39 domtr 
 |-  ( ( ( A |_| B ) ~<_ ~P ( A |_| 1o ) /\ ~P ( A |_| 1o ) ~<_ ~P A ) -> ( A |_| B ) ~<_ ~P A )
40 25 38 39 syl2anc 
 |-  ( ( ( ( A |_| A ) ~~ A /\ B ~<_ ~P A ) /\ A =/= (/) ) -> ( A |_| B ) ~<_ ~P A )
41 0ex 
 |-  (/) e. _V
42 11 adantl 
 |-  ( ( ( A |_| A ) ~~ A /\ B ~<_ ~P A ) -> B e. _V )
43 djucomen 
 |-  ( ( (/) e. _V /\ B e. _V ) -> ( (/) |_| B ) ~~ ( B |_| (/) ) )
44 41 42 43 sylancr 
 |-  ( ( ( A |_| A ) ~~ A /\ B ~<_ ~P A ) -> ( (/) |_| B ) ~~ ( B |_| (/) ) )
45 dju0en 
 |-  ( B e. _V -> ( B |_| (/) ) ~~ B )
46 domen1 
 |-  ( ( B |_| (/) ) ~~ B -> ( ( B |_| (/) ) ~<_ ~P A <-> B ~<_ ~P A ) )
47 42 45 46 3syl 
 |-  ( ( ( A |_| A ) ~~ A /\ B ~<_ ~P A ) -> ( ( B |_| (/) ) ~<_ ~P A <-> B ~<_ ~P A ) )
48 9 47 mpbird 
 |-  ( ( ( A |_| A ) ~~ A /\ B ~<_ ~P A ) -> ( B |_| (/) ) ~<_ ~P A )
49 endomtr 
 |-  ( ( ( (/) |_| B ) ~~ ( B |_| (/) ) /\ ( B |_| (/) ) ~<_ ~P A ) -> ( (/) |_| B ) ~<_ ~P A )
50 44 48 49 syl2anc 
 |-  ( ( ( A |_| A ) ~~ A /\ B ~<_ ~P A ) -> ( (/) |_| B ) ~<_ ~P A )
51 2 40 50 pm2.61ne 
 |-  ( ( ( A |_| A ) ~~ A /\ B ~<_ ~P A ) -> ( A |_| B ) ~<_ ~P A )