Theorem infdjuabs

Description: Absorption law for addition to an infinite cardinal. (Contributed by NM, 30-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

	Ref	Expression
Assertion	infdjuabs	⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → ( 𝐴 ⊔ 𝐵 ) ≈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		simp3	⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → 𝐵 ≼ 𝐴 )
2		reldom	⊢ Rel ≼
3	2	brrelex2i	⊢ ( 𝐵 ≼ 𝐴 → 𝐴 ∈ V )
4		djudom2	⊢ ( ( 𝐵 ≼ 𝐴 ∧ 𝐴 ∈ V ) → ( 𝐴 ⊔ 𝐵 ) ≼ ( 𝐴 ⊔ 𝐴 ) )
5	1 3 4	syl2anc2	⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → ( 𝐴 ⊔ 𝐵 ) ≼ ( 𝐴 ⊔ 𝐴 ) )
6		xp2dju	⊢ ( 2o × 𝐴 ) = ( 𝐴 ⊔ 𝐴 )
7	5 6	breqtrrdi	⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → ( 𝐴 ⊔ 𝐵 ) ≼ ( 2o × 𝐴 ) )
8		simp1	⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → 𝐴 ∈ dom card )
9		2onn	⊢ 2o ∈ ω
10		nnsdom	⊢ ( 2o ∈ ω → 2o ≺ ω )
11		sdomdom	⊢ ( 2o ≺ ω → 2o ≼ ω )
12	9 10 11	mp2b	⊢ 2o ≼ ω
13		simp2	⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → ω ≼ 𝐴 )
14		domtr	⊢ ( ( 2o ≼ ω ∧ ω ≼ 𝐴 ) → 2o ≼ 𝐴 )
15	12 13 14	sylancr	⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → 2o ≼ 𝐴 )
16		xpdom1g	⊢ ( ( 𝐴 ∈ dom card ∧ 2o ≼ 𝐴 ) → ( 2o × 𝐴 ) ≼ ( 𝐴 × 𝐴 ) )
17	8 15 16	syl2anc	⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → ( 2o × 𝐴 ) ≼ ( 𝐴 × 𝐴 ) )
18		domtr	⊢ ( ( ( 𝐴 ⊔ 𝐵 ) ≼ ( 2o × 𝐴 ) ∧ ( 2o × 𝐴 ) ≼ ( 𝐴 × 𝐴 ) ) → ( 𝐴 ⊔ 𝐵 ) ≼ ( 𝐴 × 𝐴 ) )
19	7 17 18	syl2anc	⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → ( 𝐴 ⊔ 𝐵 ) ≼ ( 𝐴 × 𝐴 ) )
20		infxpidm2	⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝐴 × 𝐴 ) ≈ 𝐴 )
21	20	3adant3	⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → ( 𝐴 × 𝐴 ) ≈ 𝐴 )
22		domentr	⊢ ( ( ( 𝐴 ⊔ 𝐵 ) ≼ ( 𝐴 × 𝐴 ) ∧ ( 𝐴 × 𝐴 ) ≈ 𝐴 ) → ( 𝐴 ⊔ 𝐵 ) ≼ 𝐴 )
23	19 21 22	syl2anc	⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → ( 𝐴 ⊔ 𝐵 ) ≼ 𝐴 )
24	2	brrelex1i	⊢ ( 𝐵 ≼ 𝐴 → 𝐵 ∈ V )
25	24	3ad2ant3	⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → 𝐵 ∈ V )
26		djudoml	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ V ) → 𝐴 ≼ ( 𝐴 ⊔ 𝐵 ) )
27	8 25 26	syl2anc	⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → 𝐴 ≼ ( 𝐴 ⊔ 𝐵 ) )
28		sbth	⊢ ( ( ( 𝐴 ⊔ 𝐵 ) ≼ 𝐴 ∧ 𝐴 ≼ ( 𝐴 ⊔ 𝐵 ) ) → ( 𝐴 ⊔ 𝐵 ) ≈ 𝐴 )
29	23 27 28	syl2anc	⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → ( 𝐴 ⊔ 𝐵 ) ≈ 𝐴 )