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

Metamath Proof Explorer

Theorem infdjuabs

Description: Absorption law for addition to an infinite cardinal. (Contributed by NM, 30-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 simp3 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~<_ A ) -> B ~<_ A )
2 reldom 
 |-  Rel ~<_
3 2 brrelex2i 
 |-  ( B ~<_ A -> A e. _V )
4 djudom2 
 |-  ( ( B ~<_ A /\ A e. _V ) -> ( A |_| B ) ~<_ ( A |_| A ) )
5 1 3 4 syl2anc2 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~<_ A ) -> ( A |_| B ) ~<_ ( A |_| A ) )
6 xp2dju 
 |-  ( 2o X. A ) = ( A |_| A )
7 5 6 breqtrrdi 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~<_ A ) -> ( A |_| B ) ~<_ ( 2o X. A ) )
8 simp1 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~<_ A ) -> A e. dom card )
9 2onn 
 |-  2o e. _om
10 nnsdom 
 |-  ( 2o e. _om -> 2o ~< _om )
11 sdomdom 
 |-  ( 2o ~< _om -> 2o ~<_ _om )
12 9 10 11 mp2b 
 |-  2o ~<_ _om
13 simp2 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~<_ A ) -> _om ~<_ A )
14 domtr 
 |-  ( ( 2o ~<_ _om /\ _om ~<_ A ) -> 2o ~<_ A )
15 12 13 14 sylancr 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~<_ A ) -> 2o ~<_ A )
16 xpdom1g 
 |-  ( ( A e. dom card /\ 2o ~<_ A ) -> ( 2o X. A ) ~<_ ( A X. A ) )
17 8 15 16 syl2anc 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~<_ A ) -> ( 2o X. A ) ~<_ ( A X. A ) )
18 domtr 
 |-  ( ( ( A |_| B ) ~<_ ( 2o X. A ) /\ ( 2o X. A ) ~<_ ( A X. A ) ) -> ( A |_| B ) ~<_ ( A X. A ) )
19 7 17 18 syl2anc 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~<_ A ) -> ( A |_| B ) ~<_ ( A X. A ) )
20 infxpidm2 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( A X. A ) ~~ A )
21 20 3adant3 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~<_ A ) -> ( A X. A ) ~~ A )
22 domentr 
 |-  ( ( ( A |_| B ) ~<_ ( A X. A ) /\ ( A X. A ) ~~ A ) -> ( A |_| B ) ~<_ A )
23 19 21 22 syl2anc 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~<_ A ) -> ( A |_| B ) ~<_ A )
24 2 brrelex1i 
 |-  ( B ~<_ A -> B e. _V )
25 24 3ad2ant3 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~<_ A ) -> B e. _V )
26 djudoml 
 |-  ( ( A e. dom card /\ B e. _V ) -> A ~<_ ( A |_| B ) )
27 8 25 26 syl2anc 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~<_ A ) -> A ~<_ ( A |_| B ) )
28 sbth 
 |-  ( ( ( A |_| B ) ~<_ A /\ A ~<_ ( A |_| B ) ) -> ( A |_| B ) ~~ A )
29 23 27 28 syl2anc 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~<_ A ) -> ( A |_| B ) ~~ A )