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

Metamath Proof Explorer

Theorem domtriom

Description: Trichotomy of equinumerosity for _om , proven using countable choice. Equivalently, all Dedekind-finite sets (as in isfin4-2 ) are finite in the usual sense and conversely. (Contributed by Mario Carneiro, 9-Feb-2013)

Ref Expression
Hypothesis domtriom.1 
|- A e. _V
Assertion domtriom 
|- ( _om ~<_ A <-> -. A ~< _om )

Proof

Step Hyp Ref Expression
1 domtriom.1 
 |-  A e. _V
2 domnsym 
 |-  ( _om ~<_ A -> -. A ~< _om )
3 isfinite 
 |-  ( A e. Fin <-> A ~< _om )
4 eqid 
 |-  { y | ( y C_ A /\ y ~~ ~P n ) } = { y | ( y C_ A /\ y ~~ ~P n ) }
5 fveq2 
 |-  ( m = n -> ( b ` m ) = ( b ` n ) )
6 fveq2 
 |-  ( j = k -> ( b ` j ) = ( b ` k ) )
7 6 cbviunv 
 |-  U_ j e. m ( b ` j ) = U_ k e. m ( b ` k )
8 iuneq1 
 |-  ( m = n -> U_ k e. m ( b ` k ) = U_ k e. n ( b ` k ) )
9 7 8 eqtrid 
 |-  ( m = n -> U_ j e. m ( b ` j ) = U_ k e. n ( b ` k ) )
10 5 9 difeq12d 
 |-  ( m = n -> ( ( b ` m ) \ U_ j e. m ( b ` j ) ) = ( ( b ` n ) \ U_ k e. n ( b ` k ) ) )
11 10 cbvmptv 
 |-  ( m e. _om |-> ( ( b ` m ) \ U_ j e. m ( b ` j ) ) ) = ( n e. _om |-> ( ( b ` n ) \ U_ k e. n ( b ` k ) ) )
12 1 4 11 domtriomlem 
 |-  ( -. A e. Fin -> _om ~<_ A )
13 3 12 sylnbir 
 |-  ( -. A ~< _om -> _om ~<_ A )
14 2 13 impbii 
 |-  ( _om ~<_ A <-> -. A ~< _om )