Theorem fin11a

Description: Every I-finite set is Ia-finite. (Contributed by Stefan O'Rear, 30-Oct-2014) (Revised by Mario Carneiro, 17-May-2015)

	Ref	Expression
Assertion	fin11a	⊢ ( 𝐴 ∈ Fin → 𝐴 ∈ FinIa )

Proof

Step	Hyp	Ref	Expression
1		elpwi	⊢ ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴 )
2		ssfi	⊢ ( ( 𝐴 ∈ Fin ∧ 𝑥 ⊆ 𝐴 ) → 𝑥 ∈ Fin )
3	1 2	sylan2	⊢ ( ( 𝐴 ∈ Fin ∧ 𝑥 ∈ 𝒫 𝐴 ) → 𝑥 ∈ Fin )
4	3	orcd	⊢ ( ( 𝐴 ∈ Fin ∧ 𝑥 ∈ 𝒫 𝐴 ) → ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ Fin ) )
5	4	ralrimiva	⊢ ( 𝐴 ∈ Fin → ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ Fin ) )
6		isfin1a	⊢ ( 𝐴 ∈ Fin → ( 𝐴 ∈ FinIa ↔ ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ Fin ) ) )
7	5 6	mpbird	⊢ ( 𝐴 ∈ Fin → 𝐴 ∈ FinIa )