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

Metamath Proof Explorer

Theorem infdju

Description: The sum of two cardinal numbers is their maximum, if one of them is infinite. Proposition 10.41 of TakeutiZaring p. 95. (Contributed by NM, 28-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 unnum 
 |-  ( ( A e. dom card /\ B e. dom card ) -> ( A u. B ) e. dom card )
2 1 3adant3 
 |-  ( ( A e. dom card /\ B e. dom card /\ _om ~<_ A ) -> ( A u. B ) e. dom card )
3 ssun2 
 |-  B C_ ( A u. B )
4 ssdomg 
 |-  ( ( A u. B ) e. dom card -> ( B C_ ( A u. B ) -> B ~<_ ( A u. B ) ) )
5 2 3 4 mpisyl 
 |-  ( ( A e. dom card /\ B e. dom card /\ _om ~<_ A ) -> B ~<_ ( A u. B ) )
6 simp1 
 |-  ( ( A e. dom card /\ B e. dom card /\ _om ~<_ A ) -> A e. dom card )
7 djudom2 
 |-  ( ( B ~<_ ( A u. B ) /\ A e. dom card ) -> ( A |_| B ) ~<_ ( A |_| ( A u. B ) ) )
8 5 6 7 syl2anc 
 |-  ( ( A e. dom card /\ B e. dom card /\ _om ~<_ A ) -> ( A |_| B ) ~<_ ( A |_| ( A u. B ) ) )
9 djucomen 
 |-  ( ( A e. dom card /\ ( A u. B ) e. dom card ) -> ( A |_| ( A u. B ) ) ~~ ( ( A u. B ) |_| A ) )
10 6 2 9 syl2anc 
 |-  ( ( A e. dom card /\ B e. dom card /\ _om ~<_ A ) -> ( A |_| ( A u. B ) ) ~~ ( ( A u. B ) |_| A ) )
11 domentr 
 |-  ( ( ( A |_| B ) ~<_ ( A |_| ( A u. B ) ) /\ ( A |_| ( A u. B ) ) ~~ ( ( A u. B ) |_| A ) ) -> ( A |_| B ) ~<_ ( ( A u. B ) |_| A ) )
12 8 10 11 syl2anc 
 |-  ( ( A e. dom card /\ B e. dom card /\ _om ~<_ A ) -> ( A |_| B ) ~<_ ( ( A u. B ) |_| A ) )
13 simp3 
 |-  ( ( A e. dom card /\ B e. dom card /\ _om ~<_ A ) -> _om ~<_ A )
14 ssun1 
 |-  A C_ ( A u. B )
15 ssdomg 
 |-  ( ( A u. B ) e. dom card -> ( A C_ ( A u. B ) -> A ~<_ ( A u. B ) ) )
16 2 14 15 mpisyl 
 |-  ( ( A e. dom card /\ B e. dom card /\ _om ~<_ A ) -> A ~<_ ( A u. B ) )
17 domtr 
 |-  ( ( _om ~<_ A /\ A ~<_ ( A u. B ) ) -> _om ~<_ ( A u. B ) )
18 13 16 17 syl2anc 
 |-  ( ( A e. dom card /\ B e. dom card /\ _om ~<_ A ) -> _om ~<_ ( A u. B ) )
19 infdjuabs 
 |-  ( ( ( A u. B ) e. dom card /\ _om ~<_ ( A u. B ) /\ A ~<_ ( A u. B ) ) -> ( ( A u. B ) |_| A ) ~~ ( A u. B ) )
20 2 18 16 19 syl3anc 
 |-  ( ( A e. dom card /\ B e. dom card /\ _om ~<_ A ) -> ( ( A u. B ) |_| A ) ~~ ( A u. B ) )
21 domentr 
 |-  ( ( ( A |_| B ) ~<_ ( ( A u. B ) |_| A ) /\ ( ( A u. B ) |_| A ) ~~ ( A u. B ) ) -> ( A |_| B ) ~<_ ( A u. B ) )
22 12 20 21 syl2anc 
 |-  ( ( A e. dom card /\ B e. dom card /\ _om ~<_ A ) -> ( A |_| B ) ~<_ ( A u. B ) )
23 undjudom 
 |-  ( ( A e. dom card /\ B e. dom card ) -> ( A u. B ) ~<_ ( A |_| B ) )
24 23 3adant3 
 |-  ( ( A e. dom card /\ B e. dom card /\ _om ~<_ A ) -> ( A u. B ) ~<_ ( A |_| B ) )
25 sbth 
 |-  ( ( ( A |_| B ) ~<_ ( A u. B ) /\ ( A u. B ) ~<_ ( A |_| B ) ) -> ( A |_| B ) ~~ ( A u. B ) )
26 22 24 25 syl2anc 
 |-  ( ( A e. dom card /\ B e. dom card /\ _om ~<_ A ) -> ( A |_| B ) ~~ ( A u. B ) )