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 ⊢ 𝐴 ∈ V
Assertion domtriom ( ω ≼ 𝐴 ↔ ¬ 𝐴 ≺ ω )

Proof

Step Hyp Ref Expression
1 domtriom.1 ⊢ 𝐴 ∈ V
2 domnsym ⊢ ( ω ≼ 𝐴 → ¬ 𝐴 ≺ ω )
3 isfinite ⊢ ( 𝐴 ∈ Fin ↔ 𝐴 ≺ ω )
4 eqid ⊢ { 𝑦 ∣ ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛 ) } = { 𝑦 ∣ ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛 ) }
5 fveq2 ⊢ ( 𝑚 = 𝑛 → ( 𝑏 ‘ 𝑚 ) = ( 𝑏 ‘ 𝑛 ) )
6 fveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝑏 ‘ 𝑗 ) = ( 𝑏 ‘ 𝑘 ) )
7 6 cbviunv ⊢ ∪ 𝑗 ∈ 𝑚 ( 𝑏 ‘ 𝑗 ) = ∪ 𝑘 ∈ 𝑚 ( 𝑏 ‘ 𝑘 )
8 iuneq1 ⊢ ( 𝑚 = 𝑛 → ∪ 𝑘 ∈ 𝑚 ( 𝑏 ‘ 𝑘 ) = ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) )
9 7 8 eqtrid ⊢ ( 𝑚 = 𝑛 → ∪ 𝑗 ∈ 𝑚 ( 𝑏 ‘ 𝑗 ) = ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) )
10 5 9 difeq12d ⊢ ( 𝑚 = 𝑛 → ( ( 𝑏 ‘ 𝑚 ) ∖ ∪ 𝑗 ∈ 𝑚 ( 𝑏 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) ) )
11 10 cbvmptv ⊢ ( 𝑚 ∈ ω ↦ ( ( 𝑏 ‘ 𝑚 ) ∖ ∪ 𝑗 ∈ 𝑚 ( 𝑏 ‘ 𝑗 ) ) ) = ( 𝑛 ∈ ω ↦ ( ( 𝑏 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) ) )
12 1 4 11 domtriomlem ⊢ ( ¬ 𝐴 ∈ Fin → ω ≼ 𝐴 )
13 3 12 sylnbir ⊢ ( ¬ 𝐴 ≺ ω → ω ≼ 𝐴 )
14 2 13 impbii ⊢ ( ω ≼ 𝐴 ↔ ¬ 𝐴 ≺ ω )