Metamath Proof Explorer

Theorem infdifsn

Description: Removing a singleton from an infinite set does not change the cardinality of the set. (Contributed by Mario Carneiro, 30-Apr-2015) (Revised by Mario Carneiro, 16-May-2015)

Ref Expression
Assertion infdifsn 
|- ( _om ~<_ A -> ( A \ { B } ) ~~ A )

Proof

Step Hyp Ref Expression
1 brdomi 
 |-  ( _om ~<_ A -> E. f f : _om -1-1-> A )
2 1 adantr 
 |-  ( ( _om ~<_ A /\ B e. A ) -> E. f f : _om -1-1-> A )
3 reldom 
 |-  Rel ~<_
4 3 brrelex2i 
 |-  ( _om ~<_ A -> A e. _V )
5 4 ad2antrr 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> A e. _V )
6 simplr 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> B e. A )
7 f1f 
 |-  ( f : _om -1-1-> A -> f : _om --> A )
8 7 adantl 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> f : _om --> A )
9 peano1 
 |-  (/) e. _om
10 ffvelrn 
 |-  ( ( f : _om --> A /\ (/) e. _om ) -> ( f ` (/) ) e. A )
11 8 9 10 sylancl 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> ( f ` (/) ) e. A )
12 difsnen 
 |-  ( ( A e. _V /\ B e. A /\ ( f ` (/) ) e. A ) -> ( A \ { B } ) ~~ ( A \ { ( f ` (/) ) } ) )
13 5 6 11 12 syl3anc 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> ( A \ { B } ) ~~ ( A \ { ( f ` (/) ) } ) )
14 vex 
 |-  f e. _V
15 f1f1orn 
 |-  ( f : _om -1-1-> A -> f : _om -1-1-onto-> ran f )
16 15 adantl 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> f : _om -1-1-onto-> ran f )
17 f1oen3g 
 |-  ( ( f e. _V /\ f : _om -1-1-onto-> ran f ) -> _om ~~ ran f )
18 14 16 17 sylancr 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> _om ~~ ran f )
19 18 ensymd 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> ran f ~~ _om )
20 3 brrelex1i 
 |-  ( _om ~<_ A -> _om e. _V )
21 20 ad2antrr 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> _om e. _V )
22 limom 
 |-  Lim _om
23 22 limenpsi 
 |-  ( _om e. _V -> _om ~~ ( _om \ { (/) } ) )
24 21 23 syl 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> _om ~~ ( _om \ { (/) } ) )
25 14 resex 
 |-  ( f |` ( _om \ { (/) } ) ) e. _V
26 simpr 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> f : _om -1-1-> A )
27 difss 
 |-  ( _om \ { (/) } ) C_ _om
28 f1ores 
 |-  ( ( f : _om -1-1-> A /\ ( _om \ { (/) } ) C_ _om ) -> ( f |` ( _om \ { (/) } ) ) : ( _om \ { (/) } ) -1-1-onto-> ( f " ( _om \ { (/) } ) ) )
29 26 27 28 sylancl 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> ( f |` ( _om \ { (/) } ) ) : ( _om \ { (/) } ) -1-1-onto-> ( f " ( _om \ { (/) } ) ) )
30 f1oen3g 
 |-  ( ( ( f |` ( _om \ { (/) } ) ) e. _V /\ ( f |` ( _om \ { (/) } ) ) : ( _om \ { (/) } ) -1-1-onto-> ( f " ( _om \ { (/) } ) ) ) -> ( _om \ { (/) } ) ~~ ( f " ( _om \ { (/) } ) ) )
31 25 29 30 sylancr 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> ( _om \ { (/) } ) ~~ ( f " ( _om \ { (/) } ) ) )
32 f1orn 
 |-  ( f : _om -1-1-onto-> ran f <-> ( f Fn _om /\ Fun `' f ) )
33 32 simprbi 
 |-  ( f : _om -1-1-onto-> ran f -> Fun `' f )
34 imadif 
 |-  ( Fun `' f -> ( f " ( _om \ { (/) } ) ) = ( ( f " _om ) \ ( f " { (/) } ) ) )
35 16 33 34 3syl 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> ( f " ( _om \ { (/) } ) ) = ( ( f " _om ) \ ( f " { (/) } ) ) )
36 f1fn 
 |-  ( f : _om -1-1-> A -> f Fn _om )
37 36 adantl 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> f Fn _om )
38 fnima 
 |-  ( f Fn _om -> ( f " _om ) = ran f )
39 37 38 syl 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> ( f " _om ) = ran f )
40 fnsnfv 
 |-  ( ( f Fn _om /\ (/) e. _om ) -> { ( f ` (/) ) } = ( f " { (/) } ) )
41 37 9 40 sylancl 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> { ( f ` (/) ) } = ( f " { (/) } ) )
42 41 eqcomd 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> ( f " { (/) } ) = { ( f ` (/) ) } )
43 39 42 difeq12d 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> ( ( f " _om ) \ ( f " { (/) } ) ) = ( ran f \ { ( f ` (/) ) } ) )
44 35 43 eqtrd 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> ( f " ( _om \ { (/) } ) ) = ( ran f \ { ( f ` (/) ) } ) )
45 31 44 breqtrd 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> ( _om \ { (/) } ) ~~ ( ran f \ { ( f ` (/) ) } ) )
46 entr 
 |-  ( ( _om ~~ ( _om \ { (/) } ) /\ ( _om \ { (/) } ) ~~ ( ran f \ { ( f ` (/) ) } ) ) -> _om ~~ ( ran f \ { ( f ` (/) ) } ) )
47 24 45 46 syl2anc 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> _om ~~ ( ran f \ { ( f ` (/) ) } ) )
48 entr 
 |-  ( ( ran f ~~ _om /\ _om ~~ ( ran f \ { ( f ` (/) ) } ) ) -> ran f ~~ ( ran f \ { ( f ` (/) ) } ) )
49 19 47 48 syl2anc 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> ran f ~~ ( ran f \ { ( f ` (/) ) } ) )
50 difexg 
 |-  ( A e. _V -> ( A \ ran f ) e. _V )
51 enrefg 
 |-  ( ( A \ ran f ) e. _V -> ( A \ ran f ) ~~ ( A \ ran f ) )
52 5 50 51 3syl 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> ( A \ ran f ) ~~ ( A \ ran f ) )
53 disjdif 
 |-  ( ran f i^i ( A \ ran f ) ) = (/)
54 53 a1i 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> ( ran f i^i ( A \ ran f ) ) = (/) )
55 difss 
 |-  ( ran f \ { ( f ` (/) ) } ) C_ ran f
56 ssrin 
 |-  ( ( ran f \ { ( f ` (/) ) } ) C_ ran f -> ( ( ran f \ { ( f ` (/) ) } ) i^i ( A \ ran f ) ) C_ ( ran f i^i ( A \ ran f ) ) )
57 55 56 ax-mp 
 |-  ( ( ran f \ { ( f ` (/) ) } ) i^i ( A \ ran f ) ) C_ ( ran f i^i ( A \ ran f ) )
58 sseq0 
 |-  ( ( ( ( ran f \ { ( f ` (/) ) } ) i^i ( A \ ran f ) ) C_ ( ran f i^i ( A \ ran f ) ) /\ ( ran f i^i ( A \ ran f ) ) = (/) ) -> ( ( ran f \ { ( f ` (/) ) } ) i^i ( A \ ran f ) ) = (/) )
59 57 53 58 mp2an 
 |-  ( ( ran f \ { ( f ` (/) ) } ) i^i ( A \ ran f ) ) = (/)
60 59 a1i 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> ( ( ran f \ { ( f ` (/) ) } ) i^i ( A \ ran f ) ) = (/) )
61 unen 
 |-  ( ( ( ran f ~~ ( ran f \ { ( f ` (/) ) } ) /\ ( A \ ran f ) ~~ ( A \ ran f ) ) /\ ( ( ran f i^i ( A \ ran f ) ) = (/) /\ ( ( ran f \ { ( f ` (/) ) } ) i^i ( A \ ran f ) ) = (/) ) ) -> ( ran f u. ( A \ ran f ) ) ~~ ( ( ran f \ { ( f ` (/) ) } ) u. ( A \ ran f ) ) )
62 49 52 54 60 61 syl22anc 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> ( ran f u. ( A \ ran f ) ) ~~ ( ( ran f \ { ( f ` (/) ) } ) u. ( A \ ran f ) ) )
63 8 frnd 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> ran f C_ A )
64 undif 
 |-  ( ran f C_ A <-> ( ran f u. ( A \ ran f ) ) = A )
65 63 64 sylib 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> ( ran f u. ( A \ ran f ) ) = A )
66 uncom 
 |-  ( ( ran f \ { ( f ` (/) ) } ) u. ( A \ ran f ) ) = ( ( A \ ran f ) u. ( ran f \ { ( f ` (/) ) } ) )
67 eldifn 
 |-  ( ( f ` (/) ) e. ( A \ ran f ) -> -. ( f ` (/) ) e. ran f )
68 fnfvelrn 
 |-  ( ( f Fn _om /\ (/) e. _om ) -> ( f ` (/) ) e. ran f )
69 37 9 68 sylancl 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> ( f ` (/) ) e. ran f )
70 67 69 nsyl3 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> -. ( f ` (/) ) e. ( A \ ran f ) )
71 disjsn 
 |-  ( ( ( A \ ran f ) i^i { ( f ` (/) ) } ) = (/) <-> -. ( f ` (/) ) e. ( A \ ran f ) )
72 70 71 sylibr 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> ( ( A \ ran f ) i^i { ( f ` (/) ) } ) = (/) )
73 undif4 
 |-  ( ( ( A \ ran f ) i^i { ( f ` (/) ) } ) = (/) -> ( ( A \ ran f ) u. ( ran f \ { ( f ` (/) ) } ) ) = ( ( ( A \ ran f ) u. ran f ) \ { ( f ` (/) ) } ) )
74 72 73 syl 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> ( ( A \ ran f ) u. ( ran f \ { ( f ` (/) ) } ) ) = ( ( ( A \ ran f ) u. ran f ) \ { ( f ` (/) ) } ) )
75 uncom 
 |-  ( ( A \ ran f ) u. ran f ) = ( ran f u. ( A \ ran f ) )
76 75 65 syl5eq 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> ( ( A \ ran f ) u. ran f ) = A )
77 76 difeq1d 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> ( ( ( A \ ran f ) u. ran f ) \ { ( f ` (/) ) } ) = ( A \ { ( f ` (/) ) } ) )
78 74 77 eqtrd 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> ( ( A \ ran f ) u. ( ran f \ { ( f ` (/) ) } ) ) = ( A \ { ( f ` (/) ) } ) )
79 66 78 syl5eq 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> ( ( ran f \ { ( f ` (/) ) } ) u. ( A \ ran f ) ) = ( A \ { ( f ` (/) ) } ) )
80 62 65 79 3brtr3d 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> A ~~ ( A \ { ( f ` (/) ) } ) )
81 80 ensymd 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> ( A \ { ( f ` (/) ) } ) ~~ A )
82 entr 
 |-  ( ( ( A \ { B } ) ~~ ( A \ { ( f ` (/) ) } ) /\ ( A \ { ( f ` (/) ) } ) ~~ A ) -> ( A \ { B } ) ~~ A )
83 13 81 82 syl2anc 
 |-  ( ( ( _om ~<_ A /\ B e. A ) /\ f : _om -1-1-> A ) -> ( A \ { B } ) ~~ A )
84 2 83 exlimddv 
 |-  ( ( _om ~<_ A /\ B e. A ) -> ( A \ { B } ) ~~ A )
85 difsn 
 |-  ( -. B e. A -> ( A \ { B } ) = A )
86 85 adantl 
 |-  ( ( _om ~<_ A /\ -. B e. A ) -> ( A \ { B } ) = A )
87 enrefg 
 |-  ( A e. _V -> A ~~ A )
88 4 87 syl 
 |-  ( _om ~<_ A -> A ~~ A )
89 88 adantr 
 |-  ( ( _om ~<_ A /\ -. B e. A ) -> A ~~ A )
90 86 89 eqbrtrd 
 |-  ( ( _om ~<_ A /\ -. B e. A ) -> ( A \ { B } ) ~~ A )
91 84 90 pm2.61dan 
 |-  ( _om ~<_ A -> ( A \ { B } ) ~~ A )