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

Theorem infxpidm2 8426
 Description: The Cartesian 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 8969. (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 8366 . . . . . 6
21ensymd 7604 . . . . 5
3 xpen 7718 . . . . 5
42, 2, 3syl2anc 659 . . . 4
6 cardon 8357 . . . 4
7 cardom 8399 . . . . 5
8 omelon 8096 . . . . . . . 8
9 onenon 8362 . . . . . . . 8
108, 9ax-mp 5 . . . . . . 7
11 carddom2 8390 . . . . . . 7
1210, 11mpan 668 . . . . . 6
1312biimpar 483 . . . . 5
147, 13syl5eqssr 3487 . . . 4
15 infxpen 8424 . . . 4
166, 14, 15sylancr 661 . . 3
17 entr 7605 . . 3
185, 16, 17syl2anc 659 . 2