Metamath Proof Explorer


Theorem infxpidm2

Description: Every infinite well-orderable set is equinumerous to its Cartesian square. This theorem provides the basis for infinite cardinal arithmetic. Proposition 10.40 of TakeutiZaring p. 95. See also infxpidm . (Contributed by Mario Carneiro, 9-Mar-2013) (Revised by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion infxpidm2 ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝐴 × 𝐴 ) ≈ 𝐴 )

Proof

Step Hyp Ref Expression
1 cardid2 ( 𝐴 ∈ dom card → ( card ‘ 𝐴 ) ≈ 𝐴 )
2 1 ensymd ( 𝐴 ∈ dom card → 𝐴 ≈ ( card ‘ 𝐴 ) )
3 xpen ( ( 𝐴 ≈ ( card ‘ 𝐴 ) ∧ 𝐴 ≈ ( card ‘ 𝐴 ) ) → ( 𝐴 × 𝐴 ) ≈ ( ( card ‘ 𝐴 ) × ( card ‘ 𝐴 ) ) )
4 2 2 3 syl2anc ( 𝐴 ∈ dom card → ( 𝐴 × 𝐴 ) ≈ ( ( card ‘ 𝐴 ) × ( card ‘ 𝐴 ) ) )
5 4 adantr ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝐴 × 𝐴 ) ≈ ( ( card ‘ 𝐴 ) × ( card ‘ 𝐴 ) ) )
6 cardon ( card ‘ 𝐴 ) ∈ On
7 cardom ( card ‘ ω ) = ω
8 omelon ω ∈ On
9 onenon ( ω ∈ On → ω ∈ dom card )
10 8 9 ax-mp ω ∈ dom card
11 carddom2 ( ( ω ∈ dom card ∧ 𝐴 ∈ dom card ) → ( ( card ‘ ω ) ⊆ ( card ‘ 𝐴 ) ↔ ω ≼ 𝐴 ) )
12 10 11 mpan ( 𝐴 ∈ dom card → ( ( card ‘ ω ) ⊆ ( card ‘ 𝐴 ) ↔ ω ≼ 𝐴 ) )
13 12 biimpar ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( card ‘ ω ) ⊆ ( card ‘ 𝐴 ) )
14 7 13 eqsstrrid ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ω ⊆ ( card ‘ 𝐴 ) )
15 infxpen ( ( ( card ‘ 𝐴 ) ∈ On ∧ ω ⊆ ( card ‘ 𝐴 ) ) → ( ( card ‘ 𝐴 ) × ( card ‘ 𝐴 ) ) ≈ ( card ‘ 𝐴 ) )
16 6 14 15 sylancr ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( ( card ‘ 𝐴 ) × ( card ‘ 𝐴 ) ) ≈ ( card ‘ 𝐴 ) )
17 entr ( ( ( 𝐴 × 𝐴 ) ≈ ( ( card ‘ 𝐴 ) × ( card ‘ 𝐴 ) ) ∧ ( ( card ‘ 𝐴 ) × ( card ‘ 𝐴 ) ) ≈ ( card ‘ 𝐴 ) ) → ( 𝐴 × 𝐴 ) ≈ ( card ‘ 𝐴 ) )
18 5 16 17 syl2anc ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝐴 × 𝐴 ) ≈ ( card ‘ 𝐴 ) )
19 1 adantr ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( card ‘ 𝐴 ) ≈ 𝐴 )
20 entr ( ( ( 𝐴 × 𝐴 ) ≈ ( card ‘ 𝐴 ) ∧ ( card ‘ 𝐴 ) ≈ 𝐴 ) → ( 𝐴 × 𝐴 ) ≈ 𝐴 )
21 18 19 20 syl2anc ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝐴 × 𝐴 ) ≈ 𝐴 )