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

Proof

Step	Hyp	Ref	Expression
1		bj-imdirid.ex	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
2		idssxp	⊢ ( I ↾ 𝐴 ) ⊆ ( 𝐴 × 𝐴 )
3	2	a1i	⊢ ( 𝜑 → ( I ↾ 𝐴 ) ⊆ ( 𝐴 × 𝐴 ) )
4	1 1 3	bj-imdirval2	⊢ ( 𝜑 → ( ( 𝐴 𝒫* 𝐴 ) ‘ ( I ↾ 𝐴 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴 ) ∧ ( ( I ↾ 𝐴 ) “ 𝑥 ) = 𝑦 ) } )
5		resiima	⊢ ( 𝑥 ⊆ 𝐴 → ( ( I ↾ 𝐴 ) “ 𝑥 ) = 𝑥 )
6	5	adantr	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴 ) → ( ( I ↾ 𝐴 ) “ 𝑥 ) = 𝑥 )
7	6	eqeq1d	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴 ) → ( ( ( I ↾ 𝐴 ) “ 𝑥 ) = 𝑦 ↔ 𝑥 = 𝑦 ) )
8	7	bj-imdiridlem	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴 ) ∧ ( ( I ↾ 𝐴 ) “ 𝑥 ) = 𝑦 ) } = ( I ↾ 𝒫 𝐴 )
9	4 8	eqtrdi	⊢ ( 𝜑 → ( ( 𝐴 𝒫* 𝐴 ) ‘ ( I ↾ 𝐴 ) ) = ( I ↾ 𝒫 𝐴 ) )