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	|- ( ph -> A e. U )
Assertion	bj-imdirid	|- ( ph -> ( ( A ~P_* A ) ` ( _I |` A ) ) = ( _I |` ~P A ) )

Proof

Step	Hyp	Ref	Expression
1		bj-imdirid.ex	|- ( ph -> A e. U )
2		idssxp	|- ( _I |` A ) C_ ( A X. A )
3	2	a1i	|- ( ph -> ( _I |` A ) C_ ( A X. A ) )
4	1 1 3	bj-imdirval2	|- ( ph -> ( ( A ~P_* A ) ` ( _I |` A ) ) = { <. x , y >. | ( ( x C_ A /\ y C_ A ) /\ ( ( _I |` A ) " x ) = y ) } )
5		resiima	|- ( x C_ A -> ( ( _I |` A ) " x ) = x )
6	5	adantr	|- ( ( x C_ A /\ y C_ A ) -> ( ( _I |` A ) " x ) = x )
7	6	eqeq1d	|- ( ( x C_ A /\ y C_ A ) -> ( ( ( _I |` A ) " x ) = y <-> x = y ) )
8	7	bj-imdiridlem	|- { <. x , y >. | ( ( x C_ A /\ y C_ A ) /\ ( ( _I |` A ) " x ) = y ) } = ( _I |` ~P A )
9	4 8	eqtrdi	|- ( ph -> ( ( A ~P_* A ) ` ( _I |` A ) ) = ( _I |` ~P A ) )