Theorem bj-imdirid

Description: Functorial property of the direct image: the direct image by the identity on a set is the identity on the powerset. (Contributed by BJ, 24-Dec-2023)

	Ref	Expression
Hypothesis	bj-imdirid.ex	$$⊢\phi \to A\in U$$
Assertion	bj-imdirid	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-imdirid.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-imdirval2	Could not format ( ph -> ( ( A ~P_* A ) ` ( _I |` A ) ) = { <. x , y >. | ( ( x C_ A /\ y C_ A ) /\ ( ( _I |` A ) " x ) = y ) } ) : No typesetting found for |- ( ph -> ( ( A ~P_* A ) ` ( _I |` A ) ) = { <. x , y >. | ( ( x C_ A /\ y C_ A ) /\ ( ( _I |` A ) " x ) = y ) } ) with typecode |-
5		resiima	$$⊢x\subseteq A\to \left({\mathrm{I}\upharpoonright }_A\right)\left[x\right]=x$$
6	5	adantr	$$⊢\left(x\subseteq A\wedge y\subseteq A\right)\to \left({\mathrm{I}\upharpoonright }_A\right)\left[x\right]=x$$
7	6	eqeq1d	$$⊢\left(x\subseteq A\wedge y\subseteq A\right)\to \left(\left({\mathrm{I}\upharpoonright }_A\right)\left[x\right]=y\leftrightarrow x=y\right)$$
8	7	bj-imdiridlem	$$⊢\left\{⟨x,y⟩|\left(\left(x\subseteq A\wedge y\subseteq A\right)\wedge \left({\mathrm{I}\upharpoonright }_A\right)\left[x\right]=y\right)\right\}={\mathrm{I}\upharpoonright }_{𝒫A}$$
9	4 8	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 |-