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 
|- ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> ( A \ B ) ~~ A )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> A e. dom card )
2 difss 
 |-  ( A \ B ) C_ A
3 ssdomg 
 |-  ( A e. dom card -> ( ( A \ B ) C_ A -> ( A \ B ) ~<_ A ) )
4 1 2 3 mpisyl 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> ( A \ B ) ~<_ A )
5 sdomdom 
 |-  ( B ~< A -> B ~<_ A )
6 5 3ad2ant3 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> B ~<_ A )
7 numdom 
 |-  ( ( A e. dom card /\ B ~<_ A ) -> B e. dom card )
8 1 6 7 syl2anc 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> B e. dom card )
9 unnum 
 |-  ( ( A e. dom card /\ B e. dom card ) -> ( A u. B ) e. dom card )
10 1 8 9 syl2anc 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> ( A u. B ) e. dom card )
11 ssun1 
 |-  A C_ ( A u. B )
12 ssdomg 
 |-  ( ( A u. B ) e. dom card -> ( A C_ ( A u. B ) -> A ~<_ ( A u. B ) ) )
13 10 11 12 mpisyl 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> A ~<_ ( A u. B ) )
14 undif1 
 |-  ( ( A \ B ) u. B ) = ( A u. B )
15 ssnum 
 |-  ( ( A e. dom card /\ ( A \ B ) C_ A ) -> ( A \ B ) e. dom card )
16 1 2 15 sylancl 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> ( A \ B ) e. dom card )
17 undjudom 
 |-  ( ( ( A \ B ) e. dom card /\ B e. dom card ) -> ( ( A \ B ) u. B ) ~<_ ( ( A \ B ) |_| B ) )
18 16 8 17 syl2anc 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> ( ( A \ B ) u. B ) ~<_ ( ( A \ B ) |_| B ) )
19 14 18 eqbrtrrid 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> ( A u. B ) ~<_ ( ( A \ B ) |_| B ) )
20 domtr 
 |-  ( ( A ~<_ ( A u. B ) /\ ( A u. B ) ~<_ ( ( A \ B ) |_| B ) ) -> A ~<_ ( ( A \ B ) |_| B ) )
21 13 19 20 syl2anc 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> A ~<_ ( ( A \ B ) |_| B ) )
22 simp3 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> B ~< A )
23 sdomdom 
 |-  ( ( A \ B ) ~< B -> ( A \ B ) ~<_ B )
24 relsdom 
 |-  Rel ~<
25 24 brrelex2i 
 |-  ( ( A \ B ) ~< B -> B e. _V )
26 djudom1 
 |-  ( ( ( A \ B ) ~<_ B /\ B e. _V ) -> ( ( A \ B ) |_| B ) ~<_ ( B |_| B ) )
27 23 25 26 syl2anc 
 |-  ( ( A \ B ) ~< B -> ( ( A \ B ) |_| B ) ~<_ ( B |_| B ) )
28 domtr 
 |-  ( ( A ~<_ ( ( A \ B ) |_| B ) /\ ( ( A \ B ) |_| B ) ~<_ ( B |_| B ) ) -> A ~<_ ( B |_| B ) )
29 28 ex 
 |-  ( A ~<_ ( ( A \ B ) |_| B ) -> ( ( ( A \ B ) |_| B ) ~<_ ( B |_| B ) -> A ~<_ ( B |_| B ) ) )
30 21 29 syl 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> ( ( ( A \ B ) |_| B ) ~<_ ( B |_| B ) -> A ~<_ ( B |_| B ) ) )
31 simp2 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> _om ~<_ A )
32 domtr 
 |-  ( ( _om ~<_ A /\ A ~<_ ( B |_| B ) ) -> _om ~<_ ( B |_| B ) )
33 32 ex 
 |-  ( _om ~<_ A -> ( A ~<_ ( B |_| B ) -> _om ~<_ ( B |_| B ) ) )
34 31 33 syl 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> ( A ~<_ ( B |_| B ) -> _om ~<_ ( B |_| B ) ) )
35 djuinf 
 |-  ( _om ~<_ B <-> _om ~<_ ( B |_| B ) )
36 35 biimpri 
 |-  ( _om ~<_ ( B |_| B ) -> _om ~<_ B )
37 domrefg 
 |-  ( B e. dom card -> B ~<_ B )
38 infdjuabs 
 |-  ( ( B e. dom card /\ _om ~<_ B /\ B ~<_ B ) -> ( B |_| B ) ~~ B )
39 38 3com23 
 |-  ( ( B e. dom card /\ B ~<_ B /\ _om ~<_ B ) -> ( B |_| B ) ~~ B )
40 39 3expia 
 |-  ( ( B e. dom card /\ B ~<_ B ) -> ( _om ~<_ B -> ( B |_| B ) ~~ B ) )
41 37 40 mpdan 
 |-  ( B e. dom card -> ( _om ~<_ B -> ( B |_| B ) ~~ B ) )
42 8 36 41 syl2im 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> ( _om ~<_ ( B |_| B ) -> ( B |_| B ) ~~ B ) )
43 34 42 syld 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> ( A ~<_ ( B |_| B ) -> ( B |_| B ) ~~ B ) )
44 domen2 
 |-  ( ( B |_| B ) ~~ B -> ( A ~<_ ( B |_| B ) <-> A ~<_ B ) )
45 44 biimpcd 
 |-  ( A ~<_ ( B |_| B ) -> ( ( B |_| B ) ~~ B -> A ~<_ B ) )
46 43 45 sylcom 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> ( A ~<_ ( B |_| B ) -> A ~<_ B ) )
47 30 46 syld 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> ( ( ( A \ B ) |_| B ) ~<_ ( B |_| B ) -> A ~<_ B ) )
48 domnsym 
 |-  ( A ~<_ B -> -. B ~< A )
49 27 47 48 syl56 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> ( ( A \ B ) ~< B -> -. B ~< A ) )
50 22 49 mt2d 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> -. ( A \ B ) ~< B )
51 domtri2 
 |-  ( ( B e. dom card /\ ( A \ B ) e. dom card ) -> ( B ~<_ ( A \ B ) <-> -. ( A \ B ) ~< B ) )
52 8 16 51 syl2anc 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> ( B ~<_ ( A \ B ) <-> -. ( A \ B ) ~< B ) )
53 50 52 mpbird 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> B ~<_ ( A \ B ) )
54 difexg 
 |-  ( A e. dom card -> ( A \ B ) e. _V )
55 1 54 syl 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> ( A \ B ) e. _V )
56 djudom2 
 |-  ( ( B ~<_ ( A \ B ) /\ ( A \ B ) e. _V ) -> ( ( A \ B ) |_| B ) ~<_ ( ( A \ B ) |_| ( A \ B ) ) )
57 53 55 56 syl2anc 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> ( ( A \ B ) |_| B ) ~<_ ( ( A \ B ) |_| ( A \ B ) ) )
58 domtr 
 |-  ( ( A ~<_ ( ( A \ B ) |_| B ) /\ ( ( A \ B ) |_| B ) ~<_ ( ( A \ B ) |_| ( A \ B ) ) ) -> A ~<_ ( ( A \ B ) |_| ( A \ B ) ) )
59 21 57 58 syl2anc 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> A ~<_ ( ( A \ B ) |_| ( A \ B ) ) )
60 domtr 
 |-  ( ( _om ~<_ A /\ A ~<_ ( ( A \ B ) |_| ( A \ B ) ) ) -> _om ~<_ ( ( A \ B ) |_| ( A \ B ) ) )
61 31 59 60 syl2anc 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> _om ~<_ ( ( A \ B ) |_| ( A \ B ) ) )
62 djuinf 
 |-  ( _om ~<_ ( A \ B ) <-> _om ~<_ ( ( A \ B ) |_| ( A \ B ) ) )
63 61 62 sylibr 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> _om ~<_ ( A \ B ) )
64 domrefg 
 |-  ( ( A \ B ) e. dom card -> ( A \ B ) ~<_ ( A \ B ) )
65 16 64 syl 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> ( A \ B ) ~<_ ( A \ B ) )
66 infdjuabs 
 |-  ( ( ( A \ B ) e. dom card /\ _om ~<_ ( A \ B ) /\ ( A \ B ) ~<_ ( A \ B ) ) -> ( ( A \ B ) |_| ( A \ B ) ) ~~ ( A \ B ) )
67 16 63 65 66 syl3anc 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> ( ( A \ B ) |_| ( A \ B ) ) ~~ ( A \ B ) )
68 domentr 
 |-  ( ( A ~<_ ( ( A \ B ) |_| ( A \ B ) ) /\ ( ( A \ B ) |_| ( A \ B ) ) ~~ ( A \ B ) ) -> A ~<_ ( A \ B ) )
69 59 67 68 syl2anc 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> A ~<_ ( A \ B ) )
70 sbth 
 |-  ( ( ( A \ B ) ~<_ A /\ A ~<_ ( A \ B ) ) -> ( A \ B ) ~~ A )
71 4 69 70 syl2anc 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~< A ) -> ( A \ B ) ~~ A )