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	syl5eq	⊢ ( 𝑚 = 𝑛 → ∪ 𝑗 ∈ 𝑚 ( 𝑏 ‘ 𝑗 ) = ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) )
10	5 9	difeq12d	⊢ ( 𝑚 = 𝑛 → ( ( 𝑏 ‘ 𝑚 ) ∖ ∪ 𝑗 ∈ 𝑚 ( 𝑏 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) ) )
11	10	cbvmptv	⊢ ( 𝑚 ∈ ω ↦ ( ( 𝑏 ‘ 𝑚 ) ∖ ∪ 𝑗 ∈ 𝑚 ( 𝑏 ‘ 𝑗 ) ) ) = ( 𝑛 ∈ ω ↦ ( ( 𝑏 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ 𝑛 ( 𝑏 ‘ 𝑘 ) ) )
12	1 4 11	domtriomlem	⊢ ( ¬ 𝐴 ∈ Fin → ω ≼ 𝐴 )
13	3 12	sylnbir	⊢ ( ¬ 𝐴 ≺ ω → ω ≼ 𝐴 )
14	2 13	impbii	⊢ ( ω ≼ 𝐴 ↔ ¬ 𝐴 ≺ ω )