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 ⊢ A ∈ dom ⁡ card ∧ ω ≼ A → A × A ≈ A

Proof

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