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