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 ( ( 𝐴𝑉 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ 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 )