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\in V\to \left(A\in \mathrm{Fin}\leftrightarrow [\subset ]\mathrm{Fr}𝒫A\right)$$

Proof

Step	Hyp	Ref	Expression
1		isfin1-3	$$⊢A\in V\to \left(A\in \mathrm{Fin}\leftrightarrow {[\subset ]}^{-1}\mathrm{Fr}𝒫A\right)$$
2		eqid	$$⊢\left(x\in 𝒫A⟼A\setminus x\right)=\left(x\in 𝒫A⟼A\setminus x\right)$$
3	2	compssiso	$$⊢A\in V\to \left(x\in 𝒫A⟼A\setminus x\right){Isom}_{[\subset ],{[\subset ]}^{-1}}\left(𝒫A,𝒫A\right)$$
4		isofr	$$⊢\left(x\in 𝒫A⟼A\setminus x\right){Isom}_{[\subset ],{[\subset ]}^{-1}}\left(𝒫A,𝒫A\right)\to \left([\subset ]\mathrm{Fr}𝒫A\leftrightarrow {[\subset ]}^{-1}\mathrm{Fr}𝒫A\right)$$
5	3 4	syl	$$⊢A\in V\to \left([\subset ]\mathrm{Fr}𝒫A\leftrightarrow {[\subset ]}^{-1}\mathrm{Fr}𝒫A\right)$$
6	1 5	bitr4d	$$⊢A\in V\to \left(A\in \mathrm{Fin}\leftrightarrow [\subset ]\mathrm{Fr}𝒫A\right)$$