Metamath Proof Explorer

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

Proof

Step	Hyp	Ref	Expression
1		bj-imdirid.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-imdirval2	$⊢ φ \to (A 𝒫_{*} A) ({I ↾}_{A}) = \{⟨x, y⟩ \| ((x \subseteq A \land y \subseteq A) \land ({I ↾}_{A}) [x] = y)\}$
5		resiima	$⊢ x \subseteq A \to ({I ↾}_{A}) [x] = x$
6	5	adantr	$⊢ (x \subseteq A \land y \subseteq A) \to ({I ↾}_{A}) [x] = x$
7	6	eqeq1d	$⊢ (x \subseteq A \land y \subseteq A) \to (({I ↾}_{A}) [x] = y \leftrightarrow x = y)$
8	7	bj-imdiridlem	$⊢ \{⟨x, y⟩ \| ((x \subseteq A \land y \subseteq A) \land ({I ↾}_{A}) [x] = y)\} = {I ↾}_{𝒫 A}$
9	4 8	eqtrdi	$⊢ φ \to (A 𝒫_{*} A) ({I ↾}_{A}) = {I ↾}_{𝒫 A}$