Metamath Proof Explorer


Theorem infdif

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 AdomcardωABAABA

Proof

Step Hyp Ref Expression
1 simp1 AdomcardωABAAdomcard
2 difss ABA
3 ssdomg AdomcardABAABA
4 1 2 3 mpisyl AdomcardωABAABA
5 sdomdom BABA
6 5 3ad2ant3 AdomcardωABABA
7 numdom AdomcardBABdomcard
8 1 6 7 syl2anc AdomcardωABABdomcard
9 unnum AdomcardBdomcardABdomcard
10 1 8 9 syl2anc AdomcardωABAABdomcard
11 ssun1 AAB
12 ssdomg ABdomcardAABAAB
13 10 11 12 mpisyl AdomcardωABAAAB
14 undif1 ABB=AB
15 ssnum AdomcardABAABdomcard
16 1 2 15 sylancl AdomcardωABAABdomcard
17 undjudom ABdomcardBdomcardABBAB⊔︀B
18 16 8 17 syl2anc AdomcardωABAABBAB⊔︀B
19 14 18 eqbrtrrid AdomcardωABAABAB⊔︀B
20 domtr AABABAB⊔︀BAAB⊔︀B
21 13 19 20 syl2anc AdomcardωABAAAB⊔︀B
22 simp3 AdomcardωABABA
23 sdomdom ABBABB
24 relsdom Rel
25 24 brrelex2i ABBBV
26 djudom1 ABBBVAB⊔︀BB⊔︀B
27 23 25 26 syl2anc ABBAB⊔︀BB⊔︀B
28 domtr AAB⊔︀BAB⊔︀BB⊔︀BAB⊔︀B
29 28 ex AAB⊔︀BAB⊔︀BB⊔︀BAB⊔︀B
30 21 29 syl AdomcardωABAAB⊔︀BB⊔︀BAB⊔︀B
31 simp2 AdomcardωABAωA
32 domtr ωAAB⊔︀BωB⊔︀B
33 32 ex ωAAB⊔︀BωB⊔︀B
34 31 33 syl AdomcardωABAAB⊔︀BωB⊔︀B
35 djuinf ωBωB⊔︀B
36 35 biimpri ωB⊔︀BωB
37 domrefg BdomcardBB
38 infdjuabs BdomcardωBBBB⊔︀BB
39 38 3com23 BdomcardBBωBB⊔︀BB
40 39 3expia BdomcardBBωBB⊔︀BB
41 37 40 mpdan BdomcardωBB⊔︀BB
42 8 36 41 syl2im AdomcardωABAωB⊔︀BB⊔︀BB
43 34 42 syld AdomcardωABAAB⊔︀BB⊔︀BB
44 domen2 B⊔︀BBAB⊔︀BAB
45 44 biimpcd AB⊔︀BB⊔︀BBAB
46 43 45 sylcom AdomcardωABAAB⊔︀BAB
47 30 46 syld AdomcardωABAAB⊔︀BB⊔︀BAB
48 domnsym AB¬BA
49 27 47 48 syl56 AdomcardωABAABB¬BA
50 22 49 mt2d AdomcardωABA¬ABB
51 domtri2 BdomcardABdomcardBAB¬ABB
52 8 16 51 syl2anc AdomcardωABABAB¬ABB
53 50 52 mpbird AdomcardωABABAB
54 1 difexd AdomcardωABAABV
55 djudom2 BABABVAB⊔︀BAB⊔︀AB
56 53 54 55 syl2anc AdomcardωABAAB⊔︀BAB⊔︀AB
57 domtr AAB⊔︀BAB⊔︀BAB⊔︀ABAAB⊔︀AB
58 21 56 57 syl2anc AdomcardωABAAAB⊔︀AB
59 domtr ωAAAB⊔︀ABωAB⊔︀AB
60 31 58 59 syl2anc AdomcardωABAωAB⊔︀AB
61 djuinf ωABωAB⊔︀AB
62 60 61 sylibr AdomcardωABAωAB
63 domrefg ABdomcardABAB
64 16 63 syl AdomcardωABAABAB
65 infdjuabs ABdomcardωABABABAB⊔︀ABAB
66 16 62 64 65 syl3anc AdomcardωABAAB⊔︀ABAB
67 domentr AAB⊔︀ABAB⊔︀ABABAAB
68 58 66 67 syl2anc AdomcardωABAAAB
69 sbth ABAAABABA
70 4 68 69 syl2anc AdomcardωABAABA