This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem infxpidm

Description: Every infinite class is equinumerous to its Cartesian square. This theorem, which is equivalent to the axiom of choice over ZF, provides the basis for infinite cardinal arithmetic. Proposition 10.40 of TakeutiZaring p. 95. This is a corollary of infxpen (used via infxpidm2 ). (Contributed by NM, 17-Sep-2004) (Revised by Mario Carneiro, 9-Mar-2013)

		Ref	Expression
	Assertion	infxpidm	\|- ( _om ~<_ A -> ( A X. A ) ~~ A )

Proof

Step	Hyp	Ref	Expression
1		reldom	\|- Rel ~<_
2	1	brrelex2i	\|- ( _om ~<_ A -> A e. _V )
3		numth3	\|- ( A e. _V -> A e. dom card )
4	2 3	syl	\|- ( _om ~<_ A -> A e. dom card )
5		infxpidm2	\|- ( ( A e. dom card /\ _om ~<_ A ) -> ( A X. A ) ~~ A )
6	4 5	mpancom	\|- ( _om ~<_ A -> ( A X. A ) ~~ A )