Theorem infdif 4948

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		domtr 3320	. . . . . . 7 |- ((om ~<_ A /\ A ~<_ ((A \ B) +c (A \ B))) -> om ~<_ ((A \ B) +c (A \ B)))
2		infunabs.1	. . . . . . . . 9 |- A e. V
3		difexg 1703	. . . . . . . . 9 |- (A e. V -> (A \ B) e. V)
4	2, 3	ax-mp 6	. . . . . . . 8 |- (A \ B) e. V
5	4	cdainf 3731	. . . . . . 7 |- (om ~<_ (A \ B) <-> om ~<_ ((A \ B) +c (A \ B)))
6	1, 5	sylibr 175	. . . . . 6 |- ((om ~<_ A /\ A ~<_ ((A \ B) +c (A \ B))) -> om ~<_ (A \ B))
7		domrefg 3297	. . . . . . . 8 |- ((A \ B) e. V -> (A \ B) ~<_ (A \ B))
8	4, 7	ax-mp 6	. . . . . . 7 |- (A \ B) ~<_ (A \ B)
9	4, 4	infcdaabs 4947	. . . . . . 7 |- ((om ~<_ (A \ B) /\ (A \ B) ~<_ (A \ B)) -> ((A \ B) +c (A \ B)) ~~ (A \ B))
10	8, 9	mpan2 519	. . . . . 6 |- (om ~<_ (A \ B) -> ((A \ B) +c (A \ B)) ~~ (A \ B))
11	6, 10	syl 12	. . . . 5 |- ((om ~<_ A /\ A ~<_ ((A \ B) +c (A \ B))) -> ((A \ B) +c (A \ B)) ~~ (A \ B))
12		domentr 3326	. . . . . . 7 |- ((A ~<_ ((A \ B) +c (A \ B)) /\ ((A \ B) +c (A \ B)) ~~ (A \ B)) -> A ~<_ (A \ B))
13	12	exp 291	. . . . . 6 |- (A ~<_ ((A \ B) +c (A \ B)) -> (((A \ B) +c (A \ B)) ~~ (A \ B) -> A ~<_ (A \ B)))
14	13	adantl 305	. . . . 5 |- ((om ~<_ A /\ A ~<_ ((A \ B) +c (A \ B))) -> (((A \ B) +c (A \ B)) ~~ (A \ B) -> A ~<_ (A \ B)))
15	11, 14	mpd 46	. . . 4 |- ((om ~<_ A /\ A ~<_ ((A \ B) +c (A \ B))) -> A ~<_ (A \ B))
16		pm3.26 256	. . . 4 |- ((om ~<_ A /\ B ~< A) -> om ~<_ A)
17		endomtr 3325	. . . . 5 |- ((A ~~ (A u. B) /\ (A u. B) ~<_ ((A \ B) +c (A \ B))) -> A ~<_ ((A \ B) +c (A \ B)))
18		infunabs.2	. . . . . . . 8 |- B e. V
19	2, 18	infunabs 4946	. . . . . . 7 |- ((om ~<_ A /\ B ~<_ A) -> (A u. B) ~~ A)
20	2	ensym 3317	. . . . . . 7 |- ((A u. B) ~~ A -> A ~~ (A u. B))
21	19, 20	syl 12	. . . . . 6 |- ((om ~<_ A /\ B ~<_ A) -> A ~~ (A u. B))
22		sdomdom 3290	. . . . . 6 |- (B ~< A -> B ~<_ A)
23	21, 22	sylan2 346	. . . . 5 |- ((om ~<_ A /\ B ~< A) -> A ~~ (A u. B))
24		omex 3475	. . . . . . . . 9 |- om e. V
25		entri2 3646	. . . . . . . . 9 |- ((om e. V /\ B e. V) -> (om ~<_ B \/ B ~< om))
26	24, 18, 25	mp2an 520	. . . . . . . 8 |- (om ~<_ B \/ B ~< om)
27		ssun1 1621	. . . . . . . . . . . . . 14 |- A (_ (A u. B)
28		ssdomg 3311	. . . . . . . . . . . . . 14 |- (A e. V -> (A (_ (A u. B) -> A ~<_ (A u. B)))
29	2, 27, 28	mp2 43	. . . . . . . . . . . . 13 |- A ~<_ (A u. B)
30	2, 18	unex 1949	. . . . . . . . . . . . . 14 |- (A u. B) e. V
31		domtri 3644	. . . . . . . . . . . . . 14 |- ((A e. V /\ (A u. B) e. V) -> (A ~<_ (A u. B) <-> -. (A u. B) ~< A))
32	2, 30, 31	mp2an 520	. . . . . . . . . . . . 13 |- (A ~<_ (A u. B) <-> -. (A u. B) ~< A)
33	29, 32	mpbi 164	. . . . . . . . . . . 12 |- -. (A u. B) ~< A
34		domsdomtr 3374	. . . . . . . . . . . . . . 15 |- (((A u. B) ~<_ (B +c B) /\ (B +c B) ~< A) -> (A u. B) ~< A)
35	4, 18, 18	cdadom1 3727	. . . . . . . . . . . . . . . . 17 |- ((A \ B) ~<_ B -> ((A \ B) +c B) ~<_ (B +c B))
36	4, 18	uncdadom 3718	. . . . . . . . . . . . . . . . . 18 |- ((A \ B) u. B) ~<_ ((A \ B) +c B)
37		domtr 3320	. . . . . . . . . . . . . . . . . 18 |- ((((A \ B) u. B) ~<_ ((A \ B) +c B) /\ ((A \ B) +c B) ~<_ (B +c B)) -> ((A \ B) u. B) ~<_ (B +c B))
38	36, 37	mpan 518	. . . . . . . . . . . . . . . . 17 |- (((A \ B) +c B) ~<_ (B +c B) -> ((A \ B) u. B) ~<_ (B +c B))
39	35, 38	syl 12	. . . . . . . . . . . . . . . 16 |- ((A \ B) ~<_ B -> ((A \ B) u. B) ~<_ (B +c B))
40		undif1 1761	. . . . . . . . . . . . . . . 16 |- ((A \ B) u. B) = (A u. B)
41	39, 40	syl5eqbrr 2090	. . . . . . . . . . . . . . 15 |- ((A \ B) ~<_ B -> (A u. B) ~<_ (B +c B))
42		ensdomtr 3372	. . . . . . . . . . . . . . . . 17 |- (((B +c B) ~~ B /\ B ~< A) -> (B +c B) ~< A)
43		domrefg 3297	. . . . . . . . . . . . . . . . . . 19 |- (B e. V -> B ~<_ B)
44	18, 43	ax-mp 6	. . . . . . . . . . . . . . . . . 18 |- B ~<_ B
45	18, 18	infcdaabs 4947	. . . . . . . . . . . . . . . . . 18 |- ((om ~<_ B /\ B ~<_ B) -> (B +c B) ~~ B)
46	44, 45	mpan2 519	. . . . . . . . . . . . . . . . 17 |- (om ~<_ B -> (B +c B) ~~ B)
47	42, 46	sylan 343	. . . . . . . . . . . . . . . 16 |- ((om ~<_ B /\ B ~< A) -> (B +c B) ~< A)
48	47	ancoms 334	. . . . . . . . . . . . . . 15 |- ((B ~< A /\ om ~<_ B) -> (B +c B) ~< A)
49	34, 41, 48	syl2an 349	. . . . . . . . . . . . . 14 |- (((A \ B) ~<_ B /\ (B ~< A /\ om ~<_ B)) -> (A u. B) ~< A)
50	49	ancoms 334	. . . . . . . . . . . . 13 |- (((B ~< A /\ om ~<_ B) /\ (A \ B) ~<_ B) -> (A u. B) ~< A)
51	50	exp 291	. . . . . . . . . . . 12 |- ((B ~< A /\ om ~<_ B) -> ((A \ B) ~<_ B -> (A u. B) ~< A))
52	33, 51	mtoi 94	. . . . . . . . . . 11 |- ((B ~< A /\ om ~<_ B) -> -. (A \ B) ~<_ B)
53	52	exp 291	. . . . . . . . . 10 |- (B ~< A -> (om ~<_ B -> -. (A \ B) ~<_ B))
54	53	adantl 305	. . . . . . . . 9 |- ((om ~<_ A /\ B ~< A) -> (om ~<_ B -> -. (A \ B) ~<_ B))
55	16	adantr 306	. . . . . . . . . . 11 |- (((om ~<_ A /\ B ~< A) /\ B ~< om) -> om ~<_ A)
56		domsdomtr 3374	. . . . . . . . . . . . . . . 16 |- ((A ~<_ (B +c B) /\ (B +c B) ~< om) -> A ~< om)
57		endomtr 3325	. . . . . . . . . . . . . . . . 17 |- ((A ~~ (A u. B) /\ (A u. B) ~<_ (B +c B)) -> A ~<_ (B +c B))
58	57, 23, 41	syl2an 349	. . . . . . . . . . . . . . . 16 |- (((om ~<_ A /\ B ~< A) /\ (A \ B) ~<_ B) -> A ~<_ (B +c B))
59		cdafi 3730	. . . . . . . . . . . . . . . . 17 |- ((B ~< om /\ B ~< om) -> (B +c B) ~< om)
60	59	anidms 332	. . . . . . . . . . . . . . . 16 |- (B ~< om -> (B +c B) ~< om)
61	56, 58, 60	syl2an 349	. . . . . . . . . . . . . . 15 |- ((((om ~<_ A /\ B ~< A) /\ (A \ B) ~<_ B) /\ B ~< om) -> A ~< om)
62	61	an1rs 373	. . . . . . . . . . . . . 14 |- ((((om ~<_ A /\ B ~< A) /\ B ~< om) /\ (A \ B) ~<_ B) -> A ~< om)
63	62	exp 291	. . . . . . . . . . . . 13 |- (((om ~<_ A /\ B ~< A) /\ B ~< om) -> ((A \ B) ~<_ B -> A ~< om))
64	63	con3d 87	. . . . . . . . . . . 12 |- (((om ~<_ A /\ B ~< A) /\ B ~< om) -> (-. A ~< om -> -. (A \ B) ~<_ B))
65		domtri 3644	. . . . . . . . . . . . 13 |- ((om e. V /\ A e. V) -> (om ~<_ A <-> -. A ~< om))
66	24, 2, 65	mp2an 520	. . . . . . . . . . . 12 |- (om ~<_ A <-> -. A ~< om)
67	64, 66	syl5ib 181	. . . . . . . . . . 11 |- (((om ~<_ A /\ B ~< A) /\ B ~< om) -> (om ~<_ A -> -. (A \ B) ~<_ B))
68	55, 67	mpd 46	. . . . . . . . . 10 |- (((om ~<_ A /\ B ~< A) /\ B ~< om) -> -. (A \ B) ~<_ B)
69	68	exp 291	. . . . . . . . 9 |- ((om ~<_ A /\ B ~< A) -> (B ~< om -> -. (A \ B) ~<_ B))
70	54, 69	jaod 329	. . . . . . . 8 |- ((om ~<_ A /\ B ~< A) -> ((om ~<_ B \/ B ~< om) -> -. (A \ B) ~<_ B))
71	26, 70	mpi 44	. . . . . . 7 |- ((om ~<_ A /\ B ~< A) -> -. (A \ B) ~<_ B)
72		domtri 3644	. . . . . . . . 9 |- (((A \ B) e. V /\ B e. V) -> ((A \ B) ~<_ B <-> -. B ~< (A \ B)))
73	4, 18, 72	mp2an 520	. . . . . . . 8 |- ((A \ B) ~<_ B <-> -. B ~< (A \ B))
74	73	bicon2i 194	. . . . . . 7 |- (B ~< (A \ B) <-> -. (A \ B) ~<_ B)
75	71, 74	sylibr 175	. . . . . 6 |- ((om ~<_ A /\ B ~< A) -> B ~< (A \ B))
76		sdomdom 3290	. . . . . 6 |- (B ~< (A \ B) -> B ~<_ (A \ B))
77	18, 4, 4	cdadom2 3728	. . . . . . 7 |- (B ~<_ (A \ B) -> ((A \ B) +c B) ~<_ ((A \ B) +c (A \ B)))
78	40, 36	eqbrtrr 2078	. . . . . . . 8 |- (A u. B) ~<_ ((A \ B) +c B)
79		domtr 3320	. . . . . . . 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)