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

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