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

Theorem infdif 9231
Description: The cardinality of an infinite set does not change after subtracting a strictly smaller one. Example in [Enderton] p. 164. (Contributed by NM, 22-Oct-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
Assertion
Ref Expression
infdif ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → (𝐴𝐵) ≈ 𝐴)

Proof of Theorem infdif
StepHypRef Expression
1 simp1 1128 . . 3 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → 𝐴 ∈ dom card)
2 difss 3885 . . 3 (𝐴𝐵) ⊆ 𝐴
3 ssdomg 8153 . . 3 (𝐴 ∈ dom card → ((𝐴𝐵) ⊆ 𝐴 → (𝐴𝐵) ≼ 𝐴))
41, 2, 3mpisyl 21 . 2 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → (𝐴𝐵) ≼ 𝐴)
5 sdomdom 8135 . . . . . . . . 9 (𝐵𝐴𝐵𝐴)
653ad2ant3 1127 . . . . . . . 8 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → 𝐵𝐴)
7 numdom 9059 . . . . . . . 8 ((𝐴 ∈ dom card ∧ 𝐵𝐴) → 𝐵 ∈ dom card)
81, 6, 7syl2anc 693 . . . . . . 7 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → 𝐵 ∈ dom card)
9 unnum 9222 . . . . . . 7 ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴𝐵) ∈ dom card)
101, 8, 9syl2anc 693 . . . . . 6 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → (𝐴𝐵) ∈ dom card)
11 ssun1 3924 . . . . . 6 𝐴 ⊆ (𝐴𝐵)
12 ssdomg 8153 . . . . . 6 ((𝐴𝐵) ∈ dom card → (𝐴 ⊆ (𝐴𝐵) → 𝐴 ≼ (𝐴𝐵)))
1310, 11, 12mpisyl 21 . . . . 5 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → 𝐴 ≼ (𝐴𝐵))
14 undif1 4182 . . . . . 6 ((𝐴𝐵) ∪ 𝐵) = (𝐴𝐵)
15 ssnum 9060 . . . . . . . 8 ((𝐴 ∈ dom card ∧ (𝐴𝐵) ⊆ 𝐴) → (𝐴𝐵) ∈ dom card)
161, 2, 15sylancl 694 . . . . . . 7 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → (𝐴𝐵) ∈ dom card)
17 uncdadom 9193 . . . . . . 7 (((𝐴𝐵) ∈ dom card ∧ 𝐵 ∈ dom card) → ((𝐴𝐵) ∪ 𝐵) ≼ ((𝐴𝐵) +𝑐 𝐵))
1816, 8, 17syl2anc 693 . . . . . 6 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → ((𝐴𝐵) ∪ 𝐵) ≼ ((𝐴𝐵) +𝑐 𝐵))
1914, 18syl5eqbrr 4819 . . . . 5 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → (𝐴𝐵) ≼ ((𝐴𝐵) +𝑐 𝐵))
20 domtr 8160 . . . . 5 ((𝐴 ≼ (𝐴𝐵) ∧ (𝐴𝐵) ≼ ((𝐴𝐵) +𝑐 𝐵)) → 𝐴 ≼ ((𝐴𝐵) +𝑐 𝐵))
2113, 19, 20syl2anc 693 . . . 4 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → 𝐴 ≼ ((𝐴𝐵) +𝑐 𝐵))
22 simp3 1130 . . . . . . 7 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → 𝐵𝐴)
23 sdomdom 8135 . . . . . . . . 9 ((𝐴𝐵) ≺ 𝐵 → (𝐴𝐵) ≼ 𝐵)
24 cdadom1 9208 . . . . . . . . 9 ((𝐴𝐵) ≼ 𝐵 → ((𝐴𝐵) +𝑐 𝐵) ≼ (𝐵 +𝑐 𝐵))
2523, 24syl 17 . . . . . . . 8 ((𝐴𝐵) ≺ 𝐵 → ((𝐴𝐵) +𝑐 𝐵) ≼ (𝐵 +𝑐 𝐵))
26 domtr 8160 . . . . . . . . . . 11 ((𝐴 ≼ ((𝐴𝐵) +𝑐 𝐵) ∧ ((𝐴𝐵) +𝑐 𝐵) ≼ (𝐵 +𝑐 𝐵)) → 𝐴 ≼ (𝐵 +𝑐 𝐵))
2726ex 448 . . . . . . . . . 10 (𝐴 ≼ ((𝐴𝐵) +𝑐 𝐵) → (((𝐴𝐵) +𝑐 𝐵) ≼ (𝐵 +𝑐 𝐵) → 𝐴 ≼ (𝐵 +𝑐 𝐵)))
2821, 27syl 17 . . . . . . . . 9 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → (((𝐴𝐵) +𝑐 𝐵) ≼ (𝐵 +𝑐 𝐵) → 𝐴 ≼ (𝐵 +𝑐 𝐵)))
29 simp2 1129 . . . . . . . . . . . 12 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → ω ≼ 𝐴)
30 domtr 8160 . . . . . . . . . . . . 13 ((ω ≼ 𝐴𝐴 ≼ (𝐵 +𝑐 𝐵)) → ω ≼ (𝐵 +𝑐 𝐵))
3130ex 448 . . . . . . . . . . . 12 (ω ≼ 𝐴 → (𝐴 ≼ (𝐵 +𝑐 𝐵) → ω ≼ (𝐵 +𝑐 𝐵)))
3229, 31syl 17 . . . . . . . . . . 11 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → (𝐴 ≼ (𝐵 +𝑐 𝐵) → ω ≼ (𝐵 +𝑐 𝐵)))
33 cdainf 9214 . . . . . . . . . . . . 13 (ω ≼ 𝐵 ↔ ω ≼ (𝐵 +𝑐 𝐵))
3433biimpri 218 . . . . . . . . . . . 12 (ω ≼ (𝐵 +𝑐 𝐵) → ω ≼ 𝐵)
35 domrefg 8142 . . . . . . . . . . . . 13 (𝐵 ∈ dom card → 𝐵𝐵)
36 infcdaabs 9228 . . . . . . . . . . . . . . 15 ((𝐵 ∈ dom card ∧ ω ≼ 𝐵𝐵𝐵) → (𝐵 +𝑐 𝐵) ≈ 𝐵)
37363com23 1118 . . . . . . . . . . . . . 14 ((𝐵 ∈ dom card ∧ 𝐵𝐵 ∧ ω ≼ 𝐵) → (𝐵 +𝑐 𝐵) ≈ 𝐵)
38373expia 1112 . . . . . . . . . . . . 13 ((𝐵 ∈ dom card ∧ 𝐵𝐵) → (ω ≼ 𝐵 → (𝐵 +𝑐 𝐵) ≈ 𝐵))
3935, 38mpdan 702 . . . . . . . . . . . 12 (𝐵 ∈ dom card → (ω ≼ 𝐵 → (𝐵 +𝑐 𝐵) ≈ 𝐵))
408, 34, 39syl2im 40 . . . . . . . . . . 11 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → (ω ≼ (𝐵 +𝑐 𝐵) → (𝐵 +𝑐 𝐵) ≈ 𝐵))
4132, 40syld 47 . . . . . . . . . 10 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → (𝐴 ≼ (𝐵 +𝑐 𝐵) → (𝐵 +𝑐 𝐵) ≈ 𝐵))
42 domen2 8257 . . . . . . . . . . 11 ((𝐵 +𝑐 𝐵) ≈ 𝐵 → (𝐴 ≼ (𝐵 +𝑐 𝐵) ↔ 𝐴𝐵))
4342biimpcd 239 . . . . . . . . . 10 (𝐴 ≼ (𝐵 +𝑐 𝐵) → ((𝐵 +𝑐 𝐵) ≈ 𝐵𝐴𝐵))
4441, 43sylcom 30 . . . . . . . . 9 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → (𝐴 ≼ (𝐵 +𝑐 𝐵) → 𝐴𝐵))
4528, 44syld 47 . . . . . . . 8 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → (((𝐴𝐵) +𝑐 𝐵) ≼ (𝐵 +𝑐 𝐵) → 𝐴𝐵))
46 domnsym 8240 . . . . . . . 8 (𝐴𝐵 → ¬ 𝐵𝐴)
4725, 45, 46syl56 36 . . . . . . 7 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → ((𝐴𝐵) ≺ 𝐵 → ¬ 𝐵𝐴))
4822, 47mt2d 133 . . . . . 6 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → ¬ (𝐴𝐵) ≺ 𝐵)
49 domtri2 9013 . . . . . . 7 ((𝐵 ∈ dom card ∧ (𝐴𝐵) ∈ dom card) → (𝐵 ≼ (𝐴𝐵) ↔ ¬ (𝐴𝐵) ≺ 𝐵))
508, 16, 49syl2anc 693 . . . . . 6 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → (𝐵 ≼ (𝐴𝐵) ↔ ¬ (𝐴𝐵) ≺ 𝐵))
5148, 50mpbird 247 . . . . 5 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → 𝐵 ≼ (𝐴𝐵))
52 cdadom2 9209 . . . . 5 (𝐵 ≼ (𝐴𝐵) → ((𝐴𝐵) +𝑐 𝐵) ≼ ((𝐴𝐵) +𝑐 (𝐴𝐵)))
5351, 52syl 17 . . . 4 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → ((𝐴𝐵) +𝑐 𝐵) ≼ ((𝐴𝐵) +𝑐 (𝐴𝐵)))
54 domtr 8160 . . . 4 ((𝐴 ≼ ((𝐴𝐵) +𝑐 𝐵) ∧ ((𝐴𝐵) +𝑐 𝐵) ≼ ((𝐴𝐵) +𝑐 (𝐴𝐵))) → 𝐴 ≼ ((𝐴𝐵) +𝑐 (𝐴𝐵)))
5521, 53, 54syl2anc 693 . . 3 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → 𝐴 ≼ ((𝐴𝐵) +𝑐 (𝐴𝐵)))
56 domtr 8160 . . . . . 6 ((ω ≼ 𝐴𝐴 ≼ ((𝐴𝐵) +𝑐 (𝐴𝐵))) → ω ≼ ((𝐴𝐵) +𝑐 (𝐴𝐵)))
5729, 55, 56syl2anc 693 . . . . 5 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → ω ≼ ((𝐴𝐵) +𝑐 (𝐴𝐵)))
58 cdainf 9214 . . . . 5 (ω ≼ (𝐴𝐵) ↔ ω ≼ ((𝐴𝐵) +𝑐 (𝐴𝐵)))
5957, 58sylibr 224 . . . 4 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → ω ≼ (𝐴𝐵))
60 domrefg 8142 . . . . 5 ((𝐴𝐵) ∈ dom card → (𝐴𝐵) ≼ (𝐴𝐵))
6116, 60syl 17 . . . 4 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → (𝐴𝐵) ≼ (𝐴𝐵))
62 infcdaabs 9228 . . . 4 (((𝐴𝐵) ∈ dom card ∧ ω ≼ (𝐴𝐵) ∧ (𝐴𝐵) ≼ (𝐴𝐵)) → ((𝐴𝐵) +𝑐 (𝐴𝐵)) ≈ (𝐴𝐵))
6316, 59, 61, 62syl3anc 1474 . . 3 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → ((𝐴𝐵) +𝑐 (𝐴𝐵)) ≈ (𝐴𝐵))
64 domentr 8166 . . 3 ((𝐴 ≼ ((𝐴𝐵) +𝑐 (𝐴𝐵)) ∧ ((𝐴𝐵) +𝑐 (𝐴𝐵)) ≈ (𝐴𝐵)) → 𝐴 ≼ (𝐴𝐵))
6555, 63, 64syl2anc 693 . 2 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → 𝐴 ≼ (𝐴𝐵))
66 sbth 8234 . 2 (((𝐴𝐵) ≼ 𝐴𝐴 ≼ (𝐴𝐵)) → (𝐴𝐵) ≈ 𝐴)
674, 65, 66syl2anc 693 1 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → (𝐴𝐵) ≈ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  w3a 1069  wcel 2143  cdif 3717  cun 3718  wss 3720   class class class wbr 4783  dom cdm 5248  (class class class)co 6791  ωcom 7210  cen 8104  cdom 8105  csdm 8106  cardccrd 8959   +𝑐 ccda 9189
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1868  ax-4 1883  ax-5 1989  ax-6 2055  ax-7 2091  ax-8 2145  ax-9 2152  ax-10 2172  ax-11 2188  ax-12 2201  ax-13 2406  ax-ext 2749  ax-rep 4901  ax-sep 4911  ax-nul 4919  ax-pow 4970  ax-pr 5033  ax-un 7094  ax-inf2 8700
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1070  df-3an 1071  df-tru 1632  df-ex 1851  df-nf 1856  df-sb 2048  df-eu 2620  df-mo 2621  df-clab 2756  df-cleq 2762  df-clel 2765  df-nfc 2900  df-ne 2942  df-ral 3064  df-rex 3065  df-reu 3066  df-rmo 3067  df-rab 3068  df-v 3350  df-sbc 3585  df-csb 3680  df-dif 3723  df-un 3725  df-in 3727  df-ss 3734  df-pss 3736  df-nul 4061  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-tp 4318  df-op 4320  df-uni 4572  df-int 4609  df-iun 4653  df-br 4784  df-opab 4844  df-mpt 4861  df-tr 4884  df-id 5156  df-eprel 5161  df-po 5169  df-so 5170  df-fr 5207  df-se 5208  df-we 5209  df-xp 5254  df-rel 5255  df-cnv 5256  df-co 5257  df-dm 5258  df-rn 5259  df-res 5260  df-ima 5261  df-pred 5822  df-ord 5868  df-on 5869  df-lim 5870  df-suc 5871  df-iota 5993  df-fun 6032  df-fn 6033  df-f 6034  df-f1 6035  df-fo 6036  df-f1o 6037  df-fv 6038  df-isom 6039  df-riota 6752  df-ov 6794  df-oprab 6795  df-mpt2 6796  df-om 7211  df-1st 7313  df-2nd 7314  df-wrecs 7557  df-recs 7619  df-rdg 7657  df-1o 7711  df-2o 7712  df-oadd 7715  df-er 7894  df-en 8108  df-dom 8109  df-sdom 8110  df-fin 8111  df-oi 8569  df-card 8963  df-cda 9190
This theorem is referenced by:  infdif2  9232  alephsuc3  9602  aleph1irr  15186
  Copyright terms: Public domain W3C validator