Metamath Proof Explorer

Theorem infunabs

Description: An infinite set is equinumerous to its union with a smaller one. (Contributed by NM, 28-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion infunabs 
|- ( ( A e. dom card /\ _om ~<_ A /\ B ~<_ A ) -> ( A u. B ) ~~ A )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~<_ A ) -> A e. dom card )
2 reldom 
 |-  Rel ~<_
3 2 brrelex1i 
 |-  ( B ~<_ A -> B e. _V )
4 3 3ad2ant3 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~<_ A ) -> B e. _V )
5 undjudom 
 |-  ( ( A e. dom card /\ B e. _V ) -> ( A u. B ) ~<_ ( A |_| B ) )
6 1 4 5 syl2anc 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~<_ A ) -> ( A u. B ) ~<_ ( A |_| B ) )
7 infdjuabs 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~<_ A ) -> ( A |_| B ) ~~ A )
8 domentr 
 |-  ( ( ( A u. B ) ~<_ ( A |_| B ) /\ ( A |_| B ) ~~ A ) -> ( A u. B ) ~<_ A )
9 6 7 8 syl2anc 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~<_ A ) -> ( A u. B ) ~<_ A )
10 unexg 
 |-  ( ( A e. dom card /\ B e. _V ) -> ( A u. B ) e. _V )
11 1 4 10 syl2anc 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~<_ A ) -> ( A u. B ) e. _V )
12 ssun1 
 |-  A C_ ( A u. B )
13 ssdomg 
 |-  ( ( A u. B ) e. _V -> ( A C_ ( A u. B ) -> A ~<_ ( A u. B ) ) )
14 11 12 13 mpisyl 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~<_ A ) -> A ~<_ ( A u. B ) )
15 sbth 
 |-  ( ( ( A u. B ) ~<_ A /\ A ~<_ ( A u. B ) ) -> ( A u. B ) ~~ A )
16 9 14 15 syl2anc 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~<_ A ) -> ( A u. B ) ~~ A )