Metamath Proof Explorer


Theorem isfin1-4

Description: A set is I-finite iff every system of subsets contains a minimal subset. (Contributed by Stefan O'Rear, 4-Nov-2014) (Revised by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion isfin1-4 ( 𝐴𝑉 → ( 𝐴 ∈ Fin ↔ [] Fr 𝒫 𝐴 ) )

Proof

Step Hyp Ref Expression
1 isfin1-3 ( 𝐴𝑉 → ( 𝐴 ∈ Fin ↔ [] Fr 𝒫 𝐴 ) )
2 eqid ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝐴𝑥 ) ) = ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝐴𝑥 ) )
3 2 compssiso ( 𝐴𝑉 → ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝐴𝑥 ) ) Isom [] , [] ( 𝒫 𝐴 , 𝒫 𝐴 ) )
4 isofr ( ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝐴𝑥 ) ) Isom [] , [] ( 𝒫 𝐴 , 𝒫 𝐴 ) → ( [] Fr 𝒫 𝐴 [] Fr 𝒫 𝐴 ) )
5 3 4 syl ( 𝐴𝑉 → ( [] Fr 𝒫 𝐴 [] Fr 𝒫 𝐴 ) )
6 1 5 bitr4d ( 𝐴𝑉 → ( 𝐴 ∈ Fin ↔ [] Fr 𝒫 𝐴 ) )