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