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