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

Theorem infxpidm2 7890
 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 8429. (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 7832 . . . . . 6
21ensymd 7150 . . . . 5
3 xpen 7262 . . . . 5
42, 2, 3syl2anc 643 . . . 4
6 cardon 7823 . . . 4
7 cardom 7865 . . . . 5
8 omelon 7593 . . . . . . . 8
9 onenon 7828 . . . . . . . 8
108, 9ax-mp 8 . . . . . . 7
11 carddom2 7856 . . . . . . 7
1210, 11mpan 652 . . . . . 6
1312biimpar 472 . . . . 5
147, 13syl5eqssr 3385 . . . 4
15 infxpen 7888 . . . 4
166, 14, 15sylancr 645 . . 3
17 entr 7151 . . 3
185, 16, 17syl2anc 643 . 2