Metamath Proof Explorer

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 ⊢ A ∈ dom ⁡ card ∧ ω ≼ A ∧ B ≼ A → A ⊔︀ B ≈ A

Proof

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