This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ Fin^IV = Fin

Proof

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