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

Metamath Proof Explorer

Theorem fin1a2

Description: Every Ia-finite set is II-finite. Theorem 1 of Levy58, p. 3. (Contributed by Stefan O'Rear, 8-Nov-2014) (Proof shortened by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion fin1a2 ⊢ A ∈ FinIa → A ∈ FinII

Proof

Step Hyp Ref Expression
1 elpwi ⊢ b ∈ 𝒫 A → b ⊆ A
2 fin1ai ⊢ A ∈ FinIa ∧ b ⊆ A → b ∈ Fin ∨ A ∖ b ∈ Fin
3 fin12 ⊢ A ∖ b ∈ Fin → A ∖ b ∈ FinII
4 3 orim2i ⊢ b ∈ Fin ∨ A ∖ b ∈ Fin → b ∈ Fin ∨ A ∖ b ∈ FinII
5 2 4 syl ⊢ A ∈ FinIa ∧ b ⊆ A → b ∈ Fin ∨ A ∖ b ∈ FinII
6 1 5 sylan2 ⊢ A ∈ FinIa ∧ b ∈ 𝒫 A → b ∈ Fin ∨ A ∖ b ∈ FinII
7 6 ralrimiva ⊢ A ∈ FinIa → ∀ b ∈ 𝒫 A b ∈ Fin ∨ A ∖ b ∈ FinII
8 fin1a2s ⊢ A ∈ FinIa ∧ ∀ b ∈ 𝒫 A b ∈ Fin ∨ A ∖ b ∈ FinII → A ∈ FinII
9 7 8 mpdan ⊢ A ∈ FinIa → A ∈ FinII