This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ( 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 ) )