Theorem bj-iminvid

Description: Functorial property of the inverse image: the inverse image by the identity on a set is the identity on the powerset. (Contributed by BJ, 26-May-2024)

	Ref	Expression
Hypothesis	bj-iminvid.ex	$$⊢\phi \to A\in U$$
Assertion	bj-iminvid	Could not format assertion : No typesetting found for |- ( ph -> ( ( A ~P^* A ) ` ( _I |` A ) ) = ( _I |` ~P A ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		bj-iminvid.ex	$$⊢\phi \to A\in U$$
2		idssxp	$$⊢{\mathrm{I}\upharpoonright }_A\subseteq A\times A$$
3	2	a1i	$$⊢\phi \to {\mathrm{I}\upharpoonright }_A\subseteq A\times A$$
4	1 1 3	bj-iminvval2	Could not format ( ph -> ( ( A ~P^* A ) ` ( _I |` A ) ) = { <. x , y >. | ( ( x C_ A /\ y C_ A ) /\ x = ( `' ( _I |` A ) " y ) ) } ) : No typesetting found for |- ( ph -> ( ( A ~P^* A ) ` ( _I |` A ) ) = { <. x , y >. | ( ( x C_ A /\ y C_ A ) /\ x = ( `' ( _I |` A ) " y ) ) } ) with typecode |-
5		cnvresid	$$⊢{\left({\mathrm{I}\upharpoonright }_A\right)}^{-1}={\mathrm{I}\upharpoonright }_A$$
6	5	imaeq1i	$$⊢{\left({\mathrm{I}\upharpoonright }_A\right)}^{-1}\left[y\right]=\left({\mathrm{I}\upharpoonright }_A\right)\left[y\right]$$
7		resiima	$$⊢y\subseteq A\to \left({\mathrm{I}\upharpoonright }_A\right)\left[y\right]=y$$
8	6 7	syl5eq	$$⊢y\subseteq A\to {\left({\mathrm{I}\upharpoonright }_A\right)}^{-1}\left[y\right]=y$$
9	8	adantl	$$⊢\left(x\subseteq A\wedge y\subseteq A\right)\to {\left({\mathrm{I}\upharpoonright }_A\right)}^{-1}\left[y\right]=y$$
10	9	eqeq2d	$$⊢\left(x\subseteq A\wedge y\subseteq A\right)\to \left(x={\left({\mathrm{I}\upharpoonright }_A\right)}^{-1}\left[y\right]\leftrightarrow x=y\right)$$
11	10	bj-imdiridlem	$$⊢\left\{⟨x,y⟩|\left(\left(x\subseteq A\wedge y\subseteq A\right)\wedge x={\left({\mathrm{I}\upharpoonright }_A\right)}^{-1}\left[y\right]\right)\right\}={\mathrm{I}\upharpoonright }_{𝒫A}$$
12	4 11	eqtrdi	Could not format ( ph -> ( ( A ~P^* A ) ` ( _I |` A ) ) = ( _I |` ~P A ) ) : No typesetting found for |- ( ph -> ( ( A ~P^* A ) ` ( _I |` A ) ) = ( _I |` ~P A ) ) with typecode |-