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 ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≺ 𝐴 ) → ( 𝐴 ∖ 𝐵 ) ≈ 𝐴 )

Proof

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