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

Proof

Step	Hyp	Ref	Expression
1		bj-iminvid.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-iminvval2	|- ( ph -> ( ( A ~P^* A ) ` ( _I |` A ) ) = { <. x , y >. | ( ( x C_ A /\ y C_ A ) /\ x = ( `' ( _I |` A ) " y ) ) } )
5		cnvresid	|- `' ( _I |` A ) = ( _I |` A )
6	5	imaeq1i	|- ( `' ( _I |` A ) " y ) = ( ( _I |` A ) " y )
7		resiima	|- ( y C_ A -> ( ( _I |` A ) " y ) = y )
8	6 7	syl5eq	|- ( y C_ A -> ( `' ( _I |` A ) " y ) = y )
9	8	adantl	|- ( ( x C_ A /\ y C_ A ) -> ( `' ( _I |` A ) " y ) = y )
10	9	eqeq2d	|- ( ( x C_ A /\ y C_ A ) -> ( x = ( `' ( _I |` A ) " y ) <-> x = y ) )
11	10	bj-imdiridlem	|- { <. x , y >. | ( ( x C_ A /\ y C_ A ) /\ x = ( `' ( _I |` A ) " y ) ) } = ( _I |` ~P A )
12	4 11	eqtrdi	|- ( ph -> ( ( A ~P^* A ) ` ( _I |` A ) ) = ( _I |` ~P A ) )