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	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
Assertion	bj-iminvid	⊢ ( 𝜑 → ( ( 𝐴 𝒫* 𝐴 ) ‘ ( I ↾ 𝐴 ) ) = ( I ↾ 𝒫 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		bj-iminvid.ex	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
2		idssxp	⊢ ( I ↾ 𝐴 ) ⊆ ( 𝐴 × 𝐴 )
3	2	a1i	⊢ ( 𝜑 → ( I ↾ 𝐴 ) ⊆ ( 𝐴 × 𝐴 ) )
4	1 1 3	bj-iminvval2	⊢ ( 𝜑 → ( ( 𝐴 𝒫* 𝐴 ) ‘ ( I ↾ 𝐴 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑥 = ( ◡ ( I ↾ 𝐴 ) “ 𝑦 ) ) } )
5		cnvresid	⊢ ◡ ( I ↾ 𝐴 ) = ( I ↾ 𝐴 )
6	5	imaeq1i	⊢ ( ◡ ( I ↾ 𝐴 ) “ 𝑦 ) = ( ( I ↾ 𝐴 ) “ 𝑦 )
7		resiima	⊢ ( 𝑦 ⊆ 𝐴 → ( ( I ↾ 𝐴 ) “ 𝑦 ) = 𝑦 )
8	6 7	syl5eq	⊢ ( 𝑦 ⊆ 𝐴 → ( ◡ ( I ↾ 𝐴 ) “ 𝑦 ) = 𝑦 )
9	8	adantl	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴 ) → ( ◡ ( I ↾ 𝐴 ) “ 𝑦 ) = 𝑦 )
10	9	eqeq2d	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴 ) → ( 𝑥 = ( ◡ ( I ↾ 𝐴 ) “ 𝑦 ) ↔ 𝑥 = 𝑦 ) )
11	10	bj-imdiridlem	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑥 = ( ◡ ( I ↾ 𝐴 ) “ 𝑦 ) ) } = ( I ↾ 𝒫 𝐴 )
12	4 11	eqtrdi	⊢ ( 𝜑 → ( ( 𝐴 𝒫* 𝐴 ) ‘ ( I ↾ 𝐴 ) ) = ( I ↾ 𝒫 𝐴 ) )