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	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to (A ∖ B) \approx A$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to A \in dom card$
2		difss	$⊢ A ∖ B \subseteq A$
3		ssdomg	$⊢ A \in dom card \to (A ∖ B \subseteq A \to (A ∖ B) ≼ A)$
4	1 2 3	mpisyl	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to (A ∖ B) ≼ A$
5		sdomdom	$⊢ B ≺ A \to B ≼ A$
6	5	3ad2ant3	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to B ≼ A$
7		numdom	$⊢ (A \in dom card \land B ≼ A) \to B \in dom card$
8	1 6 7	syl2anc	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to B \in dom card$
9		unnum	$⊢ (A \in dom card \land B \in dom card) \to A \cup B \in dom card$
10	1 8 9	syl2anc	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to A \cup B \in dom card$
11		ssun1	$⊢ A \subseteq A \cup B$
12		ssdomg	$⊢ A \cup B \in dom card \to (A \subseteq A \cup B \to A ≼ (A \cup B))$
13	10 11 12	mpisyl	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to A ≼ (A \cup B)$
14		undif1	$⊢ (A ∖ B) \cup B = A \cup B$
15		ssnum	$⊢ (A \in dom card \land A ∖ B \subseteq A) \to A ∖ B \in dom card$
16	1 2 15	sylancl	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to A ∖ B \in dom card$
17		undjudom	$⊢ (A ∖ B \in dom card \land B \in dom card) \to ((A ∖ B) \cup B) ≼ ((A ∖ B) ⊔︀ B)$
18	16 8 17	syl2anc	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to ((A ∖ B) \cup B) ≼ ((A ∖ B) ⊔︀ B)$
19	14 18	eqbrtrrid	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to (A \cup B) ≼ ((A ∖ B) ⊔︀ B)$
20		domtr	$⊢ (A ≼ (A \cup B) \land (A \cup B) ≼ ((A ∖ B) ⊔︀ B)) \to A ≼ ((A ∖ B) ⊔︀ B)$
21	13 19 20	syl2anc	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to A ≼ ((A ∖ B) ⊔︀ B)$
22		simp3	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to B ≺ A$
23		sdomdom	$⊢ (A ∖ B) ≺ B \to (A ∖ B) ≼ B$
24		relsdom	$⊢ Rel ≺$
25	24	brrelex2i	$⊢ (A ∖ B) ≺ B \to B \in V$
26		djudom1	$⊢ ((A ∖ B) ≼ B \land B \in V) \to ((A ∖ B) ⊔︀ B) ≼ (B ⊔︀ B)$
27	23 25 26	syl2anc	$⊢ (A ∖ B) ≺ B \to ((A ∖ B) ⊔︀ B) ≼ (B ⊔︀ B)$
28		domtr	$⊢ (A ≼ ((A ∖ B) ⊔︀ B) \land ((A ∖ B) ⊔︀ B) ≼ (B ⊔︀ B)) \to A ≼ (B ⊔︀ B)$
29	28	ex	$⊢ A ≼ ((A ∖ B) ⊔︀ B) \to (((A ∖ B) ⊔︀ B) ≼ (B ⊔︀ B) \to A ≼ (B ⊔︀ B))$
30	21 29	syl	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to (((A ∖ B) ⊔︀ B) ≼ (B ⊔︀ B) \to A ≼ (B ⊔︀ B))$
31		simp2	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to ω ≼ A$
32		domtr	$⊢ (ω ≼ A \land A ≼ (B ⊔︀ B)) \to ω ≼ (B ⊔︀ B)$
33	32	ex	$⊢ ω ≼ A \to (A ≼ (B ⊔︀ B) \to ω ≼ (B ⊔︀ B))$
34	31 33	syl	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to (A ≼ (B ⊔︀ B) \to ω ≼ (B ⊔︀ B))$
35		djuinf	$⊢ ω ≼ B \leftrightarrow ω ≼ (B ⊔︀ B)$
36	35	biimpri	$⊢ ω ≼ (B ⊔︀ B) \to ω ≼ B$
37		domrefg	$⊢ B \in dom card \to B ≼ B$
38		infdjuabs	$⊢ (B \in dom card \land ω ≼ B \land B ≼ B) \to (B ⊔︀ B) \approx B$
39	38	3com23	$⊢ (B \in dom card \land B ≼ B \land ω ≼ B) \to (B ⊔︀ B) \approx B$
40	39	3expia	$⊢ (B \in dom card \land B ≼ B) \to (ω ≼ B \to (B ⊔︀ B) \approx B)$
41	37 40	mpdan	$⊢ B \in dom card \to (ω ≼ B \to (B ⊔︀ B) \approx B)$
42	8 36 41	syl2im	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to (ω ≼ (B ⊔︀ B) \to (B ⊔︀ B) \approx B)$
43	34 42	syld	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to (A ≼ (B ⊔︀ B) \to (B ⊔︀ B) \approx B)$
44		domen2	$⊢ (B ⊔︀ B) \approx B \to (A ≼ (B ⊔︀ B) \leftrightarrow A ≼ B)$
45	44	biimpcd	$⊢ A ≼ (B ⊔︀ B) \to ((B ⊔︀ B) \approx B \to A ≼ B)$
46	43 45	sylcom	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to (A ≼ (B ⊔︀ B) \to A ≼ B)$
47	30 46	syld	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to (((A ∖ B) ⊔︀ B) ≼ (B ⊔︀ B) \to A ≼ B)$
48		domnsym	$⊢ A ≼ B \to \neg B ≺ A$
49	27 47 48	syl56	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to ((A ∖ B) ≺ B \to \neg B ≺ A)$
50	22 49	mt2d	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to \neg (A ∖ B) ≺ B$
51		domtri2	$⊢ (B \in dom card \land A ∖ B \in dom card) \to (B ≼ (A ∖ B) \leftrightarrow \neg (A ∖ B) ≺ B)$
52	8 16 51	syl2anc	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to (B ≼ (A ∖ B) \leftrightarrow \neg (A ∖ B) ≺ B)$
53	50 52	mpbird	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to B ≼ (A ∖ B)$
54	1	difexd	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to A ∖ B \in V$
55		djudom2	$⊢ (B ≼ (A ∖ B) \land A ∖ B \in V) \to ((A ∖ B) ⊔︀ B) ≼ ((A ∖ B) ⊔︀ (A ∖ B))$
56	53 54 55	syl2anc	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to ((A ∖ B) ⊔︀ B) ≼ ((A ∖ B) ⊔︀ (A ∖ B))$
57		domtr	$⊢ (A ≼ ((A ∖ B) ⊔︀ B) \land ((A ∖ B) ⊔︀ B) ≼ ((A ∖ B) ⊔︀ (A ∖ B))) \to A ≼ ((A ∖ B) ⊔︀ (A ∖ B))$
58	21 56 57	syl2anc	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to A ≼ ((A ∖ B) ⊔︀ (A ∖ B))$
59		domtr	$⊢ (ω ≼ A \land A ≼ ((A ∖ B) ⊔︀ (A ∖ B))) \to ω ≼ ((A ∖ B) ⊔︀ (A ∖ B))$
60	31 58 59	syl2anc	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to ω ≼ ((A ∖ B) ⊔︀ (A ∖ B))$
61		djuinf	$⊢ ω ≼ (A ∖ B) \leftrightarrow ω ≼ ((A ∖ B) ⊔︀ (A ∖ B))$
62	60 61	sylibr	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to ω ≼ (A ∖ B)$
63		domrefg	$⊢ A ∖ B \in dom card \to (A ∖ B) ≼ (A ∖ B)$
64	16 63	syl	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to (A ∖ B) ≼ (A ∖ B)$
65		infdjuabs	$⊢ (A ∖ B \in dom card \land ω ≼ (A ∖ B) \land (A ∖ B) ≼ (A ∖ B)) \to ((A ∖ B) ⊔︀ (A ∖ B)) \approx (A ∖ B)$
66	16 62 64 65	syl3anc	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to ((A ∖ B) ⊔︀ (A ∖ B)) \approx (A ∖ B)$
67		domentr	$⊢ (A ≼ ((A ∖ B) ⊔︀ (A ∖ B)) \land ((A ∖ B) ⊔︀ (A ∖ B)) \approx (A ∖ B)) \to A ≼ (A ∖ B)$
68	58 66 67	syl2anc	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to A ≼ (A ∖ B)$
69		sbth	$⊢ ((A ∖ B) ≼ A \land A ≼ (A ∖ B)) \to (A ∖ B) \approx A$
70	4 68 69	syl2anc	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to (A ∖ B) \approx A$

Metamath Proof Explorer

Theorem infdif

Proof