Theorem undjudom

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

	Ref	Expression
Assertion	undjudom	|- ( ( A e. V /\ B e. W ) -> ( A u. B ) ~<_ ( A |_| B ) )

Proof

Step	Hyp	Ref	Expression
1		0ex	|- (/) e. _V
2		xpsnen2g	|- ( ( (/) e. _V /\ A e. V ) -> ( { (/) } X. A ) ~~ A )
3	1 2	mpan	|- ( A e. V -> ( { (/) } X. A ) ~~ A )
4		ensym	|- ( ( { (/) } X. A ) ~~ A -> A ~~ ( { (/) } X. A ) )
5		endom	|- ( A ~~ ( { (/) } X. A ) -> A ~<_ ( { (/) } X. A ) )
6	3 4 5	3syl	|- ( A e. V -> A ~<_ ( { (/) } X. A ) )
7		1on	|- 1o e. On
8		xpsnen2g	|- ( ( 1o e. On /\ B e. W ) -> ( { 1o } X. B ) ~~ B )
9	7 8	mpan	|- ( B e. W -> ( { 1o } X. B ) ~~ B )
10		ensym	|- ( ( { 1o } X. B ) ~~ B -> B ~~ ( { 1o } X. B ) )
11		endom	|- ( B ~~ ( { 1o } X. B ) -> B ~<_ ( { 1o } X. B ) )
12	9 10 11	3syl	|- ( B e. W -> B ~<_ ( { 1o } X. B ) )
13		xp01disjl	|- ( ( { (/) } X. A ) i^i ( { 1o } X. B ) ) = (/)
14		undom	|- ( ( ( A ~<_ ( { (/) } X. A ) /\ B ~<_ ( { 1o } X. B ) ) /\ ( ( { (/) } X. A ) i^i ( { 1o } X. B ) ) = (/) ) -> ( A u. B ) ~<_ ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) )
15	13 14	mpan2	|- ( ( A ~<_ ( { (/) } X. A ) /\ B ~<_ ( { 1o } X. B ) ) -> ( A u. B ) ~<_ ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) )
16	6 12 15	syl2an	|- ( ( A e. V /\ B e. W ) -> ( A u. B ) ~<_ ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) )
17		df-dju	|- ( A |_| B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
18	16 17	breqtrrdi	|- ( ( A e. V /\ B e. W ) -> ( A u. B ) ~<_ ( A |_| B ) )