This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 dfss2 
 |-  ( 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 ) )