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

Theorem infcda 9324
Description: The sum of two cardinal numbers is their maximum, if one of them is infinite. Proposition 10.41 of [TakeutiZaring] p. 95. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
Assertion
Ref Expression
infcda ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω ≼ 𝐴) → (𝐴 +𝑐 𝐵) ≈ (𝐴𝐵))

Proof of Theorem infcda
StepHypRef Expression
1 unnum 9316 . . . . . . 7 ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴𝐵) ∈ dom card)
213adant3 1155 . . . . . 6 ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω ≼ 𝐴) → (𝐴𝐵) ∈ dom card)
3 ssun2 3987 . . . . . 6 𝐵 ⊆ (𝐴𝐵)
4 ssdomg 8247 . . . . . 6 ((𝐴𝐵) ∈ dom card → (𝐵 ⊆ (𝐴𝐵) → 𝐵 ≼ (𝐴𝐵)))
52, 3, 4mpisyl 21 . . . . 5 ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω ≼ 𝐴) → 𝐵 ≼ (𝐴𝐵))
6 cdadom2 9303 . . . . 5 (𝐵 ≼ (𝐴𝐵) → (𝐴 +𝑐 𝐵) ≼ (𝐴 +𝑐 (𝐴𝐵)))
75, 6syl 17 . . . 4 ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω ≼ 𝐴) → (𝐴 +𝑐 𝐵) ≼ (𝐴 +𝑐 (𝐴𝐵)))
8 cdacomen 9297 . . . 4 (𝐴 +𝑐 (𝐴𝐵)) ≈ ((𝐴𝐵) +𝑐 𝐴)
9 domentr 8260 . . . 4 (((𝐴 +𝑐 𝐵) ≼ (𝐴 +𝑐 (𝐴𝐵)) ∧ (𝐴 +𝑐 (𝐴𝐵)) ≈ ((𝐴𝐵) +𝑐 𝐴)) → (𝐴 +𝑐 𝐵) ≼ ((𝐴𝐵) +𝑐 𝐴))
107, 8, 9sylancl 576 . . 3 ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω ≼ 𝐴) → (𝐴 +𝑐 𝐵) ≼ ((𝐴𝐵) +𝑐 𝐴))
11 simp3 1161 . . . . 5 ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω ≼ 𝐴) → ω ≼ 𝐴)
12 ssun1 3986 . . . . . 6 𝐴 ⊆ (𝐴𝐵)
13 ssdomg 8247 . . . . . 6 ((𝐴𝐵) ∈ dom card → (𝐴 ⊆ (𝐴𝐵) → 𝐴 ≼ (𝐴𝐵)))
142, 12, 13mpisyl 21 . . . . 5 ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω ≼ 𝐴) → 𝐴 ≼ (𝐴𝐵))
15 domtr 8254 . . . . 5 ((ω ≼ 𝐴𝐴 ≼ (𝐴𝐵)) → ω ≼ (𝐴𝐵))
1611, 14, 15syl2anc 575 . . . 4 ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω ≼ 𝐴) → ω ≼ (𝐴𝐵))
17 infcdaabs 9322 . . . 4 (((𝐴𝐵) ∈ dom card ∧ ω ≼ (𝐴𝐵) ∧ 𝐴 ≼ (𝐴𝐵)) → ((𝐴𝐵) +𝑐 𝐴) ≈ (𝐴𝐵))
182, 16, 14, 17syl3anc 1483 . . 3 ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω ≼ 𝐴) → ((𝐴𝐵) +𝑐 𝐴) ≈ (𝐴𝐵))
19 domentr 8260 . . 3 (((𝐴 +𝑐 𝐵) ≼ ((𝐴𝐵) +𝑐 𝐴) ∧ ((𝐴𝐵) +𝑐 𝐴) ≈ (𝐴𝐵)) → (𝐴 +𝑐 𝐵) ≼ (𝐴𝐵))
2010, 18, 19syl2anc 575 . 2 ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω ≼ 𝐴) → (𝐴 +𝑐 𝐵) ≼ (𝐴𝐵))
21 uncdadom 9287 . . 3 ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴𝐵) ≼ (𝐴 +𝑐 𝐵))
22213adant3 1155 . 2 ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω ≼ 𝐴) → (𝐴𝐵) ≼ (𝐴 +𝑐 𝐵))
23 sbth 8328 . 2 (((𝐴 +𝑐 𝐵) ≼ (𝐴𝐵) ∧ (𝐴𝐵) ≼ (𝐴 +𝑐 𝐵)) → (𝐴 +𝑐 𝐵) ≈ (𝐴𝐵))
2420, 22, 23syl2anc 575 1 ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω ≼ 𝐴) → (𝐴 +𝑐 𝐵) ≈ (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1100  wcel 2157  cun 3778  wss 3780   class class class wbr 4855  dom cdm 5324  (class class class)co 6883  ωcom 7304  cen 8198  cdom 8199  cardccrd 9053   +𝑐 ccda 9283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-rep 4977  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-un 7188  ax-inf2 8794
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-pss 3796  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-tp 4386  df-op 4388  df-uni 4642  df-int 4681  df-iun 4725  df-br 4856  df-opab 4918  df-mpt 4935  df-tr 4958  df-id 5232  df-eprel 5237  df-po 5245  df-so 5246  df-fr 5283  df-se 5284  df-we 5285  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-pred 5906  df-ord 5952  df-on 5953  df-lim 5954  df-suc 5955  df-iota 6073  df-fun 6112  df-fn 6113  df-f 6114  df-f1 6115  df-fo 6116  df-f1o 6117  df-fv 6118  df-isom 6119  df-riota 6844  df-ov 6886  df-oprab 6887  df-mpt2 6888  df-om 7305  df-1st 7407  df-2nd 7408  df-wrecs 7651  df-recs 7713  df-rdg 7751  df-1o 7805  df-2o 7806  df-oadd 7809  df-er 7988  df-en 8202  df-dom 8203  df-sdom 8204  df-fin 8205  df-oi 8663  df-card 9057  df-cda 9284
This theorem is referenced by:  alephadd  9693
  Copyright terms: Public domain W3C validator