Metamath Proof Explorer

Theorem infxpabs

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

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

Proof

Step Hyp Ref Expression
1 infxpdom 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~<_ A ) -> ( A X. B ) ~<_ A )
2 1 3expa 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ B ~<_ A ) -> ( A X. B ) ~<_ A )
3 2 adantrl 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B =/= (/) /\ B ~<_ A ) ) -> ( A X. B ) ~<_ A )
4 simpll 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B =/= (/) /\ B ~<_ A ) ) -> A e. dom card )
5 numdom 
 |-  ( ( A e. dom card /\ B ~<_ A ) -> B e. dom card )
6 5 ad2ant2rl 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B =/= (/) /\ B ~<_ A ) ) -> B e. dom card )
7 simprl 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B =/= (/) /\ B ~<_ A ) ) -> B =/= (/) )
8 xpdom3 
 |-  ( ( A e. dom card /\ B e. dom card /\ B =/= (/) ) -> A ~<_ ( A X. B ) )
9 4 6 7 8 syl3anc 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B =/= (/) /\ B ~<_ A ) ) -> A ~<_ ( A X. B ) )
10 sbth 
 |-  ( ( ( A X. B ) ~<_ A /\ A ~<_ ( A X. B ) ) -> ( A X. B ) ~~ A )
11 3 9 10 syl2anc 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B =/= (/) /\ B ~<_ A ) ) -> ( A X. B ) ~~ A )