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

Theorem infdif 9638
 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 1133 . . 3 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → 𝐴 ∈ dom card)
2 difss 4062 . . 3 (𝐴𝐵) ⊆ 𝐴
3 ssdomg 8556 . . 3 (𝐴 ∈ dom card → ((𝐴𝐵) ⊆ 𝐴 → (𝐴𝐵) ≼ 𝐴))
41, 2, 3mpisyl 21 . 2 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → (𝐴𝐵) ≼ 𝐴)
5 sdomdom 8538 . . . . . . . . 9 (𝐵𝐴𝐵𝐴)
653ad2ant3 1132 . . . . . . . 8 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → 𝐵𝐴)
7 numdom 9467 . . . . . . . 8 ((𝐴 ∈ dom card ∧ 𝐵𝐴) → 𝐵 ∈ dom card)
81, 6, 7syl2anc 587 . . . . . . 7 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → 𝐵 ∈ dom card)
9 unnum 9625 . . . . . . 7 ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴𝐵) ∈ dom card)
101, 8, 9syl2anc 587 . . . . . 6 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → (𝐴𝐵) ∈ dom card)
11 ssun1 4102 . . . . . 6 𝐴 ⊆ (𝐴𝐵)
12 ssdomg 8556 . . . . . 6 ((𝐴𝐵) ∈ dom card → (𝐴 ⊆ (𝐴𝐵) → 𝐴 ≼ (𝐴𝐵)))
1310, 11, 12mpisyl 21 . . . . 5 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → 𝐴 ≼ (𝐴𝐵))
14 undif1 4385 . . . . . 6 ((𝐴𝐵) ∪ 𝐵) = (𝐴𝐵)
15 ssnum 9468 . . . . . . . 8 ((𝐴 ∈ dom card ∧ (𝐴𝐵) ⊆ 𝐴) → (𝐴𝐵) ∈ dom card)
161, 2, 15sylancl 589 . . . . . . 7 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → (𝐴𝐵) ∈ dom card)
17 undjudom 9596 . . . . . . 7 (((𝐴𝐵) ∈ dom card ∧ 𝐵 ∈ dom card) → ((𝐴𝐵) ∪ 𝐵) ≼ ((𝐴𝐵) ⊔ 𝐵))
1816, 8, 17syl2anc 587 . . . . . 6 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → ((𝐴𝐵) ∪ 𝐵) ≼ ((𝐴𝐵) ⊔ 𝐵))
1914, 18eqbrtrrid 5070 . . . . 5 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → (𝐴𝐵) ≼ ((𝐴𝐵) ⊔ 𝐵))
20 domtr 8563 . . . . 5 ((𝐴 ≼ (𝐴𝐵) ∧ (𝐴𝐵) ≼ ((𝐴𝐵) ⊔ 𝐵)) → 𝐴 ≼ ((𝐴𝐵) ⊔ 𝐵))
2113, 19, 20syl2anc 587 . . . 4 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → 𝐴 ≼ ((𝐴𝐵) ⊔ 𝐵))
22 simp3 1135 . . . . . . 7 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → 𝐵𝐴)
23 sdomdom 8538 . . . . . . . . 9 ((𝐴𝐵) ≺ 𝐵 → (𝐴𝐵) ≼ 𝐵)
24 relsdom 8517 . . . . . . . . . 10 Rel ≺
2524brrelex2i 5577 . . . . . . . . 9 ((𝐴𝐵) ≺ 𝐵𝐵 ∈ V)
26 djudom1 9611 . . . . . . . . 9 (((𝐴𝐵) ≼ 𝐵𝐵 ∈ V) → ((𝐴𝐵) ⊔ 𝐵) ≼ (𝐵𝐵))
2723, 25, 26syl2anc 587 . . . . . . . 8 ((𝐴𝐵) ≺ 𝐵 → ((𝐴𝐵) ⊔ 𝐵) ≼ (𝐵𝐵))
28 domtr 8563 . . . . . . . . . . 11 ((𝐴 ≼ ((𝐴𝐵) ⊔ 𝐵) ∧ ((𝐴𝐵) ⊔ 𝐵) ≼ (𝐵𝐵)) → 𝐴 ≼ (𝐵𝐵))
2928ex 416 . . . . . . . . . 10 (𝐴 ≼ ((𝐴𝐵) ⊔ 𝐵) → (((𝐴𝐵) ⊔ 𝐵) ≼ (𝐵𝐵) → 𝐴 ≼ (𝐵𝐵)))
3021, 29syl 17 . . . . . . . . 9 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → (((𝐴𝐵) ⊔ 𝐵) ≼ (𝐵𝐵) → 𝐴 ≼ (𝐵𝐵)))
31 simp2 1134 . . . . . . . . . . . 12 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → ω ≼ 𝐴)
32 domtr 8563 . . . . . . . . . . . . 13 ((ω ≼ 𝐴𝐴 ≼ (𝐵𝐵)) → ω ≼ (𝐵𝐵))
3332ex 416 . . . . . . . . . . . 12 (ω ≼ 𝐴 → (𝐴 ≼ (𝐵𝐵) → ω ≼ (𝐵𝐵)))
3431, 33syl 17 . . . . . . . . . . 11 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → (𝐴 ≼ (𝐵𝐵) → ω ≼ (𝐵𝐵)))
35 djuinf 9617 . . . . . . . . . . . . 13 (ω ≼ 𝐵 ↔ ω ≼ (𝐵𝐵))
3635biimpri 231 . . . . . . . . . . . 12 (ω ≼ (𝐵𝐵) → ω ≼ 𝐵)
37 domrefg 8545 . . . . . . . . . . . . 13 (𝐵 ∈ dom card → 𝐵𝐵)
38 infdjuabs 9635 . . . . . . . . . . . . . . 15 ((𝐵 ∈ dom card ∧ ω ≼ 𝐵𝐵𝐵) → (𝐵𝐵) ≈ 𝐵)
39383com23 1123 . . . . . . . . . . . . . 14 ((𝐵 ∈ dom card ∧ 𝐵𝐵 ∧ ω ≼ 𝐵) → (𝐵𝐵) ≈ 𝐵)
40393expia 1118 . . . . . . . . . . . . 13 ((𝐵 ∈ dom card ∧ 𝐵𝐵) → (ω ≼ 𝐵 → (𝐵𝐵) ≈ 𝐵))
4137, 40mpdan 686 . . . . . . . . . . . 12 (𝐵 ∈ dom card → (ω ≼ 𝐵 → (𝐵𝐵) ≈ 𝐵))
428, 36, 41syl2im 40 . . . . . . . . . . 11 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → (ω ≼ (𝐵𝐵) → (𝐵𝐵) ≈ 𝐵))
4334, 42syld 47 . . . . . . . . . 10 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → (𝐴 ≼ (𝐵𝐵) → (𝐵𝐵) ≈ 𝐵))
44 domen2 8662 . . . . . . . . . . 11 ((𝐵𝐵) ≈ 𝐵 → (𝐴 ≼ (𝐵𝐵) ↔ 𝐴𝐵))
4544biimpcd 252 . . . . . . . . . 10 (𝐴 ≼ (𝐵𝐵) → ((𝐵𝐵) ≈ 𝐵𝐴𝐵))
4643, 45sylcom 30 . . . . . . . . 9 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → (𝐴 ≼ (𝐵𝐵) → 𝐴𝐵))
4730, 46syld 47 . . . . . . . 8 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → (((𝐴𝐵) ⊔ 𝐵) ≼ (𝐵𝐵) → 𝐴𝐵))
48 domnsym 8645 . . . . . . . 8 (𝐴𝐵 → ¬ 𝐵𝐴)
4927, 47, 48syl56 36 . . . . . . 7 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → ((𝐴𝐵) ≺ 𝐵 → ¬ 𝐵𝐴))
5022, 49mt2d 138 . . . . . 6 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → ¬ (𝐴𝐵) ≺ 𝐵)
51 domtri2 9420 . . . . . . 7 ((𝐵 ∈ dom card ∧ (𝐴𝐵) ∈ dom card) → (𝐵 ≼ (𝐴𝐵) ↔ ¬ (𝐴𝐵) ≺ 𝐵))
528, 16, 51syl2anc 587 . . . . . 6 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → (𝐵 ≼ (𝐴𝐵) ↔ ¬ (𝐴𝐵) ≺ 𝐵))
5350, 52mpbird 260 . . . . 5 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → 𝐵 ≼ (𝐴𝐵))
54 difexg 5199 . . . . . 6 (𝐴 ∈ dom card → (𝐴𝐵) ∈ V)
551, 54syl 17 . . . . 5 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → (𝐴𝐵) ∈ V)
56 djudom2 9612 . . . . 5 ((𝐵 ≼ (𝐴𝐵) ∧ (𝐴𝐵) ∈ V) → ((𝐴𝐵) ⊔ 𝐵) ≼ ((𝐴𝐵) ⊔ (𝐴𝐵)))
5753, 55, 56syl2anc 587 . . . 4 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → ((𝐴𝐵) ⊔ 𝐵) ≼ ((𝐴𝐵) ⊔ (𝐴𝐵)))
58 domtr 8563 . . . 4 ((𝐴 ≼ ((𝐴𝐵) ⊔ 𝐵) ∧ ((𝐴𝐵) ⊔ 𝐵) ≼ ((𝐴𝐵) ⊔ (𝐴𝐵))) → 𝐴 ≼ ((𝐴𝐵) ⊔ (𝐴𝐵)))
5921, 57, 58syl2anc 587 . . 3 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → 𝐴 ≼ ((𝐴𝐵) ⊔ (𝐴𝐵)))
60 domtr 8563 . . . . . 6 ((ω ≼ 𝐴𝐴 ≼ ((𝐴𝐵) ⊔ (𝐴𝐵))) → ω ≼ ((𝐴𝐵) ⊔ (𝐴𝐵)))
6131, 59, 60syl2anc 587 . . . . 5 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → ω ≼ ((𝐴𝐵) ⊔ (𝐴𝐵)))
62 djuinf 9617 . . . . 5 (ω ≼ (𝐴𝐵) ↔ ω ≼ ((𝐴𝐵) ⊔ (𝐴𝐵)))
6361, 62sylibr 237 . . . 4 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → ω ≼ (𝐴𝐵))
64 domrefg 8545 . . . . 5 ((𝐴𝐵) ∈ dom card → (𝐴𝐵) ≼ (𝐴𝐵))
6516, 64syl 17 . . . 4 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → (𝐴𝐵) ≼ (𝐴𝐵))
66 infdjuabs 9635 . . . 4 (((𝐴𝐵) ∈ dom card ∧ ω ≼ (𝐴𝐵) ∧ (𝐴𝐵) ≼ (𝐴𝐵)) → ((𝐴𝐵) ⊔ (𝐴𝐵)) ≈ (𝐴𝐵))
6716, 63, 65, 66syl3anc 1368 . . 3 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → ((𝐴𝐵) ⊔ (𝐴𝐵)) ≈ (𝐴𝐵))
68 domentr 8569 . . 3 ((𝐴 ≼ ((𝐴𝐵) ⊔ (𝐴𝐵)) ∧ ((𝐴𝐵) ⊔ (𝐴𝐵)) ≈ (𝐴𝐵)) → 𝐴 ≼ (𝐴𝐵))
6959, 67, 68syl2anc 587 . 2 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → 𝐴 ≼ (𝐴𝐵))
70 sbth 8639 . 2 (((𝐴𝐵) ≼ 𝐴𝐴 ≼ (𝐴𝐵)) → (𝐴𝐵) ≈ 𝐴)
714, 69, 70syl2anc 587 1 ((𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴) → (𝐴𝐵) ≈ 𝐴)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ w3a 1084   ∈ wcel 2111  Vcvv 3442   ∖ cdif 3880   ∪ cun 3881   ⊆ wss 3883   class class class wbr 5034  dom cdm 5523  ωcom 7573   ≈ cen 8507   ≼ cdom 8508   ≺ csdm 8509   ⊔ cdju 9329  cardccrd 9366 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 2770  ax-rep 5158  ax-sep 5171  ax-nul 5178  ax-pow 5235  ax-pr 5299  ax-un 7454  ax-inf2 9106 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3444  df-sbc 3723  df-csb 3831  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4805  df-int 4843  df-iun 4887  df-br 5035  df-opab 5097  df-mpt 5115  df-tr 5141  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6123  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6334  df-fn 6335  df-f 6336  df-f1 6337  df-fo 6338  df-f1o 6339  df-fv 6340  df-isom 6341  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7574  df-1st 7684  df-2nd 7685  df-wrecs 7948  df-recs 8009  df-rdg 8047  df-1o 8103  df-2o 8104  df-oadd 8107  df-er 8290  df-en 8511  df-dom 8512  df-sdom 8513  df-fin 8514  df-oi 8976  df-dju 9332  df-card 9370 This theorem is referenced by:  infdif2  9639  alephsuc3  10009  aleph1irr  15611
 Copyright terms: Public domain W3C validator