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	⊢ ( 𝐴 ∈ Fin^Ia → 𝐴 ∈ Fin^II )

Proof

Step	Hyp	Ref	Expression
1		elpwi	⊢ ( 𝑏 ∈ 𝒫 𝐴 → 𝑏 ⊆ 𝐴 )
2		fin1ai	⊢ ( ( 𝐴 ∈ Fin^Ia ∧ 𝑏 ⊆ 𝐴 ) → ( 𝑏 ∈ Fin ∨ ( 𝐴 ∖ 𝑏 ) ∈ Fin ) )
3		fin12	⊢ ( ( 𝐴 ∖ 𝑏 ) ∈ Fin → ( 𝐴 ∖ 𝑏 ) ∈ Fin^II )
4	3	orim2i	⊢ ( ( 𝑏 ∈ Fin ∨ ( 𝐴 ∖ 𝑏 ) ∈ Fin ) → ( 𝑏 ∈ Fin ∨ ( 𝐴 ∖ 𝑏 ) ∈ Fin^II ) )
5	2 4	syl	⊢ ( ( 𝐴 ∈ Fin^Ia ∧ 𝑏 ⊆ 𝐴 ) → ( 𝑏 ∈ Fin ∨ ( 𝐴 ∖ 𝑏 ) ∈ Fin^II ) )
6	1 5	sylan2	⊢ ( ( 𝐴 ∈ Fin^Ia ∧ 𝑏 ∈ 𝒫 𝐴 ) → ( 𝑏 ∈ Fin ∨ ( 𝐴 ∖ 𝑏 ) ∈ Fin^II ) )
7	6	ralrimiva	⊢ ( 𝐴 ∈ Fin^Ia → ∀ 𝑏 ∈ 𝒫 𝐴 ( 𝑏 ∈ Fin ∨ ( 𝐴 ∖ 𝑏 ) ∈ Fin^II ) )
8		fin1a2s	⊢ ( ( 𝐴 ∈ Fin^Ia ∧ ∀ 𝑏 ∈ 𝒫 𝐴 ( 𝑏 ∈ Fin ∨ ( 𝐴 ∖ 𝑏 ) ∈ Fin^II ) ) → 𝐴 ∈ Fin^II )
9	7 8	mpdan	⊢ ( 𝐴 ∈ Fin^Ia → 𝐴 ∈ Fin^II )