Metamath Proof Explorer

Theorem infdju1

Description: An infinite set is equinumerous to itself added with one. (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion infdju1 
|- ( _om ~<_ A -> ( A |_| 1o ) ~~ A )

Proof

Step Hyp Ref Expression
1 difun2 
 |-  ( ( ( { (/) } X. A ) u. ( { 1o } X. 1o ) ) \ ( { 1o } X. 1o ) ) = ( ( { (/) } X. A ) \ ( { 1o } X. 1o ) )
2 df-dju 
 |-  ( A |_| 1o ) = ( ( { (/) } X. A ) u. ( { 1o } X. 1o ) )
3 df1o2 
 |-  1o = { (/) }
4 3 xpeq2i 
 |-  ( { 1o } X. 1o ) = ( { 1o } X. { (/) } )
5 1oex 
 |-  1o e. _V
6 0ex 
 |-  (/) e. _V
7 5 6 xpsn 
 |-  ( { 1o } X. { (/) } ) = { <. 1o , (/) >. }
8 4 7 eqtr2i 
 |-  { <. 1o , (/) >. } = ( { 1o } X. 1o )
9 2 8 difeq12i 
 |-  ( ( A |_| 1o ) \ { <. 1o , (/) >. } ) = ( ( ( { (/) } X. A ) u. ( { 1o } X. 1o ) ) \ ( { 1o } X. 1o ) )
10 xp01disjl 
 |-  ( ( { (/) } X. A ) i^i ( { 1o } X. 1o ) ) = (/)
11 disj3 
 |-  ( ( ( { (/) } X. A ) i^i ( { 1o } X. 1o ) ) = (/) <-> ( { (/) } X. A ) = ( ( { (/) } X. A ) \ ( { 1o } X. 1o ) ) )
12 10 11 mpbi 
 |-  ( { (/) } X. A ) = ( ( { (/) } X. A ) \ ( { 1o } X. 1o ) )
13 1 9 12 3eqtr4i 
 |-  ( ( A |_| 1o ) \ { <. 1o , (/) >. } ) = ( { (/) } X. A )
14 reldom 
 |-  Rel ~<_
15 14 brrelex2i 
 |-  ( _om ~<_ A -> A e. _V )
16 1on 
 |-  1o e. On
17 djudoml 
 |-  ( ( A e. _V /\ 1o e. On ) -> A ~<_ ( A |_| 1o ) )
18 15 16 17 sylancl 
 |-  ( _om ~<_ A -> A ~<_ ( A |_| 1o ) )
19 domtr 
 |-  ( ( _om ~<_ A /\ A ~<_ ( A |_| 1o ) ) -> _om ~<_ ( A |_| 1o ) )
20 18 19 mpdan 
 |-  ( _om ~<_ A -> _om ~<_ ( A |_| 1o ) )
21 infdifsn 
 |-  ( _om ~<_ ( A |_| 1o ) -> ( ( A |_| 1o ) \ { <. 1o , (/) >. } ) ~~ ( A |_| 1o ) )
22 20 21 syl 
 |-  ( _om ~<_ A -> ( ( A |_| 1o ) \ { <. 1o , (/) >. } ) ~~ ( A |_| 1o ) )
23 13 22 eqbrtrrid 
 |-  ( _om ~<_ A -> ( { (/) } X. A ) ~~ ( A |_| 1o ) )
24 23 ensymd 
 |-  ( _om ~<_ A -> ( A |_| 1o ) ~~ ( { (/) } X. A ) )
25 xpsnen2g 
 |-  ( ( (/) e. _V /\ A e. _V ) -> ( { (/) } X. A ) ~~ A )
26 6 15 25 sylancr 
 |-  ( _om ~<_ A -> ( { (/) } X. A ) ~~ A )
27 entr 
 |-  ( ( ( A |_| 1o ) ~~ ( { (/) } X. A ) /\ ( { (/) } X. A ) ~~ A ) -> ( A |_| 1o ) ~~ A )
28 24 26 27 syl2anc 
 |-  ( _om ~<_ A -> ( A |_| 1o ) ~~ A )