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

Metamath Proof Explorer

Theorem isfin3-2

Description: Weakly Dedekind-infinite sets are exactly those which can be mapped onto _om . (Contributed by Stefan O'Rear, 6-Nov-2014) (Proof shortened by Mario Carneiro, 17-May-2015)

		Ref	Expression
	Assertion	isfin3-2	$⊢ A \in V \to (A \in {Fin}^{III} \leftrightarrow \neg ω ≼^{*} A)$

Proof

Step	Hyp	Ref	Expression
1		isfin32i	$⊢ A \in {Fin}^{III} \to \neg ω ≼^{*} A$
2		isf33lem	$⊢ {Fin}^{III} = \{g \| \forall a \in ({𝒫 g}^{ω}) (\forall x \in ω a (suc x) \subseteq a (x) \to ⋂ ran a \in ran a)\}$
3	2	isf32lem12	$⊢ A \in V \to (\neg ω ≼^{*} A \to A \in {Fin}^{III})$
4	1 3	impbid2	$⊢ A \in V \to (A \in {Fin}^{III} \leftrightarrow \neg ω ≼^{*} A)$