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	⊢ ( ω ≼ 𝐴 → ( 𝐴 × 𝐴 ) ≈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		reldom	⊢ Rel ≼
2	1	brrelex2i	⊢ ( ω ≼ 𝐴 → 𝐴 ∈ V )
3		numth3	⊢ ( 𝐴 ∈ V → 𝐴 ∈ dom card )
4	2 3	syl	⊢ ( ω ≼ 𝐴 → 𝐴 ∈ dom card )
5		infxpidm2	⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝐴 × 𝐴 ) ≈ 𝐴 )
6	4 5	mpancom	⊢ ( ω ≼ 𝐴 → ( 𝐴 × 𝐴 ) ≈ 𝐴 )