Metamath Proof Explorer

Theorem djudoml

Description: A set is dominated by its disjoint union with another. (Contributed by NM, 28-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 unexg 
 |-  ( ( A e. V /\ B e. W ) -> ( A u. B ) e. _V )
2 ssun1 
 |-  A C_ ( A u. B )
3 ssdomg 
 |-  ( ( A u. B ) e. _V -> ( A C_ ( A u. B ) -> A ~<_ ( A u. B ) ) )
4 1 2 3 mpisyl 
 |-  ( ( A e. V /\ B e. W ) -> A ~<_ ( A u. B ) )
5 undjudom 
 |-  ( ( A e. V /\ B e. W ) -> ( A u. B ) ~<_ ( A |_| B ) )
6 domtr 
 |-  ( ( A ~<_ ( A u. B ) /\ ( A u. B ) ~<_ ( A |_| B ) ) -> A ~<_ ( A |_| B ) )
7 4 5 6 syl2anc 
 |-  ( ( A e. V /\ B e. W ) -> A ~<_ ( A |_| B ) )