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