Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  infxp Structured version   Visualization version   GIF version

Theorem infxp 9680
 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.)
Assertion
Ref Expression
infxp (((𝐴 ∈ dom card ∧ ω ≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) → (𝐴 × 𝐵) ≈ (𝐴𝐵))

Proof of Theorem infxp
StepHypRef Expression
1 sdomdom 8560 . . 3 (𝐵𝐴𝐵𝐴)
2 infxpabs 9677 . . . . . 6 (((𝐴 ∈ dom card ∧ ω ≼ 𝐴) ∧ (𝐵 ≠ ∅ ∧ 𝐵𝐴)) → (𝐴 × 𝐵) ≈ 𝐴)
3 infunabs 9672 . . . . . . . . 9 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → (𝐴𝐵) ≈ 𝐴)
433expa 1115 . . . . . . . 8 (((𝐴 ∈ dom card ∧ ω ≼ 𝐴) ∧ 𝐵𝐴) → (𝐴𝐵) ≈ 𝐴)
54adantrl 715 . . . . . . 7 (((𝐴 ∈ dom card ∧ ω ≼ 𝐴) ∧ (𝐵 ≠ ∅ ∧ 𝐵𝐴)) → (𝐴𝐵) ≈ 𝐴)
65ensymd 8583 . . . . . 6 (((𝐴 ∈ dom card ∧ ω ≼ 𝐴) ∧ (𝐵 ≠ ∅ ∧ 𝐵𝐴)) → 𝐴 ≈ (𝐴𝐵))
7 entr 8584 . . . . . 6 (((𝐴 × 𝐵) ≈ 𝐴𝐴 ≈ (𝐴𝐵)) → (𝐴 × 𝐵) ≈ (𝐴𝐵))
82, 6, 7syl2anc 587 . . . . 5 (((𝐴 ∈ dom card ∧ ω ≼ 𝐴) ∧ (𝐵 ≠ ∅ ∧ 𝐵𝐴)) → (𝐴 × 𝐵) ≈ (𝐴𝐵))
98expr 460 . . . 4 (((𝐴 ∈ dom card ∧ ω ≼ 𝐴) ∧ 𝐵 ≠ ∅) → (𝐵𝐴 → (𝐴 × 𝐵) ≈ (𝐴𝐵)))
109adantrl 715 . . 3 (((𝐴 ∈ dom card ∧ ω ≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) → (𝐵𝐴 → (𝐴 × 𝐵) ≈ (𝐴𝐵)))
111, 10syl5 34 . 2 (((𝐴 ∈ dom card ∧ ω ≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) → (𝐵𝐴 → (𝐴 × 𝐵) ≈ (𝐴𝐵)))
12 domtri2 9456 . . . 4 ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴𝐵 ↔ ¬ 𝐵𝐴))
1312ad2ant2r 746 . . 3 (((𝐴 ∈ dom card ∧ ω ≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) → (𝐴𝐵 ↔ ¬ 𝐵𝐴))
14 xpcomeng 8635 . . . . . 6 ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 × 𝐵) ≈ (𝐵 × 𝐴))
1514ad2ant2r 746 . . . . 5 (((𝐴 ∈ dom card ∧ ω ≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) → (𝐴 × 𝐵) ≈ (𝐵 × 𝐴))
16 simplrl 776 . . . . . . 7 ((((𝐴 ∈ dom card ∧ ω ≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴𝐵) → 𝐵 ∈ dom card)
17 domtr 8585 . . . . . . . 8 ((ω ≼ 𝐴𝐴𝐵) → ω ≼ 𝐵)
1817ad4ant24 753 . . . . . . 7 ((((𝐴 ∈ dom card ∧ ω ≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴𝐵) → ω ≼ 𝐵)
19 infn0 8818 . . . . . . . 8 (ω ≼ 𝐴𝐴 ≠ ∅)
2019ad3antlr 730 . . . . . . 7 ((((𝐴 ∈ dom card ∧ ω ≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴𝐵) → 𝐴 ≠ ∅)
21 simpr 488 . . . . . . 7 ((((𝐴 ∈ dom card ∧ ω ≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴𝐵) → 𝐴𝐵)
22 infxpabs 9677 . . . . . . 7 (((𝐵 ∈ dom card ∧ ω ≼ 𝐵) ∧ (𝐴 ≠ ∅ ∧ 𝐴𝐵)) → (𝐵 × 𝐴) ≈ 𝐵)
2316, 18, 20, 21, 22syl22anc 837 . . . . . 6 ((((𝐴 ∈ dom card ∧ ω ≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴𝐵) → (𝐵 × 𝐴) ≈ 𝐵)
24 uncom 4060 . . . . . . . 8 (𝐴𝐵) = (𝐵𝐴)
25 infunabs 9672 . . . . . . . . 9 ((𝐵 ∈ dom card ∧ ω ≼ 𝐵𝐴𝐵) → (𝐵𝐴) ≈ 𝐵)
2616, 18, 21, 25syl3anc 1368 . . . . . . . 8 ((((𝐴 ∈ dom card ∧ ω ≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴𝐵) → (𝐵𝐴) ≈ 𝐵)
2724, 26eqbrtrid 5070 . . . . . . 7 ((((𝐴 ∈ dom card ∧ ω ≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴𝐵) → (𝐴𝐵) ≈ 𝐵)
2827ensymd 8583 . . . . . 6 ((((𝐴 ∈ dom card ∧ ω ≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴𝐵) → 𝐵 ≈ (𝐴𝐵))
29 entr 8584 . . . . . 6 (((𝐵 × 𝐴) ≈ 𝐵𝐵 ≈ (𝐴𝐵)) → (𝐵 × 𝐴) ≈ (𝐴𝐵))
3023, 28, 29syl2anc 587 . . . . 5 ((((𝐴 ∈ dom card ∧ ω ≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴𝐵) → (𝐵 × 𝐴) ≈ (𝐴𝐵))
31 entr 8584 . . . . 5 (((𝐴 × 𝐵) ≈ (𝐵 × 𝐴) ∧ (𝐵 × 𝐴) ≈ (𝐴𝐵)) → (𝐴 × 𝐵) ≈ (𝐴𝐵))
3215, 30, 31syl2an2r 684 . . . 4 ((((𝐴 ∈ dom card ∧ ω ≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) ∧ 𝐴𝐵) → (𝐴 × 𝐵) ≈ (𝐴𝐵))
3332ex 416 . . 3 (((𝐴 ∈ dom card ∧ ω ≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) → (𝐴𝐵 → (𝐴 × 𝐵) ≈ (𝐴𝐵)))
3413, 33sylbird 263 . 2 (((𝐴 ∈ dom card ∧ ω ≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) → (¬ 𝐵𝐴 → (𝐴 × 𝐵) ≈ (𝐴𝐵)))
3511, 34pm2.61d 182 1 (((𝐴 ∈ dom card ∧ ω ≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) → (𝐴 × 𝐵) ≈ (𝐴𝐵))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∈ wcel 2111   ≠ wne 2951   ∪ cun 3858  ∅c0 4227   class class class wbr 5035   × cxp 5525  dom cdm 5527  ωcom 7584   ≈ cen 8529   ≼ cdom 8530   ≺ csdm 8531  cardccrd 9402 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5159  ax-sep 5172  ax-nul 5179  ax-pow 5237  ax-pr 5301  ax-un 7464  ax-inf2 9142 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-pss 3879  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4842  df-iun 4888  df-br 5036  df-opab 5098  df-mpt 5116  df-tr 5142  df-id 5433  df-eprel 5438  df-po 5446  df-so 5447  df-fr 5486  df-se 5487  df-we 5488  df-xp 5533  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-rn 5538  df-res 5539  df-ima 5540  df-pred 6130  df-ord 6176  df-on 6177  df-lim 6178  df-suc 6179  df-iota 6298  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-isom 6348  df-riota 7113  df-om 7585  df-1st 7698  df-2nd 7699  df-wrecs 7962  df-recs 8023  df-rdg 8061  df-1o 8117  df-2o 8118  df-er 8304  df-en 8533  df-dom 8534  df-sdom 8535  df-fin 8536  df-oi 9012  df-dju 9368  df-card 9406 This theorem is referenced by:  alephmul  10043
 Copyright terms: Public domain W3C validator