Metamath Proof Explorer


Theorem undjudom

Description: Cardinal addition dominates union. (Contributed by NM, 28-Sep-2004) (Revised by Jim Kingdon, 15-Aug-2023)

Ref Expression
Assertion undjudom AVBWABA⊔︀B

Proof

Step Hyp Ref Expression
1 0ex V
2 xpsnen2g VAV×AA
3 1 2 mpan AV×AA
4 ensym ×AAA×A
5 endom A×AA×A
6 3 4 5 3syl AVA×A
7 1on 1𝑜On
8 xpsnen2g 1𝑜OnBW1𝑜×BB
9 7 8 mpan BW1𝑜×BB
10 ensym 1𝑜×BBB1𝑜×B
11 endom B1𝑜×BB1𝑜×B
12 9 10 11 3syl BWB1𝑜×B
13 xp01disjl ×A1𝑜×B=
14 undom A×AB1𝑜×B×A1𝑜×B=AB×A1𝑜×B
15 13 14 mpan2 A×AB1𝑜×BAB×A1𝑜×B
16 6 12 15 syl2an AVBWAB×A1𝑜×B
17 df-dju A⊔︀B=×A1𝑜×B
18 16 17 breqtrrdi AVBWABA⊔︀B