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

Metamath Proof Explorer

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 ) )