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