Theorem isf34lem3

Description: Lemma for isfin3-4 . (Contributed by Stefan O'Rear, 7-Nov-2014) (Revised by Mario Carneiro, 17-May-2015)

	Ref	Expression
Hypothesis	compss.a	$$⊢F=\left(x\in 𝒫A⟼A\setminus x\right)$$
Assertion	isf34lem3	$$⊢\left(A\in V\wedge X\subseteq 𝒫A\right)\to F\left[F\left[X\right]\right]=X$$

Proof

Step	Hyp	Ref	Expression
1		compss.a	$$⊢F=\left(x\in 𝒫A⟼A\setminus x\right)$$
2	1	compsscnv	$$⊢F^{-1}=F$$
3	2	imaeq1i	$$⊢F^{-1}\left[F\left[X\right]\right]=F\left[F\left[X\right]\right]$$
4	1	compssiso	$$⊢A\in V\to F{Isom}_{[\subset ],{[\subset ]}^{-1}}\left(𝒫A,𝒫A\right)$$
5		isof1o	$$⊢F{Isom}_{[\subset ],{[\subset ]}^{-1}}\left(𝒫A,𝒫A\right)\to F:𝒫A\underset{1-1\; onto}{⟶}𝒫A$$
6		f1of1	$$⊢F:𝒫A\underset{1-1\; onto}{⟶}𝒫A\to F:𝒫A\underset{1-1}{⟶}𝒫A$$
7	4 5 6	3syl	$$⊢A\in V\to F:𝒫A\underset{1-1}{⟶}𝒫A$$
8		f1imacnv	$$⊢\left(F:𝒫A\underset{1-1}{⟶}𝒫A\wedge X\subseteq 𝒫A\right)\to F^{-1}\left[F\left[X\right]\right]=X$$
9	7 8	sylan	$$⊢\left(A\in V\wedge X\subseteq 𝒫A\right)\to F^{-1}\left[F\left[X\right]\right]=X$$
10	3 9	eqtr3id	$$⊢\left(A\in V\wedge X\subseteq 𝒫A\right)\to F\left[F\left[X\right]\right]=X$$