isf34lem3

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

Step	Hyp	Ref	Expression
1		compss.a	$⊢ F = (x \in 𝒫 A ⟼ A ∖ x)$
2	1	compsscnv	$⊢ F^{-1} = F$
3	2	imaeq1i	$⊢ F^{-1} [F [X]] = F [F [X]]$
4	1	compssiso	$⊢ A \in V \to F {Isom}_{[\subset], {[\subset]}^{-1}} (𝒫 A, 𝒫 A)$
5		isof1o	$⊢ F {Isom}_{[\subset], {[\subset]}^{-1}} (𝒫 A, 𝒫 A) \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	$⊢ (F : 𝒫 A \underset{1-1}{⟶} 𝒫 A \land X \subseteq 𝒫 A) \to F^{-1} [F [X]] = X$
9	7 8	sylan	$⊢ (A \in V \land X \subseteq 𝒫 A) \to F^{-1} [F [X]] = X$
10	3 9	eqtr3id	$⊢ (A \in V \land X \subseteq 𝒫 A) \to F [F [X]] = X$

Metamath Proof Explorer