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

Metamath Proof Explorer

Theorem isfin1a

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

Ref Expression
Assertion isfin1a ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ FinIa ↔ ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ∈ Fin ∨ ( 𝐴 ∖ 𝑦 ) ∈ Fin ) ) )

Proof

Step Hyp Ref Expression
1 pweq ⊢ ( 𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴 )
2 difeq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∖ 𝑦 ) = ( 𝐴 ∖ 𝑦 ) )
3 2 eleq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∖ 𝑦 ) ∈ Fin ↔ ( 𝐴 ∖ 𝑦 ) ∈ Fin ) )
4 3 orbi2d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑦 ∈ Fin ∨ ( 𝑥 ∖ 𝑦 ) ∈ Fin ) ↔ ( 𝑦 ∈ Fin ∨ ( 𝐴 ∖ 𝑦 ) ∈ Fin ) ) )
5 1 4 raleqbidv ⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝑦 ∈ Fin ∨ ( 𝑥 ∖ 𝑦 ) ∈ Fin ) ↔ ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ∈ Fin ∨ ( 𝐴 ∖ 𝑦 ) ∈ Fin ) ) )
6 df-fin1a ⊢ FinIa = { 𝑥 ∣ ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝑦 ∈ Fin ∨ ( 𝑥 ∖ 𝑦 ) ∈ Fin ) }
7 5 6 elab2g ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ FinIa ↔ ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ∈ Fin ∨ ( 𝐴 ∖ 𝑦 ) ∈ Fin ) ) )