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	$⊢ x \in V$
2	1	domtriom	$⊢ ω ≼ x \leftrightarrow \neg x ≺ ω$
3	2	con2bii	$⊢ x ≺ ω \leftrightarrow \neg ω ≼ x$
4		isfinite	$⊢ x \in Fin \leftrightarrow x ≺ ω$
5		isfin4-2	$⊢ x \in V \to (x \in {Fin}^{IV} \leftrightarrow \neg ω ≼ x)$
6	5	elv	$⊢ x \in {Fin}^{IV} \leftrightarrow \neg ω ≼ x$
7	3 4 6	3bitr4ri	$⊢ x \in {Fin}^{IV} \leftrightarrow x \in Fin$
8	7	eqriv	$⊢ {Fin}^{IV} = Fin$