Metamath Proof Explorer

Theorem infxp

Description: Absorption law for multiplication with an infinite cardinal. Equivalent to Proposition 10.41 of TakeutiZaring p. 95. (Contributed by NM, 28-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion infxp ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) → ( 𝐴 × 𝐵 ) ≈ ( 𝐴 ∪ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 sdomdom ⊢ ( 𝐵 ≺ 𝐴 → 𝐵 ≼ 𝐴 )
2 infxpabs ⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ≠ ∅ ∧ 𝐵 ≼ 𝐴 ) ) → ( 𝐴 × 𝐵 ) ≈ 𝐴 )
3 infunabs ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → ( 𝐴 ∪ 𝐵 ) ≈ 𝐴 )
4 3 3expa ⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ 𝐵 ≼ 𝐴 ) → ( 𝐴 ∪ 𝐵 ) ≈ 𝐴 )
5 4 adantrl ⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ≠ ∅ ∧ 𝐵 ≼ 𝐴 ) ) → ( 𝐴 ∪ 𝐵 ) ≈ 𝐴 )
6 5 ensymd ⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ≠ ∅ ∧ 𝐵 ≼ 𝐴 ) ) → 𝐴 ≈ ( 𝐴 ∪ 𝐵 ) )
7 entr ⊢ ( ( ( 𝐴 × 𝐵 ) ≈ 𝐴 ∧ 𝐴 ≈ ( 𝐴 ∪ 𝐵 ) ) → ( 𝐴 × 𝐵 ) ≈ ( 𝐴 ∪ 𝐵 ) )
8 2 6 7 syl2anc ⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ≠ ∅ ∧ 𝐵 ≼ 𝐴 ) ) → ( 𝐴 × 𝐵 ) ≈ ( 𝐴 ∪ 𝐵 ) )
9 8 expr ⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ 𝐵 ≠ ∅ ) → ( 𝐵 ≼ 𝐴 → ( 𝐴 × 𝐵 ) ≈ ( 𝐴 ∪ 𝐵 ) ) )
10 9 adantrl ⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) → ( 𝐵 ≼ 𝐴 → ( 𝐴 × 𝐵 ) ≈ ( 𝐴 ∪ 𝐵 ) ) )
11 1 10 syl5 ⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) → ( 𝐵 ≺ 𝐴 → ( 𝐴 × 𝐵 ) ≈ ( 𝐴 ∪ 𝐵 ) ) )
12 domtri2 ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( 𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴 ) )
13 12 ad2ant2r ⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) → ( 𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴 ) )
14 xpcomeng ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( 𝐴 × 𝐵 ) ≈ ( 𝐵 × 𝐴 ) )
15 14 ad2ant2r ⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) → ( 𝐴 × 𝐵 ) ≈ ( 𝐵 × 𝐴 ) )
16 simplrl ⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) ∧ 𝐴 ≼ 𝐵 ) → 𝐵 ∈ dom card )
17 domtr ⊢ ( ( ω ≼ 𝐴 ∧ 𝐴 ≼ 𝐵 ) → ω ≼ 𝐵 )
18 17 ad4ant24 ⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) ∧ 𝐴 ≼ 𝐵 ) → ω ≼ 𝐵 )
19 infn0 ⊢ ( ω ≼ 𝐴 → 𝐴 ≠ ∅ )
20 19 ad3antlr ⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) ∧ 𝐴 ≼ 𝐵 ) → 𝐴 ≠ ∅ )
21 simpr ⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) ∧ 𝐴 ≼ 𝐵 ) → 𝐴 ≼ 𝐵 )
22 infxpabs ⊢ ( ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) ∧ ( 𝐴 ≠ ∅ ∧ 𝐴 ≼ 𝐵 ) ) → ( 𝐵 × 𝐴 ) ≈ 𝐵 )
23 16 18 20 21 22 syl22anc ⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) ∧ 𝐴 ≼ 𝐵 ) → ( 𝐵 × 𝐴 ) ≈ 𝐵 )
24 uncom ⊢ ( 𝐴 ∪ 𝐵 ) = ( 𝐵 ∪ 𝐴 )
25 infunabs ⊢ ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ∧ 𝐴 ≼ 𝐵 ) → ( 𝐵 ∪ 𝐴 ) ≈ 𝐵 )
26 16 18 21 25 syl3anc ⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) ∧ 𝐴 ≼ 𝐵 ) → ( 𝐵 ∪ 𝐴 ) ≈ 𝐵 )
27 24 26 eqbrtrid ⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) ∧ 𝐴 ≼ 𝐵 ) → ( 𝐴 ∪ 𝐵 ) ≈ 𝐵 )
28 27 ensymd ⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) ∧ 𝐴 ≼ 𝐵 ) → 𝐵 ≈ ( 𝐴 ∪ 𝐵 ) )
29 entr ⊢ ( ( ( 𝐵 × 𝐴 ) ≈ 𝐵 ∧ 𝐵 ≈ ( 𝐴 ∪ 𝐵 ) ) → ( 𝐵 × 𝐴 ) ≈ ( 𝐴 ∪ 𝐵 ) )
30 23 28 29 syl2anc ⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) ∧ 𝐴 ≼ 𝐵 ) → ( 𝐵 × 𝐴 ) ≈ ( 𝐴 ∪ 𝐵 ) )
31 entr ⊢ ( ( ( 𝐴 × 𝐵 ) ≈ ( 𝐵 × 𝐴 ) ∧ ( 𝐵 × 𝐴 ) ≈ ( 𝐴 ∪ 𝐵 ) ) → ( 𝐴 × 𝐵 ) ≈ ( 𝐴 ∪ 𝐵 ) )
32 15 30 31 syl2an2r ⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) ∧ 𝐴 ≼ 𝐵 ) → ( 𝐴 × 𝐵 ) ≈ ( 𝐴 ∪ 𝐵 ) )
33 32 ex ⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) → ( 𝐴 ≼ 𝐵 → ( 𝐴 × 𝐵 ) ≈ ( 𝐴 ∪ 𝐵 ) ) )
34 13 33 sylbird ⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) → ( ¬ 𝐵 ≺ 𝐴 → ( 𝐴 × 𝐵 ) ≈ ( 𝐴 ∪ 𝐵 ) ) )
35 11 34 pm2.61d ⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) → ( 𝐴 × 𝐵 ) ≈ ( 𝐴 ∪ 𝐵 ) )