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	|- ( A e. V -> ( A e. Fin <-> [C.] Fr ~P A ) )

Proof

Step	Hyp	Ref	Expression
1		isfin1-3	|- ( A e. V -> ( A e. Fin <-> `' [C.] Fr ~P A ) )
2		eqid	|- ( x e. ~P A |-> ( A \ x ) ) = ( x e. ~P A |-> ( A \ x ) )
3	2	compssiso	|- ( A e. V -> ( x e. ~P A |-> ( A \ x ) ) Isom [C.] , `' [C.] ( ~P A , ~P A ) )
4		isofr	|- ( ( x e. ~P A |-> ( A \ x ) ) Isom [C.] , `' [C.] ( ~P A , ~P A ) -> ( [C.] Fr ~P A <-> `' [C.] Fr ~P A ) )
5	3 4	syl	|- ( A e. V -> ( [C.] Fr ~P A <-> `' [C.] Fr ~P A ) )
6	1 5	bitr4d	|- ( A e. V -> ( A e. Fin <-> [C.] Fr ~P A ) )