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)
Ref | Expression | ||
---|---|---|---|
Assertion | infdif | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1 | |
|
2 | difss | |
|
3 | ssdomg | |
|
4 | 1 2 3 | mpisyl | |
5 | sdomdom | |
|
6 | 5 | 3ad2ant3 | |
7 | numdom | |
|
8 | 1 6 7 | syl2anc | |
9 | unnum | |
|
10 | 1 8 9 | syl2anc | |
11 | ssun1 | |
|
12 | ssdomg | |
|
13 | 10 11 12 | mpisyl | |
14 | undif1 | |
|
15 | ssnum | |
|
16 | 1 2 15 | sylancl | |
17 | undjudom | |
|
18 | 16 8 17 | syl2anc | |
19 | 14 18 | eqbrtrrid | |
20 | domtr | |
|
21 | 13 19 20 | syl2anc | |
22 | simp3 | |
|
23 | sdomdom | |
|
24 | relsdom | |
|
25 | 24 | brrelex2i | |
26 | djudom1 | |
|
27 | 23 25 26 | syl2anc | |
28 | domtr | |
|
29 | 28 | ex | |
30 | 21 29 | syl | |
31 | simp2 | |
|
32 | domtr | |
|
33 | 32 | ex | |
34 | 31 33 | syl | |
35 | djuinf | |
|
36 | 35 | biimpri | |
37 | domrefg | |
|
38 | infdjuabs | |
|
39 | 38 | 3com23 | |
40 | 39 | 3expia | |
41 | 37 40 | mpdan | |
42 | 8 36 41 | syl2im | |
43 | 34 42 | syld | |
44 | domen2 | |
|
45 | 44 | biimpcd | |
46 | 43 45 | sylcom | |
47 | 30 46 | syld | |
48 | domnsym | |
|
49 | 27 47 48 | syl56 | |
50 | 22 49 | mt2d | |
51 | domtri2 | |
|
52 | 8 16 51 | syl2anc | |
53 | 50 52 | mpbird | |
54 | 1 | difexd | |
55 | djudom2 | |
|
56 | 53 54 55 | syl2anc | |
57 | domtr | |
|
58 | 21 56 57 | syl2anc | |
59 | domtr | |
|
60 | 31 58 59 | syl2anc | |
61 | djuinf | |
|
62 | 60 61 | sylibr | |
63 | domrefg | |
|
64 | 16 63 | syl | |
65 | infdjuabs | |
|
66 | 16 62 64 65 | syl3anc | |
67 | domentr | |
|
68 | 58 66 67 | syl2anc | |
69 | sbth | |
|
70 | 4 68 69 | syl2anc | |