Metamath Proof Explorer

Theorem infxpidm2

Description: Every infinite well-orderable set is equinumerous to its Cartesian square. This theorem provides the basis for infinite cardinal arithmetic. Proposition 10.40 of TakeutiZaring p. 95. See also infxpidm . (Contributed by Mario Carneiro, 9-Mar-2013) (Revised by Mario Carneiro, 29-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 cardid2 
 |-  ( A e. dom card -> ( card ` A ) ~~ A )
2 1 ensymd 
 |-  ( A e. dom card -> A ~~ ( card ` A ) )
3 xpen 
 |-  ( ( A ~~ ( card ` A ) /\ A ~~ ( card ` A ) ) -> ( A X. A ) ~~ ( ( card ` A ) X. ( card ` A ) ) )
4 2 2 3 syl2anc 
 |-  ( A e. dom card -> ( A X. A ) ~~ ( ( card ` A ) X. ( card ` A ) ) )
5 4 adantr 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( A X. A ) ~~ ( ( card ` A ) X. ( card ` A ) ) )
6 cardon 
 |-  ( card ` A ) e. On
7 cardom 
 |-  ( card ` _om ) = _om
8 omelon 
 |-  _om e. On
9 onenon 
 |-  ( _om e. On -> _om e. dom card )
10 8 9 ax-mp 
 |-  _om e. dom card
11 carddom2 
 |-  ( ( _om e. dom card /\ A e. dom card ) -> ( ( card ` _om ) C_ ( card ` A ) <-> _om ~<_ A ) )
12 10 11 mpan 
 |-  ( A e. dom card -> ( ( card ` _om ) C_ ( card ` A ) <-> _om ~<_ A ) )
13 12 biimpar 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( card ` _om ) C_ ( card ` A ) )
14 7 13 eqsstrrid 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> _om C_ ( card ` A ) )
15 infxpen 
 |-  ( ( ( card ` A ) e. On /\ _om C_ ( card ` A ) ) -> ( ( card ` A ) X. ( card ` A ) ) ~~ ( card ` A ) )
16 6 14 15 sylancr 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( ( card ` A ) X. ( card ` A ) ) ~~ ( card ` A ) )
17 entr 
 |-  ( ( ( A X. A ) ~~ ( ( card ` A ) X. ( card ` A ) ) /\ ( ( card ` A ) X. ( card ` A ) ) ~~ ( card ` A ) ) -> ( A X. A ) ~~ ( card ` A ) )
18 5 16 17 syl2anc 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( A X. A ) ~~ ( card ` A ) )
19 1 adantr 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( card ` A ) ~~ A )
20 entr 
 |-  ( ( ( A X. A ) ~~ ( card ` A ) /\ ( card ` A ) ~~ A ) -> ( A X. A ) ~~ A )
21 18 19 20 syl2anc 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( A X. A ) ~~ A )