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