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

Metamath Proof Explorer

Theorem fin1a2lem8

Description: Lemma for fin1a2 . Split a III-infinite set in two pieces. (Contributed by Stefan O'Rear, 7-Nov-2014)

		Ref	Expression
	Assertion	fin1a2lem8	$⊢ (A \in V \land \forall x \in 𝒫 A (x \in {Fin}^{III} \lor A ∖ x \in {Fin}^{III})) \to A \in {Fin}^{III}$

Step	Hyp	Ref	Expression
1		eqid	$⊢ (y \in ω ⟼ 2_{𝑜} \cdot_{𝑜} y) = (y \in ω ⟼ 2_{𝑜} \cdot_{𝑜} y)$
2		eqid	$⊢ (y \in On ⟼ suc y) = (y \in On ⟼ suc y)$
3	1 2	fin1a2lem7	$⊢ (A \in V \land \forall x \in 𝒫 A (x \in {Fin}^{III} \lor A ∖ x \in {Fin}^{III})) \to A \in {Fin}^{III}$