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≼𝒫A→A⊔︀B≼𝒫A

Proof

Step Hyp Ref Expression
1 djueq1 ⊢A=∅→A⊔︀B=∅⊔︀B
2 1 breq1d ⊢A=∅→A⊔︀B≼𝒫A↔∅⊔︀B≼𝒫A
3 relen ⊢Rel⁡≈
4 3 brrelex2i ⊢A⊔︀A≈A→A∈V
5 4 adantr ⊢A⊔︀A≈A∧B≼𝒫A→A∈V
6 canth2g ⊢A∈V→A≺𝒫A
7 sdomdom ⊢A≺𝒫A→A≼𝒫A
8 5 6 7 3syl ⊢A⊔︀A≈A∧B≼𝒫A→A≼𝒫A
9 simpr ⊢A⊔︀A≈A∧B≼𝒫A→B≼𝒫A
10 reldom ⊢Rel⁡≼
11 10 brrelex1i ⊢B≼𝒫A→B∈V
12 djudom1 ⊢A≼𝒫A∧B∈V→A⊔︀B≼𝒫A⊔︀B
13 11 12 sylan2 ⊢A≼𝒫A∧B≼𝒫A→A⊔︀B≼𝒫A⊔︀B
14 simpr ⊢A≼𝒫A∧B≼𝒫A→B≼𝒫A
15 10 brrelex2i ⊢B≼𝒫A→𝒫A∈V
16 djudom2 ⊢B≼𝒫A∧𝒫A∈V→𝒫A⊔︀B≼𝒫A⊔︀𝒫A
17 14 15 16 syl2anc2 ⊢A≼𝒫A∧B≼𝒫A→𝒫A⊔︀B≼𝒫A⊔︀𝒫A
18 domtr ⊢A⊔︀B≼𝒫A⊔︀B∧𝒫A⊔︀B≼𝒫A⊔︀𝒫A→A⊔︀B≼𝒫A⊔︀𝒫A
19 13 17 18 syl2anc ⊢A≼𝒫A∧B≼𝒫A→A⊔︀B≼𝒫A⊔︀𝒫A
20 8 9 19 syl2anc ⊢A⊔︀A≈A∧B≼𝒫A→A⊔︀B≼𝒫A⊔︀𝒫A
21 pwdju1 ⊢A∈V→𝒫A⊔︀𝒫A≈𝒫A⊔︀1𝑜
22 5 21 syl ⊢A⊔︀A≈A∧B≼𝒫A→𝒫A⊔︀𝒫A≈𝒫A⊔︀1𝑜
23 domentr ⊢A⊔︀B≼𝒫A⊔︀𝒫A∧𝒫A⊔︀𝒫A≈𝒫A⊔︀1𝑜→A⊔︀B≼𝒫A⊔︀1𝑜
24 20 22 23 syl2anc ⊢A⊔︀A≈A∧B≼𝒫A→A⊔︀B≼𝒫A⊔︀1𝑜
25 24 adantr ⊢A⊔︀A≈A∧B≼𝒫A∧A≠∅→A⊔︀B≼𝒫A⊔︀1𝑜
26 0sdomg ⊢A∈V→∅≺A↔A≠∅
27 5 26 syl ⊢A⊔︀A≈A∧B≼𝒫A→∅≺A↔A≠∅
28 27 biimpar ⊢A⊔︀A≈A∧B≼𝒫A∧A≠∅→∅≺A
29 0sdom1dom ⊢∅≺A↔1𝑜≼A
30 28 29 sylib ⊢A⊔︀A≈A∧B≼𝒫A∧A≠∅→1𝑜≼A
31 5 adantr ⊢A⊔︀A≈A∧B≼𝒫A∧A≠∅→A∈V
32 djudom2 ⊢1𝑜≼A∧A∈V→A⊔︀1𝑜≼A⊔︀A
33 30 31 32 syl2anc ⊢A⊔︀A≈A∧B≼𝒫A∧A≠∅→A⊔︀1𝑜≼A⊔︀A
34 simpll ⊢A⊔︀A≈A∧B≼𝒫A∧A≠∅→A⊔︀A≈A
35 domentr ⊢A⊔︀1𝑜≼A⊔︀A∧A⊔︀A≈A→A⊔︀1𝑜≼A
36 33 34 35 syl2anc ⊢A⊔︀A≈A∧B≼𝒫A∧A≠∅→A⊔︀1𝑜≼A
37 pwdom ⊢A⊔︀1𝑜≼A→𝒫A⊔︀1𝑜≼𝒫A
38 36 37 syl ⊢A⊔︀A≈A∧B≼𝒫A∧A≠∅→𝒫A⊔︀1𝑜≼𝒫A
39 domtr ⊢A⊔︀B≼𝒫A⊔︀1𝑜∧𝒫A⊔︀1𝑜≼𝒫A→A⊔︀B≼𝒫A
40 25 38 39 syl2anc ⊢A⊔︀A≈A∧B≼𝒫A∧A≠∅→A⊔︀B≼𝒫A
41 0ex ⊢∅∈V
42 11 adantl ⊢A⊔︀A≈A∧B≼𝒫A→B∈V
43 djucomen ⊢∅∈V∧B∈V→∅⊔︀B≈B⊔︀∅
44 41 42 43 sylancr ⊢A⊔︀A≈A∧B≼𝒫A→∅⊔︀B≈B⊔︀∅
45 dju0en ⊢B∈V→B⊔︀∅≈B
46 domen1 ⊢B⊔︀∅≈B→B⊔︀∅≼𝒫A↔B≼𝒫A
47 42 45 46 3syl ⊢A⊔︀A≈A∧B≼𝒫A→B⊔︀∅≼𝒫A↔B≼𝒫A
48 9 47 mpbird ⊢A⊔︀A≈A∧B≼𝒫A→B⊔︀∅≼𝒫A
49 endomtr ⊢∅⊔︀B≈B⊔︀∅∧B⊔︀∅≼𝒫A→∅⊔︀B≼𝒫A
50 44 48 49 syl2anc ⊢A⊔︀A≈A∧B≼𝒫A→∅⊔︀B≼𝒫A
51 2 40 50 pm2.61ne ⊢A⊔︀A≈A∧B≼𝒫A→A⊔︀B≼𝒫A