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 ∈ 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 ≺ ω