This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴 ) → ( 𝐴 ⊔ 𝐵 ) ≼ 𝒫 𝐴 )

Proof

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