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 AdomcardωABAA⊔︀BA

Proof

Step Hyp Ref Expression
1 simp3 AdomcardωABABA
2 reldom Rel
3 2 brrelex2i BAAV
4 djudom2 BAAVA⊔︀BA⊔︀A
5 1 3 4 syl2anc2 AdomcardωABAA⊔︀BA⊔︀A
6 xp2dju 2𝑜×A=A⊔︀A
7 5 6 breqtrrdi AdomcardωABAA⊔︀B2𝑜×A
8 simp1 AdomcardωABAAdomcard
9 2onn 2𝑜ω
10 nnsdom 2𝑜ω2𝑜ω
11 sdomdom 2𝑜ω2𝑜ω
12 9 10 11 mp2b 2𝑜ω
13 simp2 AdomcardωABAωA
14 domtr 2𝑜ωωA2𝑜A
15 12 13 14 sylancr AdomcardωABA2𝑜A
16 xpdom1g Adomcard2𝑜A2𝑜×AA×A
17 8 15 16 syl2anc AdomcardωABA2𝑜×AA×A
18 domtr A⊔︀B2𝑜×A2𝑜×AA×AA⊔︀BA×A
19 7 17 18 syl2anc AdomcardωABAA⊔︀BA×A
20 infxpidm2 AdomcardωAA×AA
21 20 3adant3 AdomcardωABAA×AA
22 domentr A⊔︀BA×AA×AAA⊔︀BA
23 19 21 22 syl2anc AdomcardωABAA⊔︀BA
24 2 brrelex1i BABV
25 24 3ad2ant3 AdomcardωABABV
26 djudoml AdomcardBVAA⊔︀B
27 8 25 26 syl2anc AdomcardωABAAA⊔︀B
28 sbth A⊔︀BAAA⊔︀BA⊔︀BA
29 23 27 28 syl2anc AdomcardωABAA⊔︀BA