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	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ FinIII ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinIII ) ) → 𝐴 ∈ FinIII )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝑦 ∈ ω ↦ ( 2o ·o 𝑦 ) ) = ( 𝑦 ∈ ω ↦ ( 2o ·o 𝑦 ) )
2		eqid	⊢ ( 𝑦 ∈ On ↦ suc 𝑦 ) = ( 𝑦 ∈ On ↦ suc 𝑦 )
3	1 2	fin1a2lem7	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ FinIII ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinIII ) ) → 𝐴 ∈ FinIII )