Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  infxpidm2 Unicode version

Theorem infxpidm2 7528
 Description: The cross product of an infinite set with itself is idempotent. This theorem provides the basis for infinite cardinal arithmetic. Proposition 10.40 of [TakeutiZaring] p. 95. See also infxpidm 8066. (Contributed by Mario Carneiro, 9-Mar-2013.) (Revised by Mario Carneiro, 29-Apr-2015.)
Assertion
Ref Expression
infxpidm2

Proof of Theorem infxpidm2
StepHypRef Expression
1 cardid2 7470 . . . . . 6
2 ensym 6796 . . . . . 6
31, 2syl 17 . . . . 5
4 xpen 6909 . . . . 5
53, 3, 4syl2anc 645 . . . 4
7 cardon 7461 . . . 4
8 cardom 7503 . . . . 5
9 omelon 7231 . . . . . . . 8
10 onenon 7466 . . . . . . . 8
119, 10ax-mp 10 . . . . . . 7
12 carddom2 7494 . . . . . . 7
1311, 12mpan 654 . . . . . 6
1413biimpar 473 . . . . 5
158, 14syl5eqssr 3144 . . . 4
16 infxpen 7526 . . . 4
177, 15, 16sylancr 647 . . 3
18 entr 6798 . . 3
196, 17, 18syl2anc 645 . 2