Metamath Proof Explorer

Theorem infxpidm2

Description: The Cartesian product of an infinite set with itself is idempotent. 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 ∧ ω ≼ 𝐴 ) → ( 𝐴 × 𝐴 ) ≈ 𝐴 )