Theorem fin1ai

Description: Property of a Ia-finite set. (Contributed by Stefan O'Rear, 16-May-2015)

	Ref	Expression
Assertion	fin1ai	⊢ ( ( 𝐴 ∈ FinIa ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑋 ∈ Fin ∨ ( 𝐴 ∖ 𝑋 ) ∈ Fin ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ Fin ↔ 𝑋 ∈ Fin ) )
2		difeq2	⊢ ( 𝑥 = 𝑋 → ( 𝐴 ∖ 𝑥 ) = ( 𝐴 ∖ 𝑋 ) )
3	2	eleq1d	⊢ ( 𝑥 = 𝑋 → ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ↔ ( 𝐴 ∖ 𝑋 ) ∈ Fin ) )
4	1 3	orbi12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ Fin ) ↔ ( 𝑋 ∈ Fin ∨ ( 𝐴 ∖ 𝑋 ) ∈ Fin ) ) )
5		isfin1a	⊢ ( 𝐴 ∈ FinIa → ( 𝐴 ∈ FinIa ↔ ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ Fin ) ) )
6	5	ibi	⊢ ( 𝐴 ∈ FinIa → ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ Fin ) )
7	6	adantr	⊢ ( ( 𝐴 ∈ FinIa ∧ 𝑋 ⊆ 𝐴 ) → ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ Fin ) )
8		elpw2g	⊢ ( 𝐴 ∈ FinIa → ( 𝑋 ∈ 𝒫 𝐴 ↔ 𝑋 ⊆ 𝐴 ) )
9	8	biimpar	⊢ ( ( 𝐴 ∈ FinIa ∧ 𝑋 ⊆ 𝐴 ) → 𝑋 ∈ 𝒫 𝐴 )
10	4 7 9	rspcdva	⊢ ( ( 𝐴 ∈ FinIa ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑋 ∈ Fin ∨ ( 𝐴 ∖ 𝑋 ) ∈ Fin ) )