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 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | ⊢ ( 𝑦 ∈ ω ↦ ( 2o ·o 𝑦 ) ) = ( 𝑦 ∈ ω ↦ ( 2o ·o 𝑦 ) ) | |
2 | eqid | ⊢ ( 𝑦 ∈ On ↦ suc 𝑦 ) = ( 𝑦 ∈ On ↦ suc 𝑦 ) | |
3 | 1 2 | fin1a2lem7 | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ FinIII ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinIII ) ) → 𝐴 ∈ FinIII ) |