Metamath Proof Explorer


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 φ A 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 φ A U
2 idssxp I A A × A
3 2 a1i φ I A A × 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 I A -1 = I A
6 5 imaeq1i I A -1 y = I A y
7 resiima y A I A y = y
8 6 7 syl5eq y A I A -1 y = y
9 8 adantl x A y A I A -1 y = y
10 9 eqeq2d x A y A x = I A -1 y x = y
11 10 bj-imdiridlem x y | x A y A x = I A -1 y = I 𝒫 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 |-