Theorem fin41

Description: Under countable choice, the IV-finite sets (Dedekind-finite) coincide with I-finite (finite in the usual sense) sets. (Contributed by Mario Carneiro, 16-May-2015)

	Ref	Expression
Assertion	fin41	⊢ FinIV = Fin

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2	1	domtriom	⊢ ( ω ≼ 𝑥 ↔ ¬ 𝑥 ≺ ω )
3	2	con2bii	⊢ ( 𝑥 ≺ ω ↔ ¬ ω ≼ 𝑥 )
4		isfinite	⊢ ( 𝑥 ∈ Fin ↔ 𝑥 ≺ ω )
5		isfin4-2	⊢ ( 𝑥 ∈ V → ( 𝑥 ∈ FinIV ↔ ¬ ω ≼ 𝑥 ) )
6	5	elv	⊢ ( 𝑥 ∈ FinIV ↔ ¬ ω ≼ 𝑥 )
7	3 4 6	3bitr4ri	⊢ ( 𝑥 ∈ FinIV ↔ 𝑥 ∈ Fin )
8	7	eqriv	⊢ FinIV = Fin