Theorem infdif 7519

Description: The cardinality of an infinite set does not change after subtracting a strictly smaller one. Example in [Enderton] p. 164.

Hypotheses

Ref	Expression
infunabs.1	|- A e. V
infunabs.2	|- B e. V

Assertion

Ref	Expression
infdif	|- ((om ~<_ A /\ B ~< A) -> (A \ B) ~~ A)

Proof of Theorem infdif

Step	Hyp	Ref	Expression
1		endomtr 4407	. . . . 5 |- ((A ~~ (A u. B) /\ (A u. B) ~<_ ((A \ B) +c (A \ B))) -> A ~<_ ((A \ B) +c (A \ B)))
2		infunabs.1	. . . . . . . 8 |- A e. V
3		infunabs.2	. . . . . . . 8 |- B e. V
4	2, 3	infunabs 7516	. . . . . . 7 |- ((om ~<_ A /\ B ~<_ A) -> (A u. B) ~~ A)
5	2	ensym 4399	. . . . . . 7 |- ((A u. B) ~~ A -> A ~~ (A u. B))
6	4, 5	syl 10	. . . . . 6 |- ((om ~<_ A /\ B ~<_ A) -> A ~~ (A u. B))
7		sdomdom 4373	. . . . . 6 |- (B ~< A -> B ~<_ A)
8	6, 7	sylan2 451	. . . . 5 |- ((om ~<_ A /\ B ~< A) -> A ~~ (A u. B))
9		omex 4607	. . . . . . . . 9 |- om e. V
10		entri2 4820	. . . . . . . . 9 |- ((om e. V /\ B e. V) -> (om ~<_ B \/ B ~< om))
11	9, 3, 10	mp2an 696	. . . . . . . 8 |- (om ~<_ B \/ B ~< om)
12		ssun1 2189	. . . . . . . . . . . . . 14 |- A (_ (A u. B)
13		ssdomg 4395	. . . . . . . . . . . . . 14 |- (A e. V -> (A (_ (A u. B) -> A ~<_ (A u. B)))
14	2, 12, 13	mp2 43	. . . . . . . . . . . . 13 |- A ~<_ (A u. B)
15	2, 3	unex 2867	. . . . . . . . . . . . . 14 |- (A u. B) e. V
16		domtri 4818	. . . . . . . . . . . . . 14 |- ((A e. V /\ (A u. B) e. V) -> (A ~<_ (A u. B) <-> -. (A u. B) ~< A))
17	2, 15, 16	mp2an 696	. . . . . . . . . . . . 13 |- (A ~<_ (A u. B) <-> -. (A u. B) ~< A)
18	14, 17	mpbi 189	. . . . . . . . . . . 12 |- -. (A u. B) ~< A
19		domsdomtr 4462	. . . . . . . . . . . . . 14 |- (((A u. B) ~<_ (B +c B) /\ (B +c B) ~< A) -> (A u. B) ~< A)
20		difexg 2717	. . . . . . . . . . . . . . . . . 18 |- (A e. V -> (A \ B) e. V)
21	2, 20	ax-mp 7	. . . . . . . . . . . . . . . . 17 |- (A \ B) e. V
22	21, 3, 3	cdadom1 4913	. . . . . . . . . . . . . . . 16 |- ((A \ B) ~<_ B -> ((A \ B) +c B) ~<_ (B +c B))
23	21, 3	uncdadom 4901	. . . . . . . . . . . . . . . . 17 |- ((A \ B) u. B) ~<_ ((A \ B) +c B)
24		domtr 4402	. . . . . . . . . . . . . . . . 17 |- ((((A \ B) u. B) ~<_ ((A \ B) +c B) /\ ((A \ B) +c B) ~<_ (B +c B)) -> ((A \ B) u. B) ~<_ (B +c B))
25	23, 24	mpan 694	. . . . . . . . . . . . . . . 16 |- (((A \ B) +c B) ~<_ (B +c B) -> ((A \ B) u. B) ~<_ (B +c B))
26	22, 25	syl 10	. . . . . . . . . . . . . . 15 |- ((A \ B) ~<_ B -> ((A \ B) u. B) ~<_ (B +c B))
27		undif1 2336	. . . . . . . . . . . . . . 15 |- ((A \ B) u. B) = (A u. B)
28	26, 27	syl5eqbrr 2644	. . . . . . . . . . . . . 14 |- ((A \ B) ~<_ B -> (A u. B) ~<_ (B +c B))
29		ensdomtr 4457	. . . . . . . . . . . . . . . 16 |- (((B +c B) ~~ B /\ B ~< A) -> (B +c B) ~< A)
30		domrefg 4380	. . . . . . . . . . . . . . . . . 18 |- (B e. V -> B ~<_ B)
31	3, 30	ax-mp 7	. . . . . . . . . . . . . . . . 17 |- B ~<_ B
32	3, 3	infcdaabs 7517	. . . . . . . . . . . . . . . . 17 |- ((om ~<_ B /\ B ~<_ B) -> (B +c B) ~~ B)
33	31, 32	mpan2 695	. . . . . . . . . . . . . . . 16 |- (om ~<_ B -> (B +c B) ~~ B)
34	29, 33	sylan 448	. . . . . . . . . . . . . . 15 |- ((om ~<_ B /\ B ~< A) -> (B +c B) ~< A)
35	34	ancoms 436	. . . . . . . . . . . . . 14 |- ((B ~< A /\ om ~<_ B) -> (B +c B) ~< A)
36	19, 28, 35	syl2an 454	. . . . . . . . . . . . 13 |- (((A \ B) ~<_ B /\ (B ~< A /\ om ~<_ B)) -> (A u. B) ~< A)
37	36	expcom 374	. . . . . . . . . . . 12 |- ((B ~< A /\ om ~<_ B) -> ((A \ B) ~<_ B -> (A u. B) ~< A))
38	18, 37	mtoi 107	. . . . . . . . . . 11 |- ((B ~< A /\ om ~<_ B) -> -. (A \ B) ~<_ B)
39	38	ex 373	. . . . . . . . . 10 |- (B ~< A -> (om ~<_ B -> -. (A \ B) ~<_ B))
40	39	adantl 388	. . . . . . . . 9 |- ((om ~<_ A /\ B ~< A) -> (om ~<_ B -> -. (A \ B) ~<_ B))
41		simpll 412	. . . . . . . . . . 11 |- (((om ~<_ A /\ B ~< A) /\ B ~< om) -> om ~<_ A)
42		domsdomtr 4462	. . . . . . . . . . . . . . . 16 |- ((A ~<_ (B +c B) /\ (B +c B) ~< om) -> A ~< om)
43		endomtr 4407	. . . . . . . . . . . . . . . . 17 |- ((A ~~ (A u. B) /\ (A u. B) ~<_ (B +c B)) -> A ~<_ (B +c B))
44	43, 8, 28	syl2an 454	. . . . . . . . . . . . . . . 16 |- (((om ~<_ A /\ B ~< A) /\ (A \ B) ~<_ B) -> A ~<_ (B +c B))
45		cdafi 4916	. . . . . . . . . . . . . . . . 17 |- ((B ~< om /\ B ~< om) -> (B +c B) ~< om)
46	45	anidms 434	. . . . . . . . . . . . . . . 16 |- (B ~< om -> (B +c B) ~< om)
47	42, 44, 46	syl2an 454	. . . . . . . . . . . . . . 15 |- ((((om ~<_ A /\ B ~< A) /\ (A \ B) ~<_ B) /\ B ~< om) -> A ~< om)
48	47	an1rs 489	. . . . . . . . . . . . . 14 |- ((((om ~<_ A /\ B ~< A) /\ B ~< om) /\ (A \ B) ~<_ B) -> A ~< om)
49	48	ex 373	. . . . . . . . . . . . 13 |- (((om ~<_ A /\ B ~< A) /\ B ~< om) -> ((A \ B) ~<_ B -> A ~< om))
50	49	con3d 95	. . . . . . . . . . . 12 |- (((om ~<_ A /\ B ~< A) /\ B ~< om) -> (-. A ~< om -> -. (A \ B) ~<_ B))
51		domtri 4818	. . . . . . . . . . . . 13 |- ((om e. V /\ A e. V) -> (om ~<_ A <-> -. A ~< om))
52	9, 2, 51	mp2an 696	. . . . . . . . . . . 12 |- (om ~<_ A <-> -. A ~< om)
53	50, 52	syl5ib 206	. . . . . . . . . . 11 |- (((om ~<_ A /\ B ~< A) /\ B ~< om) -> (om ~<_ A -> -. (A \ B) ~<_ B))
54	41, 53	mpd 26	. . . . . . . . . 10 |- (((om ~<_ A /\ B ~< A) /\ B ~< om) -> -. (A \ B) ~<_ B)
55	54	ex 373	. . . . . . . . 9 |- ((om ~<_ A /\ B ~< A) -> (B ~< om -> -. (A \ B) ~<_ B))
56	40, 55	jaod 424	. . . . . . . 8 |- ((om ~<_ A /\ B ~< A) -> ((om ~<_ B \/ B ~< om) -> -. (A \ B) ~<_ B))
57	11, 56	mpi 44	. . . . . . 7 |- ((om ~<_ A /\ B ~< A) -> -. (A \ B) ~<_ B)
58		domtri 4818	. . . . . . . . 9 |- (((A \ B) e. V /\ B e. V) -> ((A \ B) ~<_ B <-> -. B ~< (A \ B)))
59	21, 3, 58	mp2an 696	. . . . . . . 8 |- ((A \ B) ~<_ B <-> -. B ~< (A \ B))
60	59	con2bii 221	. . . . . . 7 |- (B ~< (A \ B) <-> -. (A \ B) ~<_ B)
61	57, 60	sylibr 200	. . . . . 6 |- ((om ~<_ A /\ B ~< A) -> B ~< (A \ B))
62		sdomdom 4373	. . . . . 6 |- (B ~< (A \ B) -> B ~<_ (A \ B))
63	3, 21, 21	cdadom2 4914	. . . . . . 7 |- (B ~<_ (A \ B) -> ((A \ B) +c B) ~<_ ((A \ B) +c (A \ B)))
64	27, 23	eqbrtrr 2631	. . . . . . . 8 |- (A u. B) ~<_ ((A \ B) +c B)
65		domtr 4402	. . . . . . . 8 |- (((A u. B) ~<_ ((A \ B) +c B) /\ ((A \ B) +c B) ~<_ ((A \ B) +c (A \ B))) -> (A u. B) ~<_ ((A \ B) +c (A \ B)))
66	64, 65	mpan 694	. . . . . . 7 |- (((A \ B) +c B) ~<_ ((A \ B) +c (A \ B)) -> (A u. B) ~<_ ((A \ B) +c (A \ B)))
67	63, 66	syl 10	. . . . . 6 |- (B ~<_ (A \ B) -> (A u. B) ~<_ ((A \ B) +c (A \ B)))
68	61, 62, 67	3syl 20	. . . . 5 |- ((om ~<_ A /\ B ~< A) -> (A u. B) ~<_ ((A \ B) +c (A \ B)))
69	1, 8, 68	sylanc 471	. . . 4 |- ((om ~<_ A /\ B ~< A) -> A ~<_ ((A \ B) +c (A \ B)))
70		domtr 4402	. . . . . . 7 |- ((om ~<_ A /\ A ~<_ ((A \ B) +c (A \ B))) -> om ~<_ ((A \ B) +c (A \ B)))
71	21	cdainf 4917	. . . . . . 7 |- (om ~<_ (A \ B) <-> om ~<_ ((A \ B) +c (A \ B)))
72	70, 71	sylibr 200	. . . . . 6 |- ((om ~<_ A /\ A ~<_ ((A \ B) +c (A \ B))) -> om ~<_ (A \ B))
73		domrefg 4380	. . . . . . . 8 |- ((A \ B) e. V -> (A \ B) ~<_ (A \ B))
74	21, 73	ax-mp 7	. . . . . . 7 |- (A \ B) ~<_ (A \ B)
75	21, 21	infcdaabs 7517	. . . . . . 7 |- ((om ~<_ (A \ B) /\ (A \ B) ~<_ (A \ B)) -> ((A \ B) +c (A \ B)) ~~ (A \ B))
76	74, 75	mpan2 695	. . . . . 6 |- (om ~<_ (A \ B) -> ((A \ B) +c (A \ B)) ~~ (A \ B))
77	72, 76	syl 10	. . . . 5 |- ((om ~<_ A /\ A ~<_ ((A \ B) +c (A \ B))) -> ((A \ B) +c (A \ B)) ~~ (A \ B))
78		domentr 4408	. . . . . . 7 |- ((A ~<_ ((A