Metamath Proof Explorer


Theorem djuinf

Description: A set is infinite iff the cardinal sum with itself is infinite. (Contributed by NM, 22-Oct-2004) (Revised by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion djuinf
|- ( _om ~<_ A <-> _om ~<_ ( A |_| A ) )

Proof

Step Hyp Ref Expression
1 reldom
 |-  Rel ~<_
2 1 brrelex2i
 |-  ( _om ~<_ A -> A e. _V )
3 djudoml
 |-  ( ( A e. _V /\ A e. _V ) -> A ~<_ ( A |_| A ) )
4 2 2 3 syl2anc
 |-  ( _om ~<_ A -> A ~<_ ( A |_| A ) )
5 domtr
 |-  ( ( _om ~<_ A /\ A ~<_ ( A |_| A ) ) -> _om ~<_ ( A |_| A ) )
6 4 5 mpdan
 |-  ( _om ~<_ A -> _om ~<_ ( A |_| A ) )
7 1 brrelex2i
 |-  ( _om ~<_ ( A |_| A ) -> ( A |_| A ) e. _V )
8 anidm
 |-  ( ( A e. _V /\ A e. _V ) <-> A e. _V )
9 djuexb
 |-  ( ( A e. _V /\ A e. _V ) <-> ( A |_| A ) e. _V )
10 8 9 bitr3i
 |-  ( A e. _V <-> ( A |_| A ) e. _V )
11 7 10 sylibr
 |-  ( _om ~<_ ( A |_| A ) -> A e. _V )
12 domeng
 |-  ( ( A |_| A ) e. _V -> ( _om ~<_ ( A |_| A ) <-> E. x ( _om ~~ x /\ x C_ ( A |_| A ) ) ) )
13 7 12 syl
 |-  ( _om ~<_ ( A |_| A ) -> ( _om ~<_ ( A |_| A ) <-> E. x ( _om ~~ x /\ x C_ ( A |_| A ) ) ) )
14 13 ibi
 |-  ( _om ~<_ ( A |_| A ) -> E. x ( _om ~~ x /\ x C_ ( A |_| A ) ) )
15 indi
 |-  ( x i^i ( ( { (/) } X. A ) u. ( { 1o } X. A ) ) ) = ( ( x i^i ( { (/) } X. A ) ) u. ( x i^i ( { 1o } X. A ) ) )
16 simpr
 |-  ( ( _om ~~ x /\ x C_ ( A |_| A ) ) -> x C_ ( A |_| A ) )
17 df-dju
 |-  ( A |_| A ) = ( ( { (/) } X. A ) u. ( { 1o } X. A ) )
18 16 17 sseqtrdi
 |-  ( ( _om ~~ x /\ x C_ ( A |_| A ) ) -> x C_ ( ( { (/) } X. A ) u. ( { 1o } X. A ) ) )
19 df-ss
 |-  ( x C_ ( ( { (/) } X. A ) u. ( { 1o } X. A ) ) <-> ( x i^i ( ( { (/) } X. A ) u. ( { 1o } X. A ) ) ) = x )
20 18 19 sylib
 |-  ( ( _om ~~ x /\ x C_ ( A |_| A ) ) -> ( x i^i ( ( { (/) } X. A ) u. ( { 1o } X. A ) ) ) = x )
21 15 20 eqtr3id
 |-  ( ( _om ~~ x /\ x C_ ( A |_| A ) ) -> ( ( x i^i ( { (/) } X. A ) ) u. ( x i^i ( { 1o } X. A ) ) ) = x )
22 ensym
 |-  ( _om ~~ x -> x ~~ _om )
23 22 adantr
 |-  ( ( _om ~~ x /\ x C_ ( A |_| A ) ) -> x ~~ _om )
24 21 23 eqbrtrd
 |-  ( ( _om ~~ x /\ x C_ ( A |_| A ) ) -> ( ( x i^i ( { (/) } X. A ) ) u. ( x i^i ( { 1o } X. A ) ) ) ~~ _om )
25 cdainflem
 |-  ( ( ( x i^i ( { (/) } X. A ) ) u. ( x i^i ( { 1o } X. A ) ) ) ~~ _om -> ( ( x i^i ( { (/) } X. A ) ) ~~ _om \/ ( x i^i ( { 1o } X. A ) ) ~~ _om ) )
26 snex
 |-  { (/) } e. _V
27 xpexg
 |-  ( ( { (/) } e. _V /\ A e. _V ) -> ( { (/) } X. A ) e. _V )
28 26 27 mpan
 |-  ( A e. _V -> ( { (/) } X. A ) e. _V )
29 inss2
 |-  ( x i^i ( { (/) } X. A ) ) C_ ( { (/) } X. A )
30 ssdomg
 |-  ( ( { (/) } X. A ) e. _V -> ( ( x i^i ( { (/) } X. A ) ) C_ ( { (/) } X. A ) -> ( x i^i ( { (/) } X. A ) ) ~<_ ( { (/) } X. A ) ) )
31 28 29 30 mpisyl
 |-  ( A e. _V -> ( x i^i ( { (/) } X. A ) ) ~<_ ( { (/) } X. A ) )
32 0ex
 |-  (/) e. _V
33 xpsnen2g
 |-  ( ( (/) e. _V /\ A e. _V ) -> ( { (/) } X. A ) ~~ A )
34 32 33 mpan
 |-  ( A e. _V -> ( { (/) } X. A ) ~~ A )
35 domentr
 |-  ( ( ( x i^i ( { (/) } X. A ) ) ~<_ ( { (/) } X. A ) /\ ( { (/) } X. A ) ~~ A ) -> ( x i^i ( { (/) } X. A ) ) ~<_ A )
36 31 34 35 syl2anc
 |-  ( A e. _V -> ( x i^i ( { (/) } X. A ) ) ~<_ A )
37 domen1
 |-  ( ( x i^i ( { (/) } X. A ) ) ~~ _om -> ( ( x i^i ( { (/) } X. A ) ) ~<_ A <-> _om ~<_ A ) )
38 36 37 syl5ibcom
 |-  ( A e. _V -> ( ( x i^i ( { (/) } X. A ) ) ~~ _om -> _om ~<_ A ) )
39 snex
 |-  { 1o } e. _V
40 xpexg
 |-  ( ( { 1o } e. _V /\ A e. _V ) -> ( { 1o } X. A ) e. _V )
41 39 40 mpan
 |-  ( A e. _V -> ( { 1o } X. A ) e. _V )
42 inss2
 |-  ( x i^i ( { 1o } X. A ) ) C_ ( { 1o } X. A )
43 ssdomg
 |-  ( ( { 1o } X. A ) e. _V -> ( ( x i^i ( { 1o } X. A ) ) C_ ( { 1o } X. A ) -> ( x i^i ( { 1o } X. A ) ) ~<_ ( { 1o } X. A ) ) )
44 41 42 43 mpisyl
 |-  ( A e. _V -> ( x i^i ( { 1o } X. A ) ) ~<_ ( { 1o } X. A ) )
45 1on
 |-  1o e. On
46 xpsnen2g
 |-  ( ( 1o e. On /\ A e. _V ) -> ( { 1o } X. A ) ~~ A )
47 45 46 mpan
 |-  ( A e. _V -> ( { 1o } X. A ) ~~ A )
48 domentr
 |-  ( ( ( x i^i ( { 1o } X. A ) ) ~<_ ( { 1o } X. A ) /\ ( { 1o } X. A ) ~~ A ) -> ( x i^i ( { 1o } X. A ) ) ~<_ A )
49 44 47 48 syl2anc
 |-  ( A e. _V -> ( x i^i ( { 1o } X. A ) ) ~<_ A )
50 domen1
 |-  ( ( x i^i ( { 1o } X. A ) ) ~~ _om -> ( ( x i^i ( { 1o } X. A ) ) ~<_ A <-> _om ~<_ A ) )
51 49 50 syl5ibcom
 |-  ( A e. _V -> ( ( x i^i ( { 1o } X. A ) ) ~~ _om -> _om ~<_ A ) )
52 38 51 jaod
 |-  ( A e. _V -> ( ( ( x i^i ( { (/) } X. A ) ) ~~ _om \/ ( x i^i ( { 1o } X. A ) ) ~~ _om ) -> _om ~<_ A ) )
53 25 52 syl5
 |-  ( A e. _V -> ( ( ( x i^i ( { (/) } X. A ) ) u. ( x i^i ( { 1o } X. A ) ) ) ~~ _om -> _om ~<_ A ) )
54 24 53 syl5
 |-  ( A e. _V -> ( ( _om ~~ x /\ x C_ ( A |_| A ) ) -> _om ~<_ A ) )
55 54 exlimdv
 |-  ( A e. _V -> ( E. x ( _om ~~ x /\ x C_ ( A |_| A ) ) -> _om ~<_ A ) )
56 11 14 55 sylc
 |-  ( _om ~<_ ( A |_| A ) -> _om ~<_ A )
57 6 56 impbii
 |-  ( _om ~<_ A <-> _om ~<_ ( A |_| A ) )