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	$⊢ φ \to A \in U$
	Assertion	bj-iminvid	$⊢ φ \to (A 𝒫^{*} A) ({I ↾}_{A}) = {I ↾}_{𝒫 A}$

Proof

Step	Hyp	Ref	Expression
1		bj-iminvid.ex	$⊢ φ \to A \in U$
2		idssxp	$⊢ {I ↾}_{A} \subseteq A \times A$
3	2	a1i	$⊢ φ \to {I ↾}_{A} \subseteq A \times A$
4	1 1 3	bj-iminvval2	$⊢ φ \to (A 𝒫^{*} A) ({I ↾}_{A}) = \{⟨x, y⟩ \| ((x \subseteq A \land y \subseteq A) \land x = {({I ↾}_{A})}^{-1} [y])\}$
5		cnvresid	$⊢ {({I ↾}_{A})}^{-1} = {I ↾}_{A}$
6	5	imaeq1i	$⊢ {({I ↾}_{A})}^{-1} [y] = ({I ↾}_{A}) [y]$
7		resiima	$⊢ y \subseteq A \to ({I ↾}_{A}) [y] = y$
8	6 7	eqtrid	$⊢ y \subseteq A \to {({I ↾}_{A})}^{-1} [y] = y$
9	8	adantl	$⊢ (x \subseteq A \land y \subseteq A) \to {({I ↾}_{A})}^{-1} [y] = y$
10	9	eqeq2d	$⊢ (x \subseteq A \land y \subseteq A) \to (x = {({I ↾}_{A})}^{-1} [y] \leftrightarrow x = y)$
11	10	bj-imdiridlem	$⊢ \{⟨x, y⟩ \| ((x \subseteq A \land y \subseteq A) \land x = {({I ↾}_{A})}^{-1} [y])\} = {I ↾}_{𝒫 A}$
12	4 11	eqtrdi	$⊢ φ \to (A 𝒫^{*} A) ({I ↾}_{A}) = {I ↾}_{𝒫 A}$