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 V
Assertion domtriom ω A ¬ A ω

Proof

Step Hyp Ref Expression
1 domtriom.1 A V
2 domnsym ω A ¬ A ω
3 isfinite A Fin A ω
4 eqid y | y A y 𝒫 n = y | y A y 𝒫 n
5 fveq2 m = n b m = b n
6 fveq2 j = k b j = b k
7 6 cbviunv j m b j = k m b k
8 iuneq1 m = n k m b k = k n b k
9 7 8 eqtrid m = n j m b j = k n b k
10 5 9 difeq12d m = n b m j m b j = b n k n b k
11 10 cbvmptv m ω b m j m b j = n ω b n k n b k
12 1 4 11 domtriomlem ¬ A Fin ω A
13 3 12 sylnbir ¬ A ω ω A
14 2 13 impbii ω A ¬ A ω